J 2014

Efficient Analysis of Probabilistic Programs with an Unbounded Counter

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

Základní údaje

Originální název

Efficient Analysis of Probabilistic Programs with an Unbounded Counter

Autoři

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

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/14:00074284

Organizační jednotka

Fakulta informatiky

DOI

UT WoS

EID Scopus

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
Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)
Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky