2014
Efficient Analysis of Probabilistic Programs with an Unbounded Counter
BRÁZDIL, Tomáš, Stefan KIEFER a Antonín KUČERAZákladní údaje
Originální název
Efficient Analysis of Probabilistic Programs with an Unbounded Counter
Autoři
BRÁZDIL, Tomáš (203 Česká republika, garant, domácí), Stefan KIEFER (276 Německo) a Antonín KUČERA (203 Česká republika, domácí)
Vydání
Journal of the ACM, New York, NY, USA, ACM, 2014, 0004-5411
Další údaje
Jazyk
angličtina
Typ výsledku
Článek v odborném periodiku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Spojené státy
Utajení
není předmětem státního či obchodního tajemství
Impakt faktor
Impact factor: 1.394
Kód RIV
RIV/00216224:14330/14:00074284
Organizační jednotka
Fakulta informatiky
UT WoS
000347051200008
Klíčová slova anglicky
Markov chains; model-checking; one-counter automata
Štítky
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 27. 4. 2015 04:52, RNDr. Pavel Šmerk, Ph.D.
Anotace
V originále
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.
Návaznosti
| GBP202/12/G061, projekt VaV |
|