| BRÁZDIL, Tomáš, Stefan KIEFER and Antonín KUČERA. Efficient Analysis of Probabilistic Programs with an Unbounded Counter. Journal of the ACM. New York, NY, USA: ACM, 2014, vol. 61, No 6, p. 1-35. ISSN 0004-5411. Available from: https://dx.doi.org/10.1145/2629599. |
Other formats:
BibTeX
LaTeX
RIS
@article{1215263,
author = {Brázdil, Tomáš and Kiefer, Stefan and Kučera, Antonín},
article_location = {New York, NY, USA},
article_number = {6},
doi = {http://dx.doi.org/10.1145/2629599},
keywords = {Markov chains; model-checking; one-counter automata},
language = {eng},
issn = {0004-5411},
journal = {Journal of the ACM},
title = {Efficient Analysis of Probabilistic Programs with an Unbounded Counter},
volume = {61},
year = {2014}
}
TY - JOUR
ID - 1215263
AU - Brázdil, Tomáš - Kiefer, Stefan - Kučera, Antonín
PY - 2014
TI - Efficient Analysis of Probabilistic Programs with an Unbounded Counter
JF - Journal of the ACM
VL - 61
IS - 6
SP - 1-35
EP - 1-35
PB - ACM
SN - 00045411
KW - Markov chains
KW - model-checking
KW - one-counter automata
N2 - 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. We start by establishing a powerful link between pOC and martingale theory, which leads to fundamental observations about quantitative properties of runs in pOC. In particular, we provide a “divergence gap theorem”, which bounds a positive non-termination probability in pOC away from zero. Using these observations, we show that the expected termination time can be approximated up to an arbitrarily small relative error in polynomial time, and the same holds for the probability of all runs that satisfy a given omega-regular property encoded by a deterministic Rabin automaton.
ER -
BRÁZDIL, Tomáš, Stefan KIEFER and Antonín KUČERA. Efficient Analysis of Probabilistic Programs with an Unbounded Counter. \textit{Journal of the ACM}. New York, NY, USA: ACM, 2014, vol.~61, No~6, p.~1-35. ISSN~0004-5411. Available from: https://dx.doi.org/10.1145/2629599.
|
