Efficient Analysis of Probabilistic Programs with an Unbounded Counter

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

Efficient Analysis of Probabilistic Programs with an Unbounded Counter

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Efficient Analysis of Probabilistic Programs with an Unbounded Counter

Popis výsledku anglicky

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.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Centrum excelence - Institut teoretické informatiky (CE-ITI)</a><br>

Návaznosti

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

Rok uplatnění

2014

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Journal of the ACM

ISSN

0004-5411

e-ISSN

—

Svazek periodika

61

Číslo periodika v rámci svazku

6

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

35

Strana od-do

1-35

Kód UT WoS článku

000347051200008

EID výsledku v databázi Scopus

—