{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T23:10:16Z","timestamp":1765667416547,"version":"3.41.0"},"reference-count":82,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2023,6,23]],"date-time":"2023-06-23T00:00:00Z","timestamp":1687478400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"ERC CoG","award":["863818"],"award-info":[{"award-number":["863818"]}]},{"DOI":"10.13039\/501100001824","name":"Czech Science Foundation","doi-asserted-by":"crossref","award":["GA21-24711S"],"award-info":[{"award-number":["GA21-24711S"]}],"id":[{"id":"10.13039\/501100001824","id-type":"DOI","asserted-by":"crossref"}]},{"name":"European Union\u2019s Horizon 2020 research and innovation program under the Marie Sk\u0142odowska-Curie Grant","award":["665385"],"award-info":[{"award-number":["665385"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2023,6,30]]},"abstract":"<jats:p>We consider the almost-sure (a.s.) termination problem for probabilistic programs, which are a stochastic extension of classical imperative programs. Lexicographic ranking functions provide a sound and practical approach for termination of non-probabilistic programs, and their extension to probabilistic programs is achieved via lexicographic ranking supermartingales (LexRSMs). However, LexRSMs introduced in the previous work have a limitation that impedes their automation: all of their components have to be non-negative in all reachable states. This might result in a LexRSM not existing even for simple terminating programs. Our contributions are twofold. First, we introduce a generalization of LexRSMs that allows for some components to be negative. This standard feature of non-probabilistic termination proofs was hitherto not known to be sound in the probabilistic setting, as the soundness proof requires a careful analysis of the underlying stochastic process. Second, we present polynomial-time algorithms using our generalized LexRSMs for proving a.s. termination in broad classes of linear-arithmetic programs.<\/jats:p>","DOI":"10.1145\/3585391","type":"journal-article","created":{"date-parts":[[2023,2,27]],"date-time":"2023-02-27T12:02:51Z","timestamp":1677499371000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["On Lexicographic Proof Rules for Probabilistic Termination"],"prefix":"10.1145","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4561-241X","authenticated-orcid":false,"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[{"name":"IST Austria, Austria"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8595-0587","authenticated-orcid":false,"given":"Ehsan","family":"Kafshdar Goharshady","sequence":"additional","affiliation":[{"name":"Ferdowsi University of Mashhad, Iran"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5026-4392","authenticated-orcid":false,"given":"Petr","family":"Novotn\u00fd","sequence":"additional","affiliation":[{"name":"Masaryk University, Czech Republic"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6615-7460","authenticated-orcid":false,"given":"Ji\u0159\u00ed","family":"Z\u00e1rev\u00facky","sequence":"additional","affiliation":[{"name":"Masaryk University, Czech Republic"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4681-1699","authenticated-orcid":false,"given":"\u0110or\u0111e","family":"\u017dikeli\u0107","sequence":"additional","affiliation":[{"name":"IST Austria, Austria"}]}],"member":"320","published-online":{"date-parts":[[2023,6,23]]},"reference":[{"key":"e_1_3_1_2_1","first-page":"34:1\u201334:32","article-title":"Lexicographic ranking supermartingales: An efficient approach to termination of probabilistic programs","volume":"2","author":"Agrawal Sheshansh","year":"2018","unstructured":"Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotn\u00fd. 2018. Lexicographic ranking supermartingales: An efficient approach to termination of probabilistic programs. PACMPL 2, POPL (2018), 34:1\u201334:32.","journal-title":"PACMPL"},{"key":"e_1_3_1_3_1","series-title":"Proceedings of the 17th International Conference on Static Analysis","first-page":"117","author":"Alias Christophe","year":"2010","unstructured":"Christophe Alias, Alain Darte, Paul Feautrier, and Laure Gonnord. 2010. Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In Proceedings of the 17th International Conference on Static Analysis (Perpignan, France) (SAS\u201910). Springer, Berlin, 117\u2013133. http:\/\/dl.acm.org\/citation.cfm?id=1882094.1882102."},{"key":"e_1_3_1_4_1","volume-title":"Probability and Measure Theory","author":"Ash R. B.","year":"2000","unstructured":"R. B. Ash and C. Dol\u00e9ans-Dade. 2000. Probability and Measure Theory. Harcourt\/Academic Press. 99065669"},{"doi-asserted-by":"publisher","key":"e_1_3_1_5_1","DOI":"10.1109\/LICS.2019.8785725"},{"doi-asserted-by":"publisher","key":"e_1_3_1_6_1","DOI":"10.1016\/j.scico.2019.102338"},{"doi-asserted-by":"publisher","key":"e_1_3_1_7_1","DOI":"10.1145\/3428240"},{"key":"e_1_3_1_8_1","volume-title":"Principles of Model Checking","author":"Baier Christel","year":"2008","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. The MIT Press, Cambridge, Massachusetts."},{"key":"e_1_3_1_9_1","first-page":"43","volume-title":"Proceedings of the 28th International Conference on Computer Aided Verification (CAV\u201916), Part I, Toronto, ON, Canada, July 17-23, 2016","author":"Barthe Gilles","year":"2016","unstructured":"Gilles Barthe, Thomas Espitau, Luis Mar\u00eda Ferrer Fioriti, and Justin Hsu. 2016a. Synthesizing probabilistic invariants via Doob\u2019s decomposition. In Proceedings of the 28th International Conference on Computer Aided Verification (CAV\u201916), Part I, Toronto, ON, Canada, July 17-23, 2016, Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing, 43\u201361. 10.1007\/978-3-319-41528-4_3"},{"key":"e_1_3_1_10_1","series-title":"Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science","first-page":"749","author":"Barthe Gilles","year":"2016","unstructured":"Gilles Barthe, Marco Gaboardi, Benjamin Gr\u00e9goire, Justin Hsu, and Pierre-Yves Strub. 2016b. Proving differential privacy via probabilistic couplings. In Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science (New York, NY, USA) (LICS\u201916). ACM, New York, NY, 749\u2013758. 10.1145\/2933575.2934554"},{"doi-asserted-by":"publisher","key":"e_1_3_1_11_1","DOI":"10.1145\/2893582.2893591"},{"key":"e_1_3_1_12_1","series-title":"Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","first-page":"51","author":"Ben-Amram Amir M.","year":"2013","unstructured":"Amir M. Ben-Amram and Samir Genaim. 2013. On the linear ranking problem for integer linear-constraint loops. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Rome, Italy) (POPL\u201913). ACM, New York, NY, 51\u201362. 10.1145\/2429069.2429078"},{"key":"e_1_3_1_13_1","first-page":"304","volume-title":"Proceedings of the 27th International Conference on Computer Aided Verification (CAV\u201915, San Francisco, CA, July 18-24, 2015","author":"Ben-Amram Amir M.","year":"2015","unstructured":"Amir M. Ben-Amram and Samir Genaim. 2015. Complexity of Bradley-Manna-Sipma lexicographic ranking functions. In Proceedings of the 27th International Conference on Computer Aided Verification (CAV\u201915, San Francisco, CA, July 18-24, 2015, Daniel Kroening and Corina S. P\u0103s\u0103reanu (Eds.). Springer International Publishing, 304\u2013321. 10.1007\/978-3-319-21668-3_18"},{"key":"e_1_3_1_14_1","volume-title":"Probability and Measure (3rd ed.)","author":"Billingsley P.","year":"1995","unstructured":"P. Billingsley. 1995. Probability and Measure (3rd ed.). Wiley."},{"key":"e_1_3_1_15_1","first-page":"323","volume-title":"RTA","author":"Bournez Olivier","year":"2005","unstructured":"Olivier Bournez and Florent Garnier. 2005. Proving positive almost-sure termination. In RTA. 323\u2013337."},{"key":"e_1_3_1_16_1","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/11513988_48","volume-title":"Proceedings of the 17th International Conference on Computer Aided Verification (CAV\u201905), Edinburgh, Scotland, UK, July 6-10, 2005","author":"Bradley Aaron R.","year":"2005","unstructured":"Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2005. Linear ranking with reachability. In Proceedings of the 17th International Conference on Computer Aided Verification (CAV\u201905), Edinburgh, Scotland, UK, July 6-10, 2005. 491\u2013504. 10.1007\/11513988_48"},{"key":"e_1_3_1_17_1","first-page":"413","volume-title":"Proceedings of the 25th International Conference on Computer Aided Verification (CAV\u201913), Saint Petersburg, Russia, July 13-19, 2013","author":"Brockschmidt Marc","year":"2013","unstructured":"Marc Brockschmidt, Byron Cook, and Carsten Fuhs. 2013. Better termination proving through cooperation. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV\u201913), Saint Petersburg, Russia, July 13-19, 2013. 413\u2013429. 10.1007\/978-3-642-39799-8_28"},{"key":"e_1_3_1_18_1","first-page":"387","volume-title":"Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems(TACAS\u201916), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS\u201916), Eindhoven, The Netherlands, April 2-8, 2016","author":"Brockschmidt Marc","year":"2016","unstructured":"Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, and Nir Piterman. 2016. T2: Temporal property verification. In Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems(TACAS\u201916), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS\u201916), Eindhoven, The Netherlands, April 2-8, 2016, Marsha Chechik and Jean-Fran\u00e7ois Raskin (Eds.). Springer, Berlin, 387\u2013393. 10.1007\/978-3-662-49674-9_22"},{"key":"e_1_3_1_19_1","first-page":"511","volume-title":"CAV 2013","author":"Chakarov Aleksandar","year":"2013","unstructured":"Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic program analysis with martingales. In CAV 2013. 511\u2013526."},{"key":"e_1_3_1_20_1","first-page":"260","volume-title":"Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201916), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS\u201916), Eindhoven, The Netherlands, April 2-8, 2016,","author":"Chakarov Aleksandar","year":"2016","unstructured":"Aleksandar Chakarov, Yuen-Lam Voronin, and Sriram Sankaranarayanan. 2016. Deductive proofs of almost sure persistence and recurrence properties. In Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201916), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS\u201916), Eindhoven, The Netherlands, April 2-8, 2016,Marsha Chechik and Jean-Fran\u00e7ois Raskin (Eds.). Springer, Berlin, 260\u2013279. 10.1007\/978-3-662-49674-9_15"},{"key":"e_1_3_1_21_1","first-page":"3","volume-title":"CAV","author":"Chatterjee Krishnendu","year":"2016","unstructured":"Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. 2016. Termination analysis of probabilistic programs through positivstellensatz\u2019s. In CAV. 3\u201322."},{"doi-asserted-by":"publisher","key":"e_1_3_1_22_1","DOI":"10.1145\/3174800"},{"key":"e_1_3_1_23_1","series-title":"Proceedings of the 34th International Conference on Computer Aided Verification (CAV\u201922), Haifa, Israel, August 7-10, 2022, Part I","first-page":"55","volume":"13371","author":"Chatterjee Krishnendu","year":"2022","unstructured":"Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, and Dorde Zikelic. 2022. Sound and complete certificates for quantitative termination analysis of probabilistic programs. In Proceedings of the 34th International Conference on Computer Aided Verification (CAV\u201922), Haifa, Israel, August 7-10, 2022, Part I(Lecture Notes in Computer Science), Vol. 13371, Sharon Shoham and Yakir Vizel (Eds.). Springer, Berlin, 55\u201378. 10.1007\/978-3-031-13185-1_4"},{"key":"e_1_3_1_24_1","series-title":"Proceedings of the 24th International Symposium on Formal Methods (FM\u201921), Virtual Event, November 20-26, 2021","first-page":"Berlin, 619\u2013639","volume":"13047","author":"Chatterjee Krishnendu","year":"2021","unstructured":"Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotn\u00fd, Jiri Z\u00e1rev\u00facky, and Dorde Zikelic. 2021a. On lexicographic proof rules for probabilistic termination. In Proceedings of the 24th International Symposium on Formal Methods (FM\u201921), Virtual Event, November 20-26, 2021(Lecture Notes in Computer Science), Vol. 13047, Marieke Huisman, Corina S. Pasareanu, and Naijun Zhan (Eds.). Springer, Berlin, 619\u2013639. 10.1007\/978-3-030-90870-6_33"},{"unstructured":"Krishnendu Chatterjee Ehsan Kafshdar Goharshady Petr Novotn\u00fd Ji\u0159\u00ed Z\u00e1rev\u00facky and Dorde Zikelic. 2021b. On Lexicographic Proof Rules for Probabilistic Termination. arxiv:2108.02188 [cs.PL] https:\/\/arxiv.org\/abs\/2108.02188.","key":"e_1_3_1_25_1"},{"key":"e_1_3_1_26_1","series-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages","first-page":"145","author":"Chatterjee Krishnendu","year":"2017","unstructured":"Krishnendu Chatterjee, Petr Novotn\u00fd, and Dorde Zikelic. 2017. Stochastic invariants for probabilistic termination. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Paris, France) (POPL\u201917). ACM, New York, NY, 145\u2013160. 10.1145\/3009837.3009873"},{"key":"e_1_3_1_27_1","first-page":"869","volume-title":"Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI\u201920), London, UK, June 15-20, 2020","author":"Chen Jianhui","year":"2020","unstructured":"Jianhui Chen and Fei He. 2020. Proving almost-sure termination by omega-regular decomposition. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI\u201920), London, UK, June 15-20, 2020. 869\u2013882. 10.1145\/3385412.3386002"},{"key":"e_1_3_1_28_1","first-page":"92","volume-title":"Joint Meeting on Foundations of Software Engineering","author":"Claret Guillaume","year":"2013","unstructured":"Guillaume Claret, Sriram K. Rajamani, Aditya V. Nori, Andrew D. Gordon, and Johannes Borgstr\u00f6m. 2013. Bayesian inference using data flow analysis. In Joint Meeting on Foundations of Software Engineering. ACM, 92\u2013102."},{"key":"e_1_3_1_29_1","first-page":"67","volume-title":"Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901) Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS\u201901) Genova, Italy, April 2-6, 2001","author":"Col\u00f3n Michael","year":"2001","unstructured":"Michael Col\u00f3n and Henny Sipma. 2001. Synthesis of linear ranking functions. In Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901) Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS\u201901) Genova, Italy, April 2-6, 2001. 67\u201381. 10.1007\/3-540-45319-9_6"},{"doi-asserted-by":"publisher","key":"e_1_3_1_30_1","DOI":"10.1145\/1133255.1134029"},{"doi-asserted-by":"publisher","key":"e_1_3_1_31_1","DOI":"10.1145\/1941487.1941509"},{"key":"e_1_3_1_32_1","series-title":"Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","first-page":"47","author":"Cook Byron","year":"2013","unstructured":"Byron Cook, Abigail See, and Florian Zuleger. 2013. Ramsey vs. lexicographic termination proving. In Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Rome, Italy) (TACAS\u201913). Springer, Berlin,47\u201361. 10.1007\/978-3-642-36742-7_4"},{"key":"e_1_3_1_33_1","first-page":"238","volume-title":"Conference Record of the 4th ACM Symposium on Principles of Programming Languages, Los Angeles, CA, January 1977","author":"Cousot Patrick","year":"1977","unstructured":"Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symposium on Principles of Programming Languages, Los Angeles, CA, January 1977. 238\u2013252. 10.1145\/512950.512973"},{"doi-asserted-by":"publisher","key":"e_1_3_1_34_1","DOI":"10.1145\/3434313"},{"key":"e_1_3_1_35_1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511581274","volume-title":"Concentration of Measure for the Analysis of Randomized Algorithms (1st ed.)","author":"Dubhashi Devdatt","year":"2009","unstructured":"Devdatt Dubhashi and Alessandro Panconesi. 2009. Concentration of Measure for the Analysis of Randomized Algorithms (1st ed.). Cambridge University Press, New York, NY."},{"key":"e_1_3_1_36_1","first-page":"123","volume-title":"CAV 2012","author":"Esparza Javier","year":"2012","unstructured":"Javier Esparza, Andreas Gaiser, and Stefan Kiefer. 2012. Proving termination of probabilistic programs using patterns. In CAV 2012. 123\u2013138."},{"doi-asserted-by":"publisher","key":"e_1_3_1_37_1","DOI":"10.1016\/S0019-9958(84)80039-X"},{"key":"e_1_3_1_38_1","first-page":"181","volume-title":"Proceedings of the 14th Annual ACM Symposium on Theory of Computing","author":"Feldman Yishai A.","year":"1982","unstructured":"Yishai A. Feldman and David Harel. 1982. A probabilistic dynamic logic. In Proceedings of the 14th Annual ACM Symposium on Theory of Computing. ACM, 181\u2013195."},{"key":"e_1_3_1_39_1","first-page":"489","volume-title":"Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (POPL\u201915), Mumbai, India, January 15-17, 2015","author":"Fioriti Luis Mar\u00eda Ferrer","year":"2015","unstructured":"Luis Mar\u00eda Ferrer Fioriti and Holger Hermanns. 2015. Probabilistic termination: Soundness, completeness, and compositionality. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (POPL\u201915), Mumbai, India, January 15-17, 2015. 489\u2013501. 10.1145\/2676726.2677001"},{"key":"e_1_3_1_40_1","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","article-title":"Assigning meanings to programs","volume":"19","author":"Floyd Robert W.","year":"1967","unstructured":"Robert W. Floyd. 1967. Assigning meanings to programs. Mathematical Aspects of Computer Science 19 (1967), 19\u201333.","journal-title":"Mathematical Aspects of Computer Science"},{"issue":"3","key":"e_1_3_1_41_1","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1214\/aoms\/1177728976","article-title":"On the stochastic matrices associated with certain queuing processes","volume":"24","author":"Foster F. G.","year":"1953","unstructured":"F. G. Foster. 1953. On the stochastic matrices associated with certain queuing processes. The Annals of Mathematical Statistics 24, 3 (1953), 355\u2013360.","journal-title":"The Annals of Mathematical Statistics"},{"key":"e_1_3_1_42_1","first-page":"282","volume-title":"ESOP\u201916","author":"Foster Nate","year":"2016","unstructured":"Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. 2016. Probabilistic NetKAT. In ESOP\u201916. Springer, 282\u2013309."},{"key":"e_1_3_1_43_1","series-title":"Proceedings of the 20th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI\u201919), Cascais, Portugal, January 13-15, 2019","first-page":"468","volume":"11388","author":"Fu Hongfei","year":"2019","unstructured":"Hongfei Fu and Krishnendu Chatterjee. 2019. Termination of nondeterministic probabilistic programs. In Proceedings of the 20th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI\u201919), Cascais, Portugal, January 13-15, 2019(Lecture Notes in Computer Science), Vol. 11388, Constantin Enea and Ruzica Piskac (Eds.). Springer, Berlin, 468\u2013490. 10.1007\/978-3-030-11245-5_22"},{"issue":"7553","key":"e_1_3_1_44_1","doi-asserted-by":"crossref","first-page":"452","DOI":"10.1038\/nature14541","article-title":"Probabilistic machine learning and artificial intelligence","volume":"521","author":"Ghahramani Zoubin","year":"2015","unstructured":"Zoubin Ghahramani. 2015. Probabilistic machine learning and artificial intelligence. Nature 521, 7553 (2015), 452\u2013459.","journal-title":"Nature"},{"key":"e_1_3_1_45_1","first-page":"269","volume-title":"Automated Deduction (CADE 27)","author":"Giesl J\u00fcrgen","year":"2019","unstructured":"J\u00fcrgen Giesl, Peter Giesl, and Marcel Hark. 2019. Computing expected runtimes for constant probability programs. In Automated Deduction (CADE 27), Pascal Fontaine (Ed.). Springer International Publishing, Cham, 269\u2013286."},{"key":"e_1_3_1_46_1","series-title":"Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation","first-page":"608","author":"Gonnord Laure","year":"2015","unstructured":"Laure Gonnord, David Monniaux, and Gabriel Radanne. 2015. Synthesis of ranking functions using extremal counterexamples. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (Portland, OR) (PLDI\u201915). ACM, New York, NY, 608\u2013618. 10.1145\/2737924.2737976"},{"issue":"1","key":"e_1_3_1_47_1","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1145\/2480359.2429119","article-title":"A model-learner pattern for Bayesian reasoning","volume":"48","author":"Gordon Andrew D.","year":"2013","unstructured":"Andrew D. Gordon, Mihhail Aizatulin, Johannes Borgstrom, Guillaume Claret, Thore Graepel, Aditya V. Nori, Sriram K. Rajamani, and Claudio Russo. 2013. A model-learner pattern for Bayesian reasoning. ACM SIGPLAN Notices 48, 1 (2013), 403\u2013416.","journal-title":"ACM SIGPLAN Notices"},{"key":"e_1_3_1_48_1","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1145\/2593882.2593900","volume-title":"Proceedings of the on Future of Software Engineering","author":"Gordon Andrew D.","year":"2014","unstructured":"Andrew D. Gordon, Thomas A. Henzinger, Aditya V. Nori, and Sriram K. Rajamani. 2014. Probabilistic programming. In Proceedings of the on Future of Software Engineering. ACM, 167\u2013181."},{"doi-asserted-by":"publisher","key":"e_1_3_1_49_1","DOI":"10.1016\/j.peva.2013.11.004"},{"doi-asserted-by":"publisher","key":"e_1_3_1_50_1","DOI":"10.1145\/3371105"},{"key":"e_1_3_1_51_1","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/978-3-030-02768-1_11","volume-title":"Programming Languages and Systems","author":"Huang Mingzhang","year":"2018","unstructured":"Mingzhang Huang, Hongfei Fu, and Krishnendu Chatterjee. 2018. New approaches for almost-sure termination of probabilistic programs. In Programming Languages and Systems, Sukyoung Ryu (Ed.). Springer International Publishing, Cham, 181\u2013201."},{"doi-asserted-by":"publisher","key":"e_1_3_1_52_1","DOI":"10.1145\/3360555"},{"key":"e_1_3_1_53_1","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1613\/jair.301","article-title":"Reinforcement learning: A survey","volume":"4","author":"Kaelbling L. P.","year":"1996","unstructured":"L. P. Kaelbling, M. L. Littman, and A. W. Moore. 1996. Reinforcement learning: A survey. Journal of Artificial Intelligence Research 4 (1996), 237\u2013285.","journal-title":"Journal of Artificial Intelligence Research"},{"doi-asserted-by":"publisher","key":"e_1_3_1_54_1","DOI":"10.1145\/3208102"},{"key":"e_1_3_1_55_1","first-page":"1","article-title":"On the hardness of analyzing probabilistic programs","author":"Kaminski Benjamin Lucien","year":"2018","unstructured":"Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2018a. On the hardness of analyzing probabilistic programs. Acta Informatica (2018), 1\u201331.","journal-title":"Acta Informatica"},{"issue":"4","key":"e_1_3_1_56_1","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. Logical Methods in Computer Science 16, 4 (2020). https:\/\/lmcs.episciences.org\/6817.","journal-title":"Logical Methods in Computer Science"},{"doi-asserted-by":"publisher","key":"e_1_3_1_57_1","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_3_1_58_1","first-page":"291","volume-title":"Proceedings of the 15th Annual ACM Symposium on Theory of Computing (STOC\u201983)","author":"Kozen Dexter","year":"1983","unstructured":"Dexter Kozen. 1983. A probabilistic PDL. In Proceedings of the 15th Annual ACM Symposium on Theory of Computing (STOC\u201983). ACM, New York, NY, 291\u2013297. 10.1145\/800061.808758"},{"key":"e_1_3_1_59_1","first-page":"585","volume-title":"CAV\u201911 (Lecture Notes in Computer Science)","author":"Kwiatkowska Marta Z.","year":"2011","unstructured":"Marta Z. Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In CAV\u201911 (Lecture Notes in Computer Science), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Vol. 6806, Springer, Berlin. 585\u2013591."},{"doi-asserted-by":"publisher","key":"e_1_3_1_60_1","DOI":"10.1145\/3293605"},{"key":"e_1_3_1_61_1","first-page":"123","volume-title":"PSSE","author":"McIver Annabelle","year":"2004","unstructured":"Annabelle McIver and Carroll Morgan. 2004. Developing and reasoning about probabilistic programs in pGCL. In PSSE. 123\u2013155."},{"key":"e_1_3_1_62_1","volume-title":"Abstraction, Refinement and Proof for Probabilistic Systems","author":"McIver Annabelle","year":"2005","unstructured":"Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement and Proof for Probabilistic Systems. Springer."},{"key":"e_1_3_1_63_1","article-title":"A new rule for almost-certain termination of probabilistic and demonic programs","volume":"1612","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.","journal-title":"CoRR"},{"doi-asserted-by":"crossref","unstructured":"Annabelle McIver Carroll Morgan Benjamin Lucien Kaminski and Joost-Pieter Katoen. 2018. A new proof rule for almost-sure termination. Proc. ACM Program. Lang. 2 POPL (2018).","key":"e_1_3_1_64_1","DOI":"10.1145\/3158121"},{"key":"e_1_3_1_65_1","series-title":"Proceedings of the 8th International Symposium on Static Analysis (SAS\u201901), Paris, France, July 16-18, 2001","first-page":"Berlin, 111\u2013126","volume":"2126","author":"Monniaux David","year":"2001","unstructured":"David Monniaux. 2001. An abstract analysis of the probabilistic termination of programs. In Proceedings of the 8th International Symposium on Static Analysis (SAS\u201901), Paris, France, July 16-18, 2001(Lecture Notes in Computer Science), Vol. 2126, Patrick Cousot (Ed.). Springer, Berlin, 111\u2013126. 10.1007\/3-540-47764-0_7"},{"key":"e_1_3_1_66_1","series-title":"Programming Languages and Systems - Proceedings of the 30th European Symposium on Programming (ESOP\u201921), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS\u201921), Luxembourg City, Luxembourg, March 27 - April 1, 2021","first-page":"Berlin, 491\u2013518","volume":"12648","author":"Moosbrugger Marcel","year":"2021","unstructured":"Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, and Laura Kov\u00e1cs. 2021. Automated termination analysis of polynomial probabilistic programs. In Programming Languages and Systems - Proceedings of the 30th European Symposium on Programming (ESOP\u201921), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS\u201921), Luxembourg City, Luxembourg, March 27 - April 1, 2021(Lecture Notes in Computer Science), Vol. 12648, Nobuko Yoshida (Ed.). Springer, Berlin, 491\u2013518. 10.1007\/978-3-030-72019-3_18"},{"unstructured":"Carroll Morgan and A McIver. 1999. pGCL: Formal reasoning for random algorithms. (1999).","key":"e_1_3_1_67_1"},{"issue":"3","key":"e_1_3_1_68_1","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1145\/229542.229547","article-title":"Probabilistic predicate transformers","volume":"18","author":"Morgan Carroll","year":"1996","unstructured":"Carroll Morgan, Annabelle McIver, and Karen Seidel. 1996. Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems 18, 3 (1996), 325\u2013353.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"e_1_3_1_69_1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511814075","volume-title":"Randomized Algorithms","author":"Motwani Rajeev","year":"1995","unstructured":"Rajeev Motwani and Prabhakar Raghavan. 1995. Randomized Algorithms. Cambridge University Press, New York, NY."},{"key":"e_1_3_1_70_1","first-page":"412","volume-title":"International Conference on Concurrency Theory (CONCUR\u201907)","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\u201907). Springer, 412\u2013427."},{"key":"e_1_3_1_71_1","first-page":"364","volume-title":"Proceedings of the 12th International Conference of Foundations of Software Science and Computational Structures (FOSSACS\u201909), Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS\u201909), York, UK, March 22-29, 2009.","author":"Neuh\u00e4u\u00dfer Martin R.","year":"2009","unstructured":"Martin R. Neuh\u00e4u\u00dfer, Mari\u00eblle Stoelinga, and Joost-Pieter Katoen. 2009. Delayed nondeterminism in continuous-time Markov decision processes. In Proceedings of the 12th International Conference of Foundations of Software Science and Computational Structures (FOSSACS\u201909), Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS\u201909), York, UK, March 22-29, 2009.364\u2013379. 10.1007\/978-3-642-00596-1_26"},{"key":"e_1_3_1_72_1","first-page":"496","volume-title":"PLDI 2018","author":"Ngo Van Chan","year":"2018","unstructured":"Van Chan Ngo, Quentin Carbonneaux, and Jan Hoffmann. 2018. Bounded expectations: Resource analysis for probabilistic programs. In PLDI 2018. 496\u2013512."},{"key":"e_1_3_1_73_1","series-title":"Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science","first-page":"672","author":"Olmedo Federico","year":"2016","unstructured":"Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2016. Reasoning about recursive probabilistic programs. In Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science (New York, NY) (LICS\u201916). ACM, New York, NY, 672\u2013681. 10.1145\/2933575.2935317"},{"key":"e_1_3_1_74_1","first-page":"239","volume-title":"Proceedings of the 5th International Conference of Verification, Model Checking, and Abstract Interpretation (VMCAI\u201904), Venice, January 11-13, 2004","author":"Podelski Andreas","year":"2004","unstructured":"Andreas Podelski and Andrey Rybalchenko. 2004a. A complete method for the synthesis of linear ranking functions. In Proceedings of the 5th International Conference of Verification, Model Checking, and Abstract Interpretation (VMCAI\u201904), Venice, January 11-13, 2004. 239\u2013251. 10.1007\/978-3-540-24622-0_20"},{"key":"e_1_3_1_75_1","first-page":"32","volume-title":"Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS\u201904)","author":"Podelski Andreas","year":"2004","unstructured":"Andreas Podelski and Andrey Rybalchenko. 2004b. Transition invariants. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS\u201904). IEEE Computer Society, Washington, DC, 32\u201341. 10.1109\/LICS.2004.50"},{"key":"e_1_3_1_76_1","first-page":"26","volume-title":"Nonparametric Bayesian Workshop, International Conference on Machine Learning","volume":"22","author":"Roy D. M.","year":"2008","unstructured":"D. M. Roy, V. K. Mansinghka, N. D. Goodman, and J. B. Tenenbaum. 2008. A stochastic programming perspective on nonparametric Bayes. In Nonparametric Bayesian Workshop, International Conference on Machine Learning, Vol. 22. 26."},{"issue":"12","key":"e_1_3_1_77_1","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1145\/2887747.2804317","article-title":"Practical probabilistic programming with monads","volume":"50","author":"\u015acibior Adam","year":"2015","unstructured":"Adam \u015acibior, Zoubin Ghahramani, and Andrew D. Gordon. 2015. Practical probabilistic programming with monads. ACM SIGPLAN Notices 50, 12 (2015), 165\u2013176.","journal-title":"ACM SIGPLAN Notices"},{"key":"e_1_3_1_78_1","first-page":"557","volume-title":"POPL\u201917","author":"Smolka Steffen","year":"2017","unstructured":"Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva. 2017. Cantor meets Scott: Semantic foundations for probabilistic networks. In POPL\u201917. 557\u2013571."},{"key":"e_1_3_1_79_1","first-page":"216","volume-title":"Proceedings of the 10th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, May 29-31, 1991, Denver, CO","author":"Sohn Kirack","year":"1991","unstructured":"Kirack Sohn and Allen Van Gelder. 1991. Termination detection in logic programs using argument sizes. In Proceedings of the 10th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, May 29-31, 1991, Denver, CO. 216\u2013226. 10.1145\/113413.113433"},{"issue":"3","key":"e_1_3_1_80_1","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1145\/504729.504754","article-title":"Probabilistic robotics","volume":"45","author":"Thrun Sebastian","year":"2002","unstructured":"Sebastian Thrun. 2002. Probabilistic robotics. Communications of the ACM 45, 3 (2002), 52\u201357.","journal-title":"Communications of the ACM"},{"key":"e_1_3_1_81_1","first-page":"513","volume-title":"PLDI\u201918","author":"Wang Di","year":"2018","unstructured":"Di Wang, Jan Hoffmann, and Thomas W. Reps. 2018. PMAF: An algebraic framework for static analysis of probabilistic programs. In PLDI\u201918. 513\u2013528."},{"key":"e_1_3_1_82_1","first-page":"204","volume-title":"PLDI\u201919","author":"Wang Peixin","year":"2019","unstructured":"Peixin Wang, Hongfei Fu, Amir Kafshdar Goharshady, Krishnendu Chatterjee, Xudong Qin, and Wenjun Shi. 2019. Cost analysis of nondeterministic probabilistic programs. In PLDI\u201919. 204\u2013220."},{"key":"e_1_3_1_83_1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511813658","volume-title":"Probability with Martingales","author":"Williams D.","year":"1991","unstructured":"D. Williams. 1991. Probability with Martingales. Cambridge University Press, Cambridge, UK. 251 pages."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3585391","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3585391","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:56Z","timestamp":1750178276000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3585391"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,23]]},"references-count":82,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,6,30]]}},"alternative-id":["10.1145\/3585391"],"URL":"https:\/\/doi.org\/10.1145\/3585391","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2023,6,23]]},"assertion":[{"value":"2022-03-31","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-02-07","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-06-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}