{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:39:33Z","timestamp":1780994373714,"version":"3.54.1"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2018,5,28]],"date-time":"2018-05-28T00:00:00Z","timestamp":1527465600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"FWF NFN","award":["S11407-N23(RiSE\/SHiNE)"],"award-info":[{"award-number":["S11407-N23(RiSE\/SHiNE)"]}]},{"DOI":"10.13039\/501100001809","name":"Natural Science Foundation of China","doi-asserted-by":"crossref","award":["61532019"],"award-info":[{"award-number":["61532019"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"REA","award":["291734"],"award-info":[{"award-number":["291734"]}]},{"name":"ERC","award":["279307: Graph Games"],"award-info":[{"award-number":["279307: Graph Games"]}]},{"name":"Austrian Science Fund","award":["P23499-N23"],"award-info":[{"award-number":["P23499-N23"]}]},{"name":"People Programme (Marie Curie Actions) of the European Union's Seventh Framework Programme","award":["FP7\/2007-2013"],"award-info":[{"award-number":["FP7\/2007-2013"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2018,6,30]]},"abstract":"<jats:p>\n            In this article, we consider the termination problem of probabilistic programs with real-valued variables. The questions concerned are: qualitative ones that ask (i) whether the program terminates with probability 1 (almost-sure termination) and (ii) whether the expected termination time is finite (finite termination); and quantitative ones that ask (i) to approximate the expected termination time (expectation problem) and (ii) to compute a bound\n            <jats:italic>B<\/jats:italic>\n            such that the probability not to terminate after\n            <jats:italic>B<\/jats:italic>\n            steps decreases exponentially (concentration problem). To solve these questions, we utilize the notion of ranking supermartingales, which is a powerful approach for proving termination of probabilistic programs. In detail, we focus on algorithmic synthesis of linear ranking-supermartingales over affine probabilistic programs (A\n            <jats:sc>pps<\/jats:sc>\n            ) with both angelic and demonic non-determinism. An important subclass of A\n            <jats:sc>pps<\/jats:sc>\n            is LRA\n            <jats:sc>pp<\/jats:sc>\n            which is defined as the class of all A\n            <jats:sc>pps<\/jats:sc>\n            over which a linear ranking-supermartingale exists.\n          <\/jats:p>\n          <jats:p>\n            Our main contributions are as follows. Firstly, we show that the membership problem of LRA\n            <jats:sc>pp<\/jats:sc>\n            (i) can be decided in polynomial time for A\n            <jats:sc>pps<\/jats:sc>\n            with at most demonic non-determinism, and (ii) is NP-hard and in PSPACE for A\n            <jats:sc>pps<\/jats:sc>\n            with angelic non-determinism. Moreover, the NP-hardness result holds already for A\n            <jats:sc>pps<\/jats:sc>\n            without probability and demonic non-determinism. Secondly, we show that the concentration problem over LRA\n            <jats:sc>pp<\/jats:sc>\n            can be solved in the same complexity as for the membership problem of LRA\n            <jats:sc>pp<\/jats:sc>\n            . Finally, we show that the expectation problem over LRA\n            <jats:sc>pp<\/jats:sc>\n            can be solved in 2EXPTIME and is PSPACE-hard even for A\n            <jats:sc>pps<\/jats:sc>\n            without probability and non-determinism (i.e., deterministic programs). Our experimental results demonstrate the effectiveness of our approach to answer the qualitative and quantitative questions over A\n            <jats:sc>pps<\/jats:sc>\n            with at most demonic non-determinism.\n          <\/jats:p>","DOI":"10.1145\/3174800","type":"journal-article","created":{"date-parts":[[2018,5,29]],"date-time":"2018-05-29T12:24:26Z","timestamp":1527596666000},"page":"1-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":36,"title":["Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs"],"prefix":"10.1145","volume":"40","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[{"name":"IST Austria, Klosterneuburg, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hongfei","family":"Fu","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, P.R. China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Petr","family":"Novotn\u00fd","sequence":"additional","affiliation":[{"name":"IST Austria, Klosterneuburg, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rouzbeh","family":"Hasheminezhad","sequence":"additional","affiliation":[{"name":"Sharif University of Technology, Iran"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,5,28]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.2748\/tmj\/1178243286"},{"key":"e_1_2_2_2_1","volume-title":"Principles of Model Checking","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press. I--XVII, 1--975 pages."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_3"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1080\/01621459.1962.10482149"},{"key":"e_1_2_2_5_1","volume-title":"Probability and Measure","author":"Billingsley P","unstructured":"P Billingsley. 1995. Probability and Measure (3rd ed.). Wiley.","edition":"3"},{"key":"e_1_2_2_6_1","volume-title":"Handbook of Automated Reasoning (in 2 volumes)","author":"Bockmayr Alexander","unstructured":"Alexander Bockmayr and Volker Weispfenning. 2001. Solving numerical constraints. In Handbook of Automated Reasoning (in 2 volumes), John Alan Robinson and Andrei Voronkov (Eds.). Elsevier and MIT Press, 751--842."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","unstructured":"Olivier Bournez and Florent Garnier. 2005. Proving positive almost-sure termination. In RTA. 323--337. 10.1007\/978-3-540-32033-3_24","DOI":"10.1007\/978-3-540-32033-3_24"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_48"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_109"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0166-0"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/62212.62257"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837639"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1080\/15427951.2006.10129115"},{"key":"e_1_2_2_15_1","unstructured":"Michael Col\u00f3n and Henny Sipma. 2001. Synthesis of linear ranking functions. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS\u201901) (Lecture Notes in Computer Science Tiziana Margaria and Wang Yi (Eds.) Vol. 2031. Springer 67--81."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","unstructured":"Byron Cook Abigail See and Florian Zuleger. 2013. Ramsey vs. lexicographic termination proving. In TACAS. 47--61. 10.1007\/978-3-642-36742-7_4","DOI":"10.1007\/978-3-642-36742-7_4"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/1568639"},{"key":"e_1_2_2_19_1","volume-title":"Probability: Theory and Examples","author":"Durrett R.","year":"1996","unstructured":"R. Durrett. 1996. Probability: Theory and Examples (2nd ed.). Duxbury Press.","edition":"2"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","unstructured":"Javier Esparza Andreas Gaiser and Stefan Kiefer. 2012. Proving termination of probabilistic programs using patterns. In CAV. 123--138. 10.1007\/978-3-642-31424-7_14","DOI":"10.1007\/978-3-642-31424-7_14"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.39"},{"key":"e_1_2_2_22_1","volume-title":"A fourier-f\u00e9le mechanikai elv alkalmaz\u00e1sai (Hungarian). Mathematikai\u00e9s Term\u00e9szettudom\u00e1nyi \u00c9rtesit\u00f6 12","author":"Farkas J.","year":"1894","unstructured":"J. Farkas. 1894. A fourier-f\u00e9le mechanikai elv alkalmaz\u00e1sai (Hungarian). Mathematikai\u00e9s Term\u00e9szettudom\u00e1nyi \u00c9rtesit\u00f6 12 (1894), 457--472."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177728976"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1137\/0214070"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1080\/01621459.1963.10500830"},{"key":"e_1_2_2_28_1","volume-title":"Dynamic Programming and Markov Processes","author":"Howard H.","unstructured":"H. Howard. 1960. Dynamic Programming and Markov Processes. MIT Press."},{"key":"e_1_2_2_29_1","unstructured":"IBM 2010. IBM ILOG CPLEX Optimizer. Retrieved from http:\/\/www-01.ibm.com\/software\/integration\/optimization\/cplex-optimizer\/."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/1643275.1643301"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622737.1622748"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/1882094.1882118"},{"key":"e_1_2_2_33_1","unstructured":"J.G. Kemeny J.L. Snell and A.W. Knapp. 1966. Denumerable Markov Chains. D. Van Nostrand Company."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2009.2030225"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","unstructured":"Marta Z. Kwiatkowska Gethin Norman and David Parker. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In CAV (LNCS 6806). 585--591.","DOI":"10.5555\/2032305.2032352"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"key":"e_1_2_2_37_1","doi-asserted-by":"crossref","unstructured":"Colin McDiarmid. 1998. Concentration. In Probabilistic Methods for Algorithmic Discrete Mathematics. 195--248.","DOI":"10.1007\/978-3-662-12788-9_6"},{"key":"e_1_2_2_38_1","doi-asserted-by":"crossref","unstructured":"Annabelle McIver and Carroll Morgan. 2004. Developing and reasoning about probabilistic programs in pGCL. In PSSE. 123--155.","DOI":"10.1007\/11889229_4"},{"key":"e_1_2_2_39_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."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","unstructured":"S. Meyn and R.L. Tweedie. 2009. Markov Chains and Stochastic Stability. Cambridge.","DOI":"10.5555\/1550713"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/647170.718306"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/211390"},{"key":"e_1_2_2_44_1","volume-title":"Osborne and Ariel Rubinstein","author":"Martin","year":"1994","unstructured":"Martin J. Osborne and Ariel Rubinstein. 1994. A Course in Game Theory."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/1097027"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(63)90290-0"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1142\/4420"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","unstructured":"Sriram Sankaranarayanan Aleksandar Chakarov and Sumit Gulwani. 2013. Static analysis for probabilistic programs: Inferring whole program properties from finitely many paths. In PLDI. 447--458. 10.1145\/2491956.2462179","DOI":"10.1145\/2491956.2462179"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/17634"},{"key":"e_1_2_2_51_1","volume-title":"Combinatorial Optimization\u2014Polyhedra and Efficiency","author":"Schrijver Alexander","unstructured":"Alexander Schrijver. 2003. Combinatorial Optimization\u2014Polyhedra and Efficiency. Springer."},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1137\/0213021"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/113413.113433"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","unstructured":"Armando Solar-Lezama Rodric M. Rabbah Rastislav Bod\u00edk and Kemal Ebcioglu. 2005. Programming by sketching for bit-streaming programs. In PLDI. 281--294. 10.1145\/1065010.1065045","DOI":"10.1145\/1065010.1065045"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/2794494.3112725"},{"key":"e_1_2_2_56_1","volume-title":"Probability with Martingales","author":"Williams David","unstructured":"David Williams. 1991. Probability with Martingales. Cambridge University Press."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3174800","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3174800","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:33Z","timestamp":1750212693000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3174800"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,5,28]]},"references-count":55,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,6,30]]}},"alternative-id":["10.1145\/3174800"],"URL":"https:\/\/doi.org\/10.1145\/3174800","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,5,28]]},"assertion":[{"value":"2016-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-05-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}