{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:09:59Z","timestamp":1775790599556,"version":"3.50.1"},"reference-count":60,"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\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S11407-N23"],"award-info":[{"award-number":["S11407-N23"]}],"id":[{"id":"10.13039\/501100002428","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>Probabilistic programs extend classical imperative programs with real-valued random variables and random branching. The most basic liveness property for such programs is the termination property. The qualitative (aka almost-sure) termination problem asks whether a given program program terminates with probability 1. While ranking functions provide a sound and complete method for non-probabilistic programs, the extension of them to probabilistic programs is achieved via ranking supermartingales (RSMs). Although deep theoretical results have been established about RSMs, their application to probabilistic programs with nondeterminism has been limited only to programs of restricted control-flow structure. For non-probabilistic programs, lexicographic ranking functions provide a compositional and practical approach for termination analysis of real-world programs. In this work we introduce lexicographic RSMs and show that they present a sound method for almost-sure termination of probabilistic programs with nondeterminism. We show that lexicographic RSMs provide a tool for compositional reasoning about almost-sure termination, and for probabilistic programs with linear arithmetic they can be synthesized efficiently (in polynomial time). We also show that with additional restrictions even asymptotic bounds on expected termination time can be obtained through lexicographic RSMs. Finally, we present experimental results on benchmarks adapted from previous work to demonstrate the effectiveness of our approach.<\/jats:p>","DOI":"10.1145\/3158122","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":54,"title":["Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs"],"prefix":"10.1145","volume":"2","author":[{"given":"Sheshansh","family":"Agrawal","sequence":"first","affiliation":[{"name":"IIT Bombay, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Krishnendu","family":"Chatterjee","sequence":"additional","affiliation":[{"name":"IST Austria, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petr","family":"Novotn\u00fd","sequence":"additional","affiliation":[{"name":"IST Austria, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"2010. IBM ILOG CPLEX Optimizer. http:\/\/www-01.ibm.com\/software\/integration\/optimization\/cplex-optimizer\/.  2010. IBM ILOG CPLEX Optimizer. http:\/\/www-01.ibm.com\/software\/integration\/optimization\/cplex-optimizer\/."},{"key":"e_1_2_2_2_1","volume-title":"Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs. CoRR abs\/1709.04037","author":"Agrawal Sheshansh","year":"2017","unstructured":"Sheshansh Agrawal , Krishnendu Chatterjee , and Petr Novotn\u00fd . 2017. Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs. CoRR abs\/1709.04037 ( 2017 ). http:\/\/arxiv.org\/abs\/1709.04037 Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotn\u00fd. 2017. Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs. CoRR abs\/1709.04037 (2017). http:\/\/arxiv.org\/abs\/1709.04037"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_8"},{"key":"e_1_2_2_4_1","unstructured":"R.B. Ash and C. Dol\u00e9ans-Dade. 2000. Probability and Measure Theory. Harcourt\/Academic Press.  R.B. Ash and C. Dol\u00e9ans-Dade. 2000. Probability and Measure Theory. Harcourt\/Academic Press."},{"key":"e_1_2_2_5_1","volume-title":"Principles of Model Checking","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen . 2008. Principles of Model Checking . The MIT Press , Cambridge, Massachusetts . 984 pages. Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. The MIT Press, Cambridge, Massachusetts. 984 pages."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_3"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934554"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2893582.2893591"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429078"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_18"},{"key":"e_1_2_2_11_1","volume-title":"Probability and Measure","author":"Billingsley P.","unstructured":"P. Billingsley . 1995. Probability and Measure ( 3 rd ed.). Wiley . P. Billingsley. 1995. Probability and Measure (3rd ed.). Wiley.","edition":"3"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_24"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_48"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_109"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_22"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958114"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_15"},{"key":"e_1_2_2_18_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 ). http:\/\/arxiv.org\/abs\/1701.02944 Krishnendu Chatterjee and Hongfei Fu. 2017. Termination of Nondeterministic Recursive Probabilistic Programs. CoRR abs\/1701.02944 (2017). http:\/\/arxiv.org\/abs\/1701.02944"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837639"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009873"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78739-6_13"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_6"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1941487.1941509"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_4"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511581274"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_14"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.09.014"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(84)80039-X"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802191"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177728976"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1038\/nature14541"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737976"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2013.11.004"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1137\/0214070"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622737.1622748"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_24"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/800061.808758"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_9"},{"key":"e_1_2_2_46_1","doi-asserted-by":"crossref","unstructured":"Marta Z. Kwiatkowska Gethin Norman and David Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-Time Systems. In CAV (LNCS 6806). 585\u2013591.  Marta Z. Kwiatkowska Gethin Norman and David Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-Time Systems. In CAV (LNCS 6806). 585\u2013591.","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"key":"e_1_2_2_48_1","doi-asserted-by":"crossref","unstructured":"Annabelle McIver and Carroll Morgan. 2004. Developing and Reasoning About Probabilistic Programs in pGCL. In PSSE. 123\u2013155.  Annabelle McIver and Carroll Morgan. 2004. Developing and Reasoning About Probabilistic Programs in pGCL. In PSSE. 123\u2013155.","DOI":"10.1007\/11889229_4"},{"key":"e_1_2_2_49_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_50_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 ). http:\/\/arxiv.org\/abs\/1612.01091 Annabelle McIver and Carroll Morgan. 2016. A new rule for almost-certain termination of probabilistic and demonic programs. CoRR abs\/1612.01091 (2016). http:\/\/arxiv.org\/abs\/1612.01091"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47764-0_7"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511814075"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/3266641.3266679"},{"key":"e_1_2_2_54_1","volume-title":"International Conference on Concurrency Theory (CONCUR","author":"Neuh\u00e4u\u00dfer Martin R","year":"2007","unstructured":"Martin R Neuh\u00e4u\u00dfer and Joost-Pieter Katoen . 2007 . Bisimulation and logical preservation for continuous-time Markov decision processes . In International Conference on Concurrency Theory (CONCUR 2007). Springer, 412\u2013427. Martin R Neuh\u00e4u\u00dfer and Joost-Pieter Katoen. 2007. Bisimulation and logical preservation for continuous-time Markov decision processes. In International Conference on Concurrency Theory (CONCUR 2007). Springer, 412\u2013427."},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.50"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1142\/4420"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1137\/0213021"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/113413.113433"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158122","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158122","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\/3158122"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":60,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158122"],"URL":"https:\/\/doi.org\/10.1145\/3158122","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"}}]}}