Efficient Analysis of Probabilistic Programs with an Unbounded Counter

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BRÁZDIL Tomáš KIEFER Stefan KUČERA Antonín

Year of publication 2011
Type Article in Proceedings
Conference Computer Aided Verification, 23rd International Conference, CAV 2011
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-642-22110-1
Field Informatics
Keywords one-counter machines; probabilistic systems; model-checking
Description We show that a subclass of infinite-state probabilistic programs that can be modeled by probabilistic one-counter automata (pOC) admits an efficient quantitative analysis. In particular, we show that the expected termination time can be approximated up to an arbitrarily small relative error with polynomially many arithmetic operations, and the same holds for the probability of all runs that satisfy a given omega-regular property.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.