{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,24]],"date-time":"2026-03-24T05:59:56Z","timestamp":1774331996632,"version":"3.50.1"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","award":["DP140101119"],"award-info":[{"award-number":["DP140101119"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>We present a new proof rule for proving almost-sure termination of probabilistic programs, including those that contain demonic non-determinism.<\/jats:p>\n          <jats:p>An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates \"almost surely\". Proving that can be hard, and this paper presents a new method for doing so. It applies directly to the program's source code, even if the program contains demonic choice.<\/jats:p>\n          <jats:p>Like others, we use variant functions (a.k.a. \"super-martingales\") that are real-valued and decrease randomly on each loop iteration; but our key innovation is that the amount as well as the probability of the decrease are parametric. We prove the soundness of the new rule, indicate where its applicability goes beyond existing rules, and explain its connection to classical results on denumerable (non-demonic) Markov chains.<\/jats:p>","DOI":"10.1145\/3158121","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":77,"title":["A new proof rule for almost-sure termination"],"prefix":"10.1145","volume":"2","author":[{"given":"Annabelle","family":"McIver","sequence":"first","affiliation":[{"name":"Macquarie University, Australia"}]},{"given":"Carroll","family":"Morgan","sequence":"additional","affiliation":[{"name":"UNSW, Australia \/ Data61 at CSIRO, Australia"}]},{"given":"Benjamin Lucien","family":"Kaminski","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany \/ University College London, UK"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany \/ IST Austria, Austria"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158122"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177728425"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11526841_9"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958114"},{"key":"e_1_2_2_6_1","volume-title":"Termination of Nondeterministic Recursive Probabilistic Programs. CoRR abs\/1701.02944","author":"Chatterjee Krishnendu","year":"2017","unstructured":"Krishnendu Chatterjee and Hongfei Fu. 2017. Termination of Nondeterministic Recursive Probabilistic Programs. CoRR abs\/1701.02944 ( 2017 ). Krishnendu Chatterjee and Hongfei Fu. 2017. Termination of Nondeterministic Recursive Probabilistic Programs. CoRR abs\/1701.02944 (2017)."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009873"},{"key":"e_1_2_2_8_1","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","unstructured":"Edsger W. Dijkstra . 1976. A Discipline of Programming . Prentice-Hall . Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_14"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100026396"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100076362"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2013.11.004"},{"key":"e_1_2_2_14_1","unstructured":"G.R. Grimmett and D. Welsh. 1986. Probability: an Introduction. Oxford Science Publications.  G.R. Grimmett and D. Welsh. 1986. Probability: an Introduction. Oxford Science Publications."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2166.357214"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100027055"},{"key":"e_1_2_2_19_1","volume-title":"Theory and Application of Infinite Series","author":"Knopp Konrad","unstructured":"Konrad Knopp . 1928. Theory and Application of Infinite Series . London . Konrad Knopp. 1928. Theory and Application of Infinite Series. London."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_15"},{"key":"e_1_2_2_22_1","volume-title":"Refinement and Proof for Probabilistic Systems","author":"McIver Annabelle","unstructured":"Annabelle McIver and Carroll Morgan . 2005. Abstraction , Refinement and Proof for Probabilistic Systems . Springer . Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement and Proof for Probabilistic Systems. Springer."},{"key":"e_1_2_2_23_1","volume-title":"A New Rule for Almost-Certain Termination of Probabilistic and Demonic Programs. CoRR abs\/1612.01091","author":"McIver Annabelle","year":"2016","unstructured":"Annabelle McIver and Carroll Morgan . 2016. A New Rule for Almost-Certain Termination of Probabilistic and Demonic Programs. CoRR abs\/1612.01091 ( 2016 ). Annabelle McIver and Carroll Morgan. 2016. A New Rule for Almost-Certain Termination of Probabilistic and Demonic Programs. CoRR abs\/1612.01091 (2016)."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.14236\/ewic\/RW1996.10"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158121","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158121","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158121"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":25,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158121"],"URL":"https:\/\/doi.org\/10.1145\/3158121","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}