Efficient Analysis of Probabilistic Programs with an Unbounded Counter
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F14%3A00074284" target="_blank" >RIV/00216224:14330/14:00074284 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1145/2629599" target="_blank" >http://dx.doi.org/10.1145/2629599</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1145/2629599" target="_blank" >10.1145/2629599</a>
Alternative languages
Result language
angličtina
Original language name
Efficient Analysis of Probabilistic Programs with an Unbounded Counter
Original language description
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, whichleads 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.
Czech name
—
Czech description
—
Classification
Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Center of excellence - Institute for theoretical computer science (CE-ITI)</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2014
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
Journal of the ACM
ISSN
0004-5411
e-ISSN
—
Volume of the periodical
61
Issue of the periodical within the volume
6
Country of publishing house
US - UNITED STATES
Number of pages
35
Pages from-to
1-35
UT code for WoS article
000347051200008
EID of the result in the Scopus database
—