




Publications  Efficient Analysis of Probabilistic Programs with an Unbounded Counter





Reference:
Tomáš Brázdil, Stefan Kiefer, and Antonín Kučera. Efficient analysis of probabilistic programs with an unbounded counter. Technical report, arXiv.org, April 2011. Available at http://arxiv.org/abs/1102.2529.
Abstract:
We show that a subclass of infinitestate probabilistic programs that can be modeled by probabilistic onecounter 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 omegaregular property. Further, our results establish 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 nontermination probability in pOC away from zero.
Suggested BibTeX entry:
@techreport{BKK:CAV11TR,
author = {Tom\'{a}\v{s} Br\'{a}zdil and Stefan Kiefer and Anton\'{\i}n Ku\v{c}era},
institution = {arXiv.org},
month = {April},
note = {Available at http://arxiv.org/abs/1102.2529},
title = {Efficient Analysis of Probabilistic Programs with an Unbounded Counter},
year = {2011}
}




