{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,29]],"date-time":"2026-07-29T05:55:48Z","timestamp":1785304548657,"version":"3.55.0"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2014,12,17]],"date-time":"2014-12-17T00:00:00Z","timestamp":1418774400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Institute for Theoretical Computer Science","award":["P202\/12\/G061"],"award-info":[{"award-number":["P202\/12\/G061"]}]},{"DOI":"10.13039\/501100000288","name":"Royal Society","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000288","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2014,12,17]]},"abstract":"<jats:p>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 \u201cdivergence gap theorem\u201d, 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 \u03c9-regular property encoded by a deterministic Rabin automaton.<\/jats:p>","DOI":"10.1145\/2629599","type":"journal-article","created":{"date-parts":[[2014,12,19]],"date-time":"2014-12-19T13:38:51Z","timestamp":1418996331000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Efficient Analysis of Probabilistic Programs with an Unbounded Counter"],"prefix":"10.1145","volume":"61","author":[{"given":"Tom\u00e1s","family":"Br\u00e1zdil","sequence":"first","affiliation":[{"name":"Masaryk University, Czech Republic"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stefan","family":"Kiefer","sequence":"additional","affiliation":[{"name":"University of Oxford, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anton\u00edn","family":"K\u016dcera","sequence":"additional","affiliation":[{"name":"Masaryk University, Czech Republic"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2014,12,17]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1137\/070697926"},{"key":"e_1_2_1_2_1","unstructured":"P. Billingsley. 1995. Probability and Measure. Wiley.  P. Billingsley. 1995. Probability and Measure. Wiley."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89439-1_17"},{"key":"e_1_2_1_4_1","volume-title":"Leibniz International Proceedings in Informatics","volume":"8","author":"Br\u00e1zdil T."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/2027223.2027256"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of SODA'10","author":"Br\u00e1zdil T."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0166-0"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.2005.19"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032323"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31585-5_16"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31856-9_12"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/62212.62257"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1880999.1881064"},{"key":"e_1_2_1_14_1","volume-title":"Leibniz International Proceedings in Informatics Series","volume":"8","author":"Chatterjee K.","year":"2010"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734087"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021838"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.39"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2008.35"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2009.12.009"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_17"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2005.8"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31856-9_28"},{"key":"e_1_2_1_23_1","unstructured":"J. Hopcroft and J. Ullman. 1979. Introduction to Automata Theory Languages and Computation. Addison-Wesley.   J. Hopcroft and J. Ullman. 1979. Introduction to Automata Theory Languages and Computation. Addison-Wesley."},{"key":"e_1_2_1_24_1","unstructured":"E. Isaacson and H. B. Keller. 1966. Analysis of Numerical Methods. Wiley.  E. Isaacson and H. B. Keller. 1966. Analysis of Numerical Methods. Wiley."},{"key":"e_1_2_1_25_1","unstructured":"J. Kemeny and J. Snell. 1960. Finite Markov chains. D. Van Nostrand Company.  J. Kemeny and J. Snell. 1960. Finite Markov chains. D. Van Nostrand Company."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250790.1250822"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of ATVA'13","volume":"8172","author":"K\u0159et\u00ednsk\u00fd J."},{"key":"e_1_2_1_28_1","unstructured":"M. Neuts. 1981. Matrix-geometric Solutions in Stochastic Models: An Algorithmic Approach. Courier Dover Publications.  M. Neuts. 1981. Matrix-geometric Solutions in Stochastic Models: An Algorithmic Approach. Courier Dover Publications."},{"key":"e_1_2_1_29_1","doi-asserted-by":"crossref","unstructured":"J. Rosenthal. 2006. A First Look at Rigorous Probability Theory. World Scientific Publishing.  J. Rosenthal. 2006. A First Look at Rigorous Probability Theory. World Scientific Publishing.","DOI":"10.1142\/6300"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_33"},{"key":"e_1_2_1_31_1","unstructured":"W. Thomas. 1991. Automata on infinite objects. Handbook of Theoretical Computer Science B 135--192.  W. Thomas. 1991. Automata on infinite objects. Handbook of Theoretical Computer Science B 135--192."},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"D. Williams. 1991. Probability with Martingales. Cambridge University Press.  D. Williams. 1991. Probability with Martingales. Cambridge University Press.","DOI":"10.1017\/CBO9780511813658"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2629599","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2629599","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:13:29Z","timestamp":1750227209000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2629599"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,12,17]]},"references-count":32,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2014,12,17]]}},"alternative-id":["10.1145\/2629599"],"URL":"https:\/\/doi.org\/10.1145\/2629599","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,12,17]]},"assertion":[{"value":"2012-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-12-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}