BRÁZDIL, Tomáš, Stefan KIEFER a Antonín KUČERA. Efficient Analysis of Probabilistic Programs with an Unbounded Counter. Journal of the ACM, New York, NY, USA: ACM, 2014, roč. 61, č. 6, s. 1-35. ISSN 0004-5411. doi:10.1145/2629599.
Další formáty:   BibTeX LaTeX RIS
Zá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
Originální jazyk angličtina
Typ výsledku Článek v odborném periodiku
Obor Computer sciences, information science, bioinformatics
Stát vydavatele Spojené státy americké
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
Doi http://dx.doi.org/10.1145/2629599
UT WoS 000347051200008
Klíčová slova anglicky Markov chains; model-checking; one-counter automata
Štítky formela-journal
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 27. 4. 2015 04:52.
Anotace
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 VaVNázev: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)
Investor: Grantová agentura ČR, Projekty na podporu excelence v základním výzkumu
VytisknoutZobrazeno: 16. 10. 2019 20:16