Found 3 Possible Name Variants:

Document

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

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.

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

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

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.

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} }

Document

**Published in:** LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Population protocols are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their states. Computations are infinite sequences of interactions in which the interacting devices are chosen uniformly at random.
In well designed population protocols, for every initial configuration of devices, and for every computation starting at this configuration, all devices eventually agree on a consensus value. We address the problem of automatically computing a parametric bound on the expected time the protocol needs to reach this consensus. We present the first algorithm that, when successful, outputs a function f(n) such that the expected time to consensus is bound by O(f(n)), where n is the number of devices executing the protocol. We experimentally show that our algorithm terminates and provides good bounds for many of the protocols found in the literature.

Michael Blondin, Javier Esparza, and Antonín Kucera. Automatic Analysis of Expected Termination Time for Population Protocols. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{blondin_et_al:LIPIcs.CONCUR.2018.33, author = {Blondin, Michael and Esparza, Javier and Kucera, Anton{\'\i}n}, title = {{Automatic Analysis of Expected Termination Time for Population Protocols}}, booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)}, pages = {33:1--33:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-087-3}, ISSN = {1868-8969}, year = {2018}, volume = {118}, editor = {Schewe, Sven and Zhang, Lijun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.33}, URN = {urn:nbn:de:0030-drops-95711}, doi = {10.4230/LIPIcs.CONCUR.2018.33}, annote = {Keywords: population protocols, performance analysis, expected termination time} }

Document

**Published in:** LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

We study graphs and two-player games in which rewards are assigned to states, and the goal of the players is to satisfy or dissatisfy certain property of the generated outcome, given as a mean payoff property. Since the notion of mean-payoff does not reflect possible fluctuations from the mean-payoff along a run, we propose definitions and algorithms for capturing the stability of the system, and give algorithms for deciding if a given mean payoff and stability objective can be ensured in the system.

Tomas Brazdil, Vojtech Forejt, Antonin Kucera, and Petr Novotny. Stability in Graphs and Games. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 10:1-10:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{brazdil_et_al:LIPIcs.CONCUR.2016.10, author = {Brazdil, Tomas and Forejt, Vojtech and Kucera, Antonin and Novotny, Petr}, title = {{Stability in Graphs and Games}}, booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)}, pages = {10:1--10:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-017-0}, ISSN = {1868-8969}, year = {2016}, volume = {59}, editor = {Desharnais, Jos\'{e}e and Jagadeesan, Radha}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.10}, URN = {urn:nbn:de:0030-drops-61784}, doi = {10.4230/LIPIcs.CONCUR.2016.10}, annote = {Keywords: Games, Stability, Mean-Payoff, Window Objectives} }

Document

**Published in:** LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009)

We study continuous-time stochastic games with time-bounded
reachability objectives. We show that each vertex in such a game
has a \emph{value} (i.e., an equilibrium probability), and we
classify the conditions under which optimal strategies exist.
Finally, we show how to compute optimal strategies in finite uniform
games, and how to compute $\varepsilon$-optimal strategies in
finitely-branching games with bounded rates (for finite games, we
provide detailed complexity estimations).

Tomas Brazdil, Vojtech Forejt, Jan Krcal, Jan Kretinsky, and Antonin Kucera. Continuous-Time Stochastic Games with Time-Bounded Reachability. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 61-72, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{brazdil_et_al:LIPIcs.FSTTCS.2009.2307, author = {Brazdil, Tomas and Forejt, Vojtech and Krcal, Jan and Kretinsky, Jan and Kucera, Antonin}, title = {{Continuous-Time Stochastic Games with Time-Bounded Reachability}}, booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science}, pages = {61--72}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-13-2}, ISSN = {1868-8969}, year = {2009}, volume = {4}, editor = {Kannan, Ravi and Narayan Kumar, K.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2307}, URN = {urn:nbn:de:0030-drops-23077}, doi = {10.4230/LIPIcs.FSTTCS.2009.2307}, annote = {Keywords: Continuous time stochastic systems, time bounded reachability, stochastic games} }

Document

**Published in:** LIPIcs, Volume 3, 26th International Symposium on Theoretical Aspects of Computer Science (2009)

We consider a class of infinite-state stochastic games generated by stateless pushdown automata (or, equivalently, 1-exit recursive state machines), where the winning objective is specified by a regular set of target configurations and a qualitative probability constraint `${>}0$' or `${=}1$'. The goal of one player is to maximize the probability of reaching the target set so that the constraint is satisfied, while the other player aims at the opposite. We show that the winner in such games can be determined in $\textbf{NP} \cap \textbf{co-NP}$. Further, we prove that the winning regions for both players are regular, and we design algorithms which compute the associated finite-state automata. Finally, we show that winning strategies can be synthesized effectively.

Tomas Brazdil, Vaclav Brozek, Antonin Kucera, and Jan Obdrzalek. Qualitative Reachability in Stochastic BPA Games. In 26th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 3, pp. 207-218, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{brazdil_et_al:LIPIcs.STACS.2009.1837, author = {Brazdil, Tomas and Brozek, Vaclav and Kucera, Antonin and Obdrzalek, Jan}, title = {{Qualitative Reachability in Stochastic BPA Games}}, booktitle = {26th International Symposium on Theoretical Aspects of Computer Science}, pages = {207--218}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-09-5}, ISSN = {1868-8969}, year = {2009}, volume = {3}, editor = {Albers, Susanne and Marion, Jean-Yves}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2009.1837}, URN = {urn:nbn:de:0030-drops-18375}, doi = {10.4230/LIPIcs.STACS.2009.1837}, annote = {Keywords: Stochastic games, Reachability, Pushdown automata} }

Document

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

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.

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

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

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.

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} }

Document

**Published in:** LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Population protocols are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their states. Computations are infinite sequences of interactions in which the interacting devices are chosen uniformly at random.
In well designed population protocols, for every initial configuration of devices, and for every computation starting at this configuration, all devices eventually agree on a consensus value. We address the problem of automatically computing a parametric bound on the expected time the protocol needs to reach this consensus. We present the first algorithm that, when successful, outputs a function f(n) such that the expected time to consensus is bound by O(f(n)), where n is the number of devices executing the protocol. We experimentally show that our algorithm terminates and provides good bounds for many of the protocols found in the literature.

Michael Blondin, Javier Esparza, and Antonín Kucera. Automatic Analysis of Expected Termination Time for Population Protocols. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{blondin_et_al:LIPIcs.CONCUR.2018.33, author = {Blondin, Michael and Esparza, Javier and Kucera, Anton{\'\i}n}, title = {{Automatic Analysis of Expected Termination Time for Population Protocols}}, booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)}, pages = {33:1--33:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-087-3}, ISSN = {1868-8969}, year = {2018}, volume = {118}, editor = {Schewe, Sven and Zhang, Lijun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.33}, URN = {urn:nbn:de:0030-drops-95711}, doi = {10.4230/LIPIcs.CONCUR.2018.33}, annote = {Keywords: population protocols, performance analysis, expected termination time} }

Document

**Published in:** LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

We study graphs and two-player games in which rewards are assigned to states, and the goal of the players is to satisfy or dissatisfy certain property of the generated outcome, given as a mean payoff property. Since the notion of mean-payoff does not reflect possible fluctuations from the mean-payoff along a run, we propose definitions and algorithms for capturing the stability of the system, and give algorithms for deciding if a given mean payoff and stability objective can be ensured in the system.

Tomas Brazdil, Vojtech Forejt, Antonin Kucera, and Petr Novotny. Stability in Graphs and Games. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 10:1-10:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{brazdil_et_al:LIPIcs.CONCUR.2016.10, author = {Brazdil, Tomas and Forejt, Vojtech and Kucera, Antonin and Novotny, Petr}, title = {{Stability in Graphs and Games}}, booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)}, pages = {10:1--10:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-017-0}, ISSN = {1868-8969}, year = {2016}, volume = {59}, editor = {Desharnais, Jos\'{e}e and Jagadeesan, Radha}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.10}, URN = {urn:nbn:de:0030-drops-61784}, doi = {10.4230/LIPIcs.CONCUR.2016.10}, annote = {Keywords: Games, Stability, Mean-Payoff, Window Objectives} }

Document

**Published in:** LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009)

We study continuous-time stochastic games with time-bounded
reachability objectives. We show that each vertex in such a game
has a \emph{value} (i.e., an equilibrium probability), and we
classify the conditions under which optimal strategies exist.
Finally, we show how to compute optimal strategies in finite uniform
games, and how to compute $\varepsilon$-optimal strategies in
finitely-branching games with bounded rates (for finite games, we
provide detailed complexity estimations).

Tomas Brazdil, Vojtech Forejt, Jan Krcal, Jan Kretinsky, and Antonin Kucera. Continuous-Time Stochastic Games with Time-Bounded Reachability. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 61-72, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{brazdil_et_al:LIPIcs.FSTTCS.2009.2307, author = {Brazdil, Tomas and Forejt, Vojtech and Krcal, Jan and Kretinsky, Jan and Kucera, Antonin}, title = {{Continuous-Time Stochastic Games with Time-Bounded Reachability}}, booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science}, pages = {61--72}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-13-2}, ISSN = {1868-8969}, year = {2009}, volume = {4}, editor = {Kannan, Ravi and Narayan Kumar, K.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2307}, URN = {urn:nbn:de:0030-drops-23077}, doi = {10.4230/LIPIcs.FSTTCS.2009.2307}, annote = {Keywords: Continuous time stochastic systems, time bounded reachability, stochastic games} }

Document

**Published in:** LIPIcs, Volume 3, 26th International Symposium on Theoretical Aspects of Computer Science (2009)

We consider a class of infinite-state stochastic games generated by stateless pushdown automata (or, equivalently, 1-exit recursive state machines), where the winning objective is specified by a regular set of target configurations and a qualitative probability constraint `${>}0$' or `${=}1$'. The goal of one player is to maximize the probability of reaching the target set so that the constraint is satisfied, while the other player aims at the opposite. We show that the winner in such games can be determined in $\textbf{NP} \cap \textbf{co-NP}$. Further, we prove that the winning regions for both players are regular, and we design algorithms which compute the associated finite-state automata. Finally, we show that winning strategies can be synthesized effectively.

Tomas Brazdil, Vaclav Brozek, Antonin Kucera, and Jan Obdrzalek. Qualitative Reachability in Stochastic BPA Games. In 26th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 3, pp. 207-218, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{brazdil_et_al:LIPIcs.STACS.2009.1837, author = {Brazdil, Tomas and Brozek, Vaclav and Kucera, Antonin and Obdrzalek, Jan}, title = {{Qualitative Reachability in Stochastic BPA Games}}, booktitle = {26th International Symposium on Theoretical Aspects of Computer Science}, pages = {207--218}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-09-5}, ISSN = {1868-8969}, year = {2009}, volume = {3}, editor = {Albers, Susanne and Marion, Jean-Yves}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2009.1837}, URN = {urn:nbn:de:0030-drops-18375}, doi = {10.4230/LIPIcs.STACS.2009.1837}, annote = {Keywords: Stochastic games, Reachability, Pushdown automata} }

Document

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

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.

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

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

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.

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} }

Document

**Published in:** LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Population protocols are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their states. Computations are infinite sequences of interactions in which the interacting devices are chosen uniformly at random.
In well designed population protocols, for every initial configuration of devices, and for every computation starting at this configuration, all devices eventually agree on a consensus value. We address the problem of automatically computing a parametric bound on the expected time the protocol needs to reach this consensus. We present the first algorithm that, when successful, outputs a function f(n) such that the expected time to consensus is bound by O(f(n)), where n is the number of devices executing the protocol. We experimentally show that our algorithm terminates and provides good bounds for many of the protocols found in the literature.

Michael Blondin, Javier Esparza, and Antonín Kucera. Automatic Analysis of Expected Termination Time for Population Protocols. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{blondin_et_al:LIPIcs.CONCUR.2018.33, author = {Blondin, Michael and Esparza, Javier and Kucera, Anton{\'\i}n}, title = {{Automatic Analysis of Expected Termination Time for Population Protocols}}, booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)}, pages = {33:1--33:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-087-3}, ISSN = {1868-8969}, year = {2018}, volume = {118}, editor = {Schewe, Sven and Zhang, Lijun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.33}, URN = {urn:nbn:de:0030-drops-95711}, doi = {10.4230/LIPIcs.CONCUR.2018.33}, annote = {Keywords: population protocols, performance analysis, expected termination time} }

Document

**Published in:** LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

We study graphs and two-player games in which rewards are assigned to states, and the goal of the players is to satisfy or dissatisfy certain property of the generated outcome, given as a mean payoff property. Since the notion of mean-payoff does not reflect possible fluctuations from the mean-payoff along a run, we propose definitions and algorithms for capturing the stability of the system, and give algorithms for deciding if a given mean payoff and stability objective can be ensured in the system.

Tomas Brazdil, Vojtech Forejt, Antonin Kucera, and Petr Novotny. Stability in Graphs and Games. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 10:1-10:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{brazdil_et_al:LIPIcs.CONCUR.2016.10, author = {Brazdil, Tomas and Forejt, Vojtech and Kucera, Antonin and Novotny, Petr}, title = {{Stability in Graphs and Games}}, booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)}, pages = {10:1--10:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-017-0}, ISSN = {1868-8969}, year = {2016}, volume = {59}, editor = {Desharnais, Jos\'{e}e and Jagadeesan, Radha}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.10}, URN = {urn:nbn:de:0030-drops-61784}, doi = {10.4230/LIPIcs.CONCUR.2016.10}, annote = {Keywords: Games, Stability, Mean-Payoff, Window Objectives} }

Document

**Published in:** LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009)

We study continuous-time stochastic games with time-bounded
reachability objectives. We show that each vertex in such a game
has a \emph{value} (i.e., an equilibrium probability), and we
classify the conditions under which optimal strategies exist.
Finally, we show how to compute optimal strategies in finite uniform
games, and how to compute $\varepsilon$-optimal strategies in
finitely-branching games with bounded rates (for finite games, we
provide detailed complexity estimations).

Tomas Brazdil, Vojtech Forejt, Jan Krcal, Jan Kretinsky, and Antonin Kucera. Continuous-Time Stochastic Games with Time-Bounded Reachability. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 61-72, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{brazdil_et_al:LIPIcs.FSTTCS.2009.2307, author = {Brazdil, Tomas and Forejt, Vojtech and Krcal, Jan and Kretinsky, Jan and Kucera, Antonin}, title = {{Continuous-Time Stochastic Games with Time-Bounded Reachability}}, booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science}, pages = {61--72}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-13-2}, ISSN = {1868-8969}, year = {2009}, volume = {4}, editor = {Kannan, Ravi and Narayan Kumar, K.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2307}, URN = {urn:nbn:de:0030-drops-23077}, doi = {10.4230/LIPIcs.FSTTCS.2009.2307}, annote = {Keywords: Continuous time stochastic systems, time bounded reachability, stochastic games} }

Document

**Published in:** LIPIcs, Volume 3, 26th International Symposium on Theoretical Aspects of Computer Science (2009)

We consider a class of infinite-state stochastic games generated by stateless pushdown automata (or, equivalently, 1-exit recursive state machines), where the winning objective is specified by a regular set of target configurations and a qualitative probability constraint `${>}0$' or `${=}1$'. The goal of one player is to maximize the probability of reaching the target set so that the constraint is satisfied, while the other player aims at the opposite. We show that the winner in such games can be determined in $\textbf{NP} \cap \textbf{co-NP}$. Further, we prove that the winning regions for both players are regular, and we design algorithms which compute the associated finite-state automata. Finally, we show that winning strategies can be synthesized effectively.

Tomas Brazdil, Vaclav Brozek, Antonin Kucera, and Jan Obdrzalek. Qualitative Reachability in Stochastic BPA Games. In 26th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 3, pp. 207-218, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{brazdil_et_al:LIPIcs.STACS.2009.1837, author = {Brazdil, Tomas and Brozek, Vaclav and Kucera, Antonin and Obdrzalek, Jan}, title = {{Qualitative Reachability in Stochastic BPA Games}}, booktitle = {26th International Symposium on Theoretical Aspects of Computer Science}, pages = {207--218}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-09-5}, ISSN = {1868-8969}, year = {2009}, volume = {3}, editor = {Albers, Susanne and Marion, Jean-Yves}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2009.1837}, URN = {urn:nbn:de:0030-drops-18375}, doi = {10.4230/LIPIcs.STACS.2009.1837}, annote = {Keywords: Stochastic games, Reachability, Pushdown automata} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail