Document Open Access Logo

Asymptotic Complexity Estimates for Probabilistic Programs and Their VASS Abstractions

Authors Michal Ajdarów , Antonín Kučera

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2023.12.pdf
  • Filesize: 0.8 MB
  • 16 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
Keywords
  • Probabilistic programs
  • asymptotic complexity
  • vector addition systems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

The standard approach to analyzing the asymptotic complexity of probabilistic programs is based on studying the asymptotic growth of certain expected values (such as the expected termination time) for increasing input size. We argue that this approach is not sufficiently robust, especially in situations when the expectations are infinite. We propose new estimates for the asymptotic analysis of probabilistic programs with non-deterministic choice that overcome this deficiency. Furthermore, we show how to efficiently compute/analyze these estimates for selected classes of programs represented as Markov decision processes over vector addition systems with states.

Cite As Get BibTex

Michal Ajdarów and Antonín Kučera. Asymptotic Complexity Estimates for Probabilistic Programs and Their VASS Abstractions. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CONCUR.2023.12

Author Details

Michal Ajdarów
  • Masaryk University, Brno, Czech Republic
Antonín Kučera
  • Masaryk University, Brno, Czech Republic

Funding

The work is supported by the Czech Science Foundation, Grant No. 21-24711S.

References

  1. M. Ajdarów and A. Kučera. Deciding polynomial termination complexity for VASS programs. In Proceedings of CONCUR 2021, volume 203 of Leibniz International Proceedings in Informatics, pages 30:1-30:15. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2021. Google Scholar
  2. M Ajdarów and A. Kučera. Asymptotic complexity estimates for probabilistic programs and their vass abstractions. arXiv, 2307.04707 [cs.FL], 2023. Google Scholar
  3. T. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, and D. Velan. Deciding fast termination for probabilistic VASS with nondeterminism. In Proceedings of ATVA 2019, volume 11781 of Lecture Notes in Computer Science, pages 462-478. Springer, 2019. Google Scholar
  4. T. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, D. Velan, and F. Zuleger. Efficient algorithms for asymptotic bounds on termination time in VASS. In Proceedings of LICS 2018, pages 185-194. ACM Press, 2018. Google Scholar
  5. M. Broy and M. Wirsing. On the algebraic specification of nondeterministic programming languages. In Proceedings of CAAP'81, volume 112 of Lecture Notes in Computer Science, pages 162-179. Springer, 1981. Google Scholar
  6. K. Chatterjee and L. Doyen. Energy parity games. In Proceedings of ICALP 2010, Part II, volume 6199 of Lecture Notes in Computer Science, pages 599-610. Springer, 2010. Google Scholar
  7. K. Chatterjee and L. Doyen. Energy and mean-payoff parity Markov decision processes. In Proceedings of MFCS 2011, volume 6907 of Lecture Notes in Computer Science, pages 206-218. Springer, 2011. Google Scholar
  8. K. Chatterjee, M. Henzinger, S. Krinninger, and D. Nanongkai. Polynomial-time algorithms for energy games with special weight structures. In Proceedings of ESA 2012, volume 7501 of Lecture Notes in Computer Science, pages 301-312. Springer, 2012. Google Scholar
  9. W. Czerwiński, S. Lasota, R. Lazić, J. Leroux, and F. Mazowiecki. The reachability problem for Petri nets is not elementary. In Proceedings of STOC 2019, pages 24-33. ACM Press, 2019. Google Scholar
  10. J. Esparza. Decidability of model checking for infinite-state concurrent systems. Acta Informatica, 34:85-107, 1997. Google Scholar
  11. J.E. Hopcroft and J.-J. Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theoretical Computer Science, 8:135-159, 1979. Google Scholar
  12. P. Jančar. Undecidability of bisimilarity for Petri nets and some related problems. Theoretical Computer Science, 148(2):281-301, 1995. Google Scholar
  13. M. Jurdziński, R. Lazić, and S. Schmitz. Fixed-dimensional energy games are in pseudo-polynomial time. In Proceedings of ICALP 2015, volume 9135 of Lecture Notes in Computer Science, pages 260-272. Springer, 2015. Google Scholar
  14. A. Kučera. Algorithmic analysis of termination and counter complexity in vector addition systems with states: A survey of recent results. ACM SIGLOG News, 8(4):4-21, 2021. Google Scholar
  15. A. Kučera, J. Leroux, and D. Velan. Efficient analysis of VASS termination complexity. In Proceedings of LICS 2020, pages 676-688. ACM Press, 2020. Google Scholar
  16. J. Leroux. Polynomial vector addition systems with states. In Proceedings of ICALP 2018, volume 107 of Leibniz International Proceedings in Informatics, pages 134:1-134:13. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2018. Google Scholar
  17. J. Leroux and Ph. Schnoebelen. On functions weakly computable by Petri nets and vector addition systems. In Reachability Problems, volume 8762 of Lecture Notes in Computer Science, pages 190-202. Springer, 2014. Google Scholar
  18. R. Lipton. The reachability problem requires exponential space. Technical report 62, Yale University, 1976. Google Scholar
  19. E.W. Mayr and A.R. Meyer. The complexity of the finite containment problem for Petri nets. Journal of the Association for Computing Machinery, 28(3):561-576, 1981. Google Scholar
  20. C.A. Petri. Kommunikation mit automaten. Schriften des Institutes für Instrumentelle Mathematik, 3, 1962. Google Scholar
  21. M. Sinn, F. Zuleger, and H. Veith. A simple and scalable static analysis for bound analysis and amortized complexity analysis. In Proceedings of CAV 2014, volume 8559 of Lecture Notes in Computer Science, pages 745-761. Springer, 2013. Google Scholar
  22. M. Sinn, F. Zuleger, and H. Veith. Complexity and resource bound analysis of imperative programs using difference constraints. Journal of Automated Reasoning, 59(1):3-45, 2017. Google Scholar
  23. F. Zuleger. The polynomial complexity of vector addition systems with states. In Proceedings of FoSSaCS 2020, volume 12077 of Lecture Notes in Computer Science, pages 622-641. Springer, 2020. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact