Efficient Analysis of Probabilistic Programs with an Unbounded Counter

Logo poskytovatele

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

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

Rok publikování 2014
Druh Článek v odborném periodiku
Časopis / Zdroj Journal of the ACM
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1145/2629599
Obor Informatika
Klíčová slova Markov chains; model-checking; one-counter automata
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.