Attributes | Values |
---|
rdf:type
| |
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, 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.
- 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. (en)
|
Title
| - Efficient Analysis of Probabilistic Programs with an Unbounded Counter
- Efficient Analysis of Probabilistic Programs with an Unbounded Counter (en)
|
skos:prefLabel
| - Efficient Analysis of Probabilistic Programs with an Unbounded Counter
- Efficient Analysis of Probabilistic Programs with an Unbounded Counter (en)
|
skos:notation
| - RIV/00216224:14330/14:00074284!RIV15-MSM-14330___
|
http://linked.open...avai/riv/aktivita
| |
http://linked.open...avai/riv/aktivity
| |
http://linked.open...iv/cisloPeriodika
| |
http://linked.open...vai/riv/dodaniDat
| |
http://linked.open...aciTvurceVysledku
| |
http://linked.open.../riv/druhVysledku
| |
http://linked.open...iv/duvernostUdaju
| |
http://linked.open...titaPredkladatele
| |
http://linked.open...dnocenehoVysledku
| |
http://linked.open...ai/riv/idVysledku
| - RIV/00216224:14330/14:00074284
|
http://linked.open...riv/jazykVysledku
| |
http://linked.open.../riv/klicovaSlova
| - Markov chains; model-checking; one-counter automata (en)
|
http://linked.open.../riv/klicoveSlovo
| |
http://linked.open...odStatuVydavatele
| - US - Spojené státy americké
|
http://linked.open...ontrolniKodProRIV
| |
http://linked.open...i/riv/nazevZdroje
| |
http://linked.open...in/vavai/riv/obor
| |
http://linked.open...ichTvurcuVysledku
| |
http://linked.open...cetTvurcuVysledku
| |
http://linked.open...vavai/riv/projekt
| |
http://linked.open...UplatneniVysledku
| |
http://linked.open...v/svazekPeriodika
| |
http://linked.open...iv/tvurceVysledku
| - Brázdil, Tomáš
- Kučera, Antonín
- Kiefer, Stefan
|
http://linked.open...ain/vavai/riv/wos
| |
issn
| |
number of pages
| |
http://bibframe.org/vocab/doi
| |
http://localhost/t...ganizacniJednotka
| |