Search Results

Documents authored by Ajdarów, Michal


Document
Asymptotic Complexity Estimates for Probabilistic Programs and Their VASS Abstractions

Authors: Michal Ajdarów and Antonín Kučera

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)


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

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)


Copy BibTex To Clipboard

@InProceedings{ajdarow_et_al:LIPIcs.CONCUR.2023.12,
  author =	{Ajdar\'{o}w, Michal and Ku\v{c}era, Anton{\'\i}n},
  title =	{{Asymptotic Complexity Estimates for Probabilistic Programs and Their VASS Abstractions}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{12:1--12:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.12},
  URN =		{urn:nbn:de:0030-drops-190065},
  doi =		{10.4230/LIPIcs.CONCUR.2023.12},
  annote =	{Keywords: Probabilistic programs, asymptotic complexity, vector addition systems}
}
Document
Deciding Polynomial Termination Complexity for VASS Programs

Authors: Michal Ajdarów and Antonín Kučera

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)


Abstract
We show that for every fixed degree k ≥ 3, the problem whether the termination/counter complexity of a given demonic VASS is O(n^k), Ω(n^k), and Θ(n^k) is coNP-complete, NP-complete, and DP-complete, respectively. We also classify the complexity of these problems for k ≤ 2. This shows that the polynomial-time algorithm designed for strongly connected demonic VASS in previous works cannot be extended to the general case. Then, we prove that the same problems for VASS games are PSPACE-complete. Again, we classify the complexity also for k ≤ 2. Tractable subclasses of demonic VASS and VASS games are obtained by bounding certain structural parameters, which opens the way to applications in program analysis despite the presented lower complexity bounds.

Cite as

Michal Ajdarów and Antonín Kučera. Deciding Polynomial Termination Complexity for VASS Programs. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 30:1-30:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{ajdarow_et_al:LIPIcs.CONCUR.2021.30,
  author =	{Ajdar\'{o}w, Michal and Ku\v{c}era, Anton{\'\i}n},
  title =	{{Deciding Polynomial Termination Complexity for VASS Programs}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{30:1--30:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.30},
  URN =		{urn:nbn:de:0030-drops-144076},
  doi =		{10.4230/LIPIcs.CONCUR.2021.30},
  annote =	{Keywords: Termination complexity, vector addition systems}
}
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