D 2011

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í

Berlin, Computer Aided Verification, 23rd International Conference, CAV 2011, od s. 208-224, 17 s. 2011

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/11:00054480

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-22109-5

Klíčová slova anglicky

one-counter machines; probabilistic systems; model-checking

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 17. 12. 2011 17:01, prof. RNDr. Antonín Kučera, 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. In particular, we show that the expected termination time can be approximated up to an arbitrarily small relative error with polynomially many arithmetic operations, and the same holds for the probability of all runs that satisfy a given omega-regular property.

Česky

V článku je dokázáno, že kvantitativní analýzu nekonečně-stavových programů popsatelných automatem s jedním čítačem lze provádět algoritmicky a efektivně. Zejména je možné aproximovat střední čas ukončení těchto programů.

Návaznosti

P202/10/1469, interní kód MU
Název: Formální metody pro analýzu a verifikaci komplexních systémů
1M0545, projekt VaV
Název: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky