{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:49:19Z","timestamp":1775868559675,"version":"3.50.1"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["389792660 TRR 248"],"award-info":[{"award-number":["389792660 TRR 248"]}],"id":[{"id":"10.13039\/501100001659","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":[[2025,1,7]]},"abstract":"<jats:p>Deciding termination is a fundamental problem in the analysis of probabilistic imperative programs. We consider the qualitative and quantitative probabilistic termination problems for an imperative programming model with discrete probabilistic choice and demonic bounded nondeterminism. The qualitative question asks if the program terminates almost-surely, no matter how nondeterminism is resolved. The quantitative question asks for a bound on the probability of termination. Despite a long and rich literature on the topic, no sound and relatively complete proof systems were known for these problems. In this paper, we provide sound and relatively complete proof rules for proving qualitative and quantitative termination in the assertion language of arithmetic. Our rules use variant functions as measures of distances to termination as well as supermartingales that restrain the growth of these variants almost-surely. Our completeness result shows how to construct suitable supermartingale and variant functions from an almost-surely terminating program. We also show that proofs of termination in many existing proof systems can be transformed to proofs in our system, pointing to its applicability in practice. As an application of our proof rule, we show an explicit proof of almost-sure termination for the two-dimensional random walker.<\/jats:p>","DOI":"10.1145\/3704899","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1871-1902","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Sound and Complete Proof Rules for Probabilistic Termination"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2136-0542","authenticated-orcid":false,"given":"Rupak","family":"Majumdar","sequence":"first","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-5187-5415","authenticated-orcid":false,"given":"V.R.","family":"Sathiyanarayana","sequence":"additional","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/357146.357150"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(86)90071-2"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/6490.6494"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2019.102338"},{"key":"e_1_3_2_6_2","volume-title":"Principles of model checking","author":"Baier Christel","year":"2008","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. MIT Press."},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_3"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434320"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60692-0_70"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_24"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_4"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009873"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1137\/0207005"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/210332.210339"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855763"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2007.07.008"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1142\/S012905410200114X"},{"key":"e_1_3_2_19_2","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","year":"1976","unstructured":"Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall. https:\/\/www.worldcat.org\/oclc\/01958445"},{"key":"e_1_3_2_20_2","volume-title":"Stochastic processes","author":"Doob J. L.","year":"1953","unstructured":"J. L. Doob. 1953. Stochastic processes. John Wiley & Sons, New York. viii+654 pages. MR 15,445b. Zbl 0053.26802."},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3586051"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611973082.15"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-1793-7_4"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100026396"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177728976"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-11245-5_22"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90005-5"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/2166.357214"},{"key":"e_1_3_2_31_2","first-page":"225","volume-title":"Automata, Languages and Programming, Colloquium, Paris, France, July 3-7, 1972","author":"Hitchcock Peter","year":"1972","unstructured":"Peter Hitchcock and David Michael Ritchie Park. 1972. Induction Rules and Termination Proofs. In Automata, Languages and Programming, Colloquium, Paris, France, July 3-7, 1972, Maurice Nivat (Ed.). North-Holland, Amsterdam, 225\u2013251."},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_11"},{"key":"e_1_3_2_33_2","unstructured":"Benjamin Lucien Kaminski. 2019. Advanced weakest precondition calculi for probabilistic programs. Ph.D. Dissertation. RWTH Aachen University Germany. http:\/\/publications.rwth-aachen.de\/record\/755408"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-018-0321-1"},{"key":"e_1_3_2_35_2","unstructured":"Joost-Pieter Katoen. 2023. Verifying Probabilistic Programs: From Theory to Automation. (2023). https:\/\/etaps.org\/2023\/speakers\/joost-pieter-katoen\/ ETAPS International Joint Conferences On Theory & Practice Of Software (2023)."},{"issue":"4","key":"e_1_3_2_36_2","article-title":"On the Termination Problem for Probabilistic Higher-Order Recursive Programs","volume":"16","author":"Kobayashi Naoki","year":"2020","unstructured":"Naoki Kobayashi, Ugo Dal Lago, and Charles Grellois. 2020. On the Termination Problem for Probabilistic Higher-Order Recursive Programs. Log. Methods Comput. Sci. 16, 4 (2020). https:\/\/lmcs.episciences.org\/6817","journal-title":"Log. Methods Comput. Sci"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","unstructured":"Dexter Kozen. 2006. Theory of Computation. Springer. https:\/\/doi.org\/10.1007\/1-84628-477-5 10.1007\/1-84628-477-5","DOI":"10.1007\/1-84628-477-5"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2310.16145"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632879"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00288637"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/B138392"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"e_1_3_2_43_2","volume-title":"Non-homogeneous random walks: Lyapunov function methods for near critical stochastic systems","author":"Menshikov Mikhail","year":"2017","unstructured":"Mikhail Menshikov, Serguei Popov, and Andrew Wade. 2017. Non-homogeneous random walks: Lyapunov function methods for near critical stochastic systems. Cambridge University Press."},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.2307\/3213440"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47764-0_7"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_26"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01458701"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","unstructured":"Serguei Popov. 2021. Two-Dimensional Random Walk: From Path Counting to Random Interlacements. Cambridge University Press. https:\/\/doi.org\/10.1017\/9781108680134 10.1017\/9781108680134","DOI":"10.1017\/9781108680134"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.2307\/2266510"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.5555\/28907"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31933-4"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/3450967"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1112\/PLMS\/S2-42.1.230"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1985.12"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454110"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704899","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704899","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:16:12Z","timestamp":1770200172000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704899"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":54,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704899"],"URL":"https:\/\/doi.org\/10.1145\/3704899","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}