BRÁZDIL, Tomáš, Stefan KIEFER and Antonín KUČERA. Efficient Analysis of Probabilistic Programs with an Unbounded Counter. In Ganesh Gopalakrishnan, Shaz Qadeer. Computer Aided Verification, 23rd International Conference, CAV 2011. Berlin: Springer, 2011, p. 208-224. ISBN 978-3-642-22109-5. Available from: https://dx.doi.org/10.1007/978-3-642-22110-1.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Efficient Analysis of Probabilistic Programs with an Unbounded Counter
Authors BRÁZDIL, Tomáš (203 Czech Republic, belonging to the institution), Stefan KIEFER (276 Germany) and Antonín KUČERA (203 Czech Republic, guarantor, belonging to the institution).
Edition Berlin, Computer Aided Verification, 23rd International Conference, CAV 2011, p. 208-224, 17 pp. 2011.
Publisher Springer
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Germany
Confidentiality degree is not subject to a state or trade secret
RIV identification code RIV/00216224:14330/11:00054480
Organization unit Faculty of Informatics
ISBN 978-3-642-22109-5
Doi http://dx.doi.org/10.1007/978-3-642-22110-1
UT WoS 000347051200008
Keywords in English one-counter machines; probabilistic systems; model-checking
Tags International impact, Reviewed
Changed by Changed by: prof. RNDr. Antonín Kučera, Ph.D., učo 2508. Changed: 17/12/2011 17:01.
Abstract
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.
Abstract (in Czech)
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ů.
Links
P202/10/1469, interní kód MUName: Formální metody pro analýzu a verifikaci komplexních systémů
1M0545, research and development projectName: Institut Teoretické Informatiky
Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science
PrintDisplayed: 29/8/2024 11:11