{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,4]],"date-time":"2025-12-04T10:00:58Z","timestamp":1764842458324,"version":"3.40.3"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030720186"},{"type":"electronic","value":"9783030720193"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The termination behavior of probabilistic programs depends on the outcomes of random assignments. Almost sure termination (AST) is concerned with the question whether a program terminates with probability one on all possible inputs. Positive almost sure termination (PAST) focuses on termination in a finite expected number of steps. This paper presents a fully automated approach to the termination analysis of probabilistic while-programs whose guards and expressions are polynomial expressions. As proving (positive) AST is undecidable in general, existing proof rules typically provide sufficient conditions. These conditions mostly involve constraints on supermartingales. We consider four proof rules from the literature and extend these with generalizations of existing proof rules for (P)AST. We automate the resulting set of proof rules by effectively computing asymptotic bounds on polynomials over the program variables. These bounds are used to decide the sufficient conditions \u2013 including the constraints on supermartingales \u2013 of a proof rule. Our software tool <jats:sc>Amber<\/jats:sc> can thus check AST, PAST, as well as their negations for a large class of polynomial probabilistic programs, while carrying out the termination reasoning fully with polynomial witnesses. Experimental results show the merits of our generalized proof rules and demonstrate that <jats:sc>Amber<\/jats:sc> can handle probabilistic programs that are out of reach for other state-of-the-art tools.<\/jats:p>","DOI":"10.1007\/978-3-030-72019-3_18","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T14:03:10Z","timestamp":1616421790000},"page":"491-518","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":23,"title":["Automated Termination Analysis of Polynomial Probabilistic Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2006-3741","authenticated-orcid":false,"given":"Marcel","family":"Moosbrugger","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8004-6601","authenticated-orcid":false,"given":"Ezio","family":"Bartocci","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8299-2714","authenticated-orcid":false,"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","unstructured":"Agrawal, S., Chatterjee, K., Novotn\u00fd, P.: Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. Proc. of POPL (2017). https:\/\/doi.org\/10.1145\/3158122","DOI":"10.1145\/3158122"},{"key":"18_CR2","doi-asserted-by":"publisher","unstructured":"Arora, N.S., Russell, S.J., Sudderth, E.B.: NET\u2013VISA: Network Processing Vertically Integrated Seismic Analysis. Seismol. Soc. Am., Bull. (2013). https:\/\/doi.org\/10.1785\/0120120107","DOI":"10.1785\/0120120107"},{"key":"18_CR3","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Lago, U.D., Yamada, A.: On probabilistic term rewriting. Sci. Comput. Program. (2020). https:\/\/doi.org\/10.1016\/j.scico.2019.102338","DOI":"10.1016\/j.scico.2019.102338"},{"key":"18_CR4","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Kov\u00e1cs, L., Stankovic, M.: Automatic generation of moment-based invariants for prob-solvable loops. In: Proc. of ATVA (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_15","DOI":"10.1007\/978-3-030-31784-3_15"},{"key":"18_CR5","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Kov\u00e1cs, L., Stankovic, M.: Analysis of bayesian networks via prob-solvable loops. In: Proc. of ICTAC (2020). https:\/\/doi.org\/10.1007\/978-3-030-64276-1_12","DOI":"10.1007\/978-3-030-64276-1_12"},{"key":"18_CR6","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Kov\u00e1cs, L., Stankovic, M.: Mora - automatic generation of moment-based invariants. In: Proc. of TACAS (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5","DOI":"10.1007\/978-3-030-45190-5"},{"key":"18_CR7","doi-asserted-by":"publisher","unstructured":"Bistline, J.E., Blum, D.M., Rinaldi, C., Shields-Estrada, G., Hecker, S.S., Pat\u00e9-Cornell, M.E.: A Bayesian Model to Assess the Size of North Korea\u2019s Uranium Enrichment Program. Sci. Global Secur. (2015). https:\/\/doi.org\/10.1080\/08929882.2015.1039431","DOI":"10.1080\/08929882.2015.1039431"},{"key":"18_CR8","doi-asserted-by":"publisher","unstructured":"Bournez, O., Garnier, F.: Proving positive almost-sure termination. In: Proc. of RTA (2005). https:\/\/doi.org\/10.1007\/978-3-540-32033-3_24","DOI":"10.1007\/978-3-540-32033-3_24"},{"key":"18_CR9","doi-asserted-by":"publisher","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Termination of Polynomial Programs. In: Proc. of VMCAI (2005). https:\/\/doi.org\/10.1007\/b105073","DOI":"10.1007\/b105073"},{"key":"18_CR10","doi-asserted-by":"publisher","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic Program Analysis with Martingales. In: Proc. of CAV (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"18_CR11","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Termination Analysis of Probabilistic Programs Through Positivstellensatz\u2019s. In: Proc. of CAV (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_1","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"18_CR12","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Fu, H., Novotn\u00fd, P., Hasheminezhad, R.: Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs. ACM Trans. Program. Lang. Syst. (2018). https:\/\/doi.org\/10.1145\/3174800","DOI":"10.1145\/3174800"},{"key":"18_CR13","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Novotn\u00fd, P., Zikelic, D.: Stochastic Invariants for Probabilistic Termination. In: Proc. of POPL (2017). https:\/\/doi.org\/10.1145\/3009837.3009873","DOI":"10.1145\/3009837.3009873"},{"key":"18_CR14","doi-asserted-by":"publisher","unstructured":"Chen, J., He, F.: Proving almost-sure termination by omega-regular decomposition. In: Proc. of PLDI (2020). https:\/\/doi.org\/10.1145\/3385412.3386002","DOI":"10.1145\/3385412.3386002"},{"key":"18_CR15","doi-asserted-by":"publisher","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Terminator: Beyond Safety. In: Proc. of CAV (2006). https:\/\/doi.org\/10.1007\/11817963_37","DOI":"10.1007\/11817963_37"},{"key":"18_CR16","doi-asserted-by":"publisher","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Proving program termination. Commun. ACM (2011). https:\/\/doi.org\/10.1145\/1941487.1941509","DOI":"10.1145\/1941487.1941509"},{"key":"18_CR17","doi-asserted-by":"publisher","unstructured":"Dal Lago, U., Grellois, C.: Probabilistic termination by monadic affine sized typing. ACM Trans. Program. Lang. Syst. (2019). https:\/\/doi.org\/10.1145\/3293605","DOI":"10.1145\/3293605"},{"key":"18_CR18","doi-asserted-by":"publisher","unstructured":"Esparza, J., Gaiser, A., Kiefer, S.: Proving Termination of Probabilistic Programs Using Patterns. In: Proc. of CAV (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_14","DOI":"10.1007\/978-3-642-31424-7_14"},{"key":"18_CR19","doi-asserted-by":"publisher","unstructured":"Ferrer\u00a0Fioriti, L.L.M., Hermanns, H.: Probabilistic Termination: Soundness, Completeness, and Compositionality. In: Proc. of POPL (2015). https:\/\/doi.org\/10.1145\/2676726.2677001","DOI":"10.1145\/2676726.2677001"},{"key":"18_CR20","doi-asserted-by":"publisher","unstructured":"Fremont, D.J., Dreossi, T., Ghosh, S., Yue, X., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Scenic: a language for scenario specification and scene generation. In: Proc. of PLDI (2019). https:\/\/doi.org\/10.1145\/3314221.3314633","DOI":"10.1145\/3314221.3314633"},{"key":"18_CR21","doi-asserted-by":"publisher","unstructured":"Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Pl\u00fccker, M., Schneider-Kamp, P., Str\u00f6der, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with aprove. J. Autom. Reasoning (2017). https:\/\/doi.org\/10.1007\/s10817-016-9388-y","DOI":"10.1007\/s10817-016-9388-y"},{"key":"18_CR22","doi-asserted-by":"publisher","unstructured":"Giesl, J., Giesl, P., Hark, M.: Computing expected runtimes for constant probability programs. In: Proc. of CADE (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_16","DOI":"10.1007\/978-3-030-29436-6_16"},{"key":"18_CR23","doi-asserted-by":"publisher","unstructured":"Gruntz, D.: On computing limits in a symbolic manipulation system. Ph.D. thesis, ETH Z\u00fcrich (1996). https:\/\/doi.org\/10.3929\/ETHZ-A-001631582","DOI":"10.3929\/ETHZ-A-001631582"},{"key":"18_CR24","doi-asserted-by":"publisher","unstructured":"Hark, M., Frohn, F., Giesl, J.: Polynomial loops: Beyond termination. In: Proc. of LPAR (2020). https:\/\/doi.org\/10.29007\/nxv1","DOI":"10.29007\/nxv1"},{"key":"18_CR25","doi-asserted-by":"publisher","unstructured":"Hark, M., Kaminski, B.L., Giesl, J., Katoen, J.: Aiming low is harder: induction for lower bounds in probabilistic program verification. In: Proc. of POPL (2020). https:\/\/doi.org\/10.1145\/3371105","DOI":"10.1145\/3371105"},{"key":"18_CR26","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Chen, Y., Dietsch, D., Greitschus, M., Hoenicke, J., Li, Y., Nutz, A., Musa, B., Schilling, C., Schindler, T., Podelski, A.: Ultimate automizer and the search for perfect interpolants - (competition contribution). In: Proc. of TACAS (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_30","DOI":"10.1007\/978-3-319-89963-3_30"},{"key":"18_CR27","doi-asserted-by":"publisher","unstructured":"Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Commun. ACM (1969). https:\/\/doi.org\/10.1145\/363235.363259","DOI":"10.1145\/363235.363259"},{"key":"18_CR28","doi-asserted-by":"publisher","unstructured":"Huang, M., Fu, H., Chatterjee, K.: New Approaches for Almost-Sure Termination of Probabilistic Programs. In: Proc. of APLAS (2018). https:\/\/doi.org\/10.1007\/978-3-030-02768-1_11","DOI":"10.1007\/978-3-030-02768-1_11"},{"key":"18_CR29","doi-asserted-by":"publisher","unstructured":"Huang, M., Fu, H., Chatterjee, K., Goharshady, A.K.: Modular verification for almost-sure termination of probabilistic programs. Proc. ACM Program. Lang. (2019). https:\/\/doi.org\/10.1145\/3360555","DOI":"10.1145\/3360555"},{"key":"18_CR30","doi-asserted-by":"publisher","unstructured":"Kaminski, B.L., Katoen, J.P.: On the hardness of almost-sure termination. In: Proc. of MFCS (2015). https:\/\/doi.org\/10.1007\/978-3-662-48057-1_24","DOI":"10.1007\/978-3-662-48057-1_24"},{"key":"18_CR31","doi-asserted-by":"publisher","unstructured":"Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM (2018). https:\/\/doi.org\/10.1145\/3208102","DOI":"10.1145\/3208102"},{"key":"18_CR32","doi-asserted-by":"crossref","unstructured":"Kauers, M., Paule, P.: The Concrete Tetrahedron: Symbolic Sums, Recurrence Equations, Generating Functions, Asymptotic Estimates. Springer (2011)","DOI":"10.1007\/978-3-7091-0445-3"},{"key":"18_CR33","doi-asserted-by":"crossref","unstructured":"Kemeny, J.G., Snell, J.L., Knapp, A.W.: Denumerable Markov Chains: with a chapter of Markov Random Fields by David Griffeath. Springer, 2 edn. (1976)","DOI":"10.1007\/978-1-4684-9455-6"},{"key":"18_CR34","doi-asserted-by":"publisher","unstructured":"Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. (1981). https:\/\/doi.org\/10.1016\/0022-0000(81)90036-2","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"18_CR35","doi-asserted-by":"publisher","unstructured":"Kozen, D.: A probabilistic PDL. J. Comput. Syst. Sci. (1985). https:\/\/doi.org\/10.1016\/0022-0000(85)90012-1","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"18_CR36","doi-asserted-by":"publisher","unstructured":"Leng\u00e1l, O., Lin, A.W., Majumdar, R., R\u00fcmmer, P.: Fair termination for parameterized probabilistic concurrent systems. In: Proc. of TACAS (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_29","DOI":"10.1007\/978-3-662-54577-5_29"},{"key":"18_CR37","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer (2005)","DOI":"10.1145\/1059816.1059824"},{"key":"18_CR38","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.P.: A New Proof Rule for Almost-sure Termination. Proc. ACM Program. Lang. (2018). https:\/\/doi.org\/10.1145\/3158121","DOI":"10.1145\/3158121"},{"key":"18_CR39","doi-asserted-by":"publisher","unstructured":"Monniaux, D.: An abstract analysis of the probabilistic termination of programs. In: Proc. of SAS (2001). https:\/\/doi.org\/10.1007\/3-540-47764-0","DOI":"10.1007\/3-540-47764-0"},{"key":"18_CR40","doi-asserted-by":"crossref","unstructured":"Moosbrugger, M., Bartocci, E., Katoen, J.P., Kov\u00e1cs, L.: Automated termination analysis of polynomial probabilistic programs (2020)","DOI":"10.26226\/morressier.604907f41a80aac83ca25d19"},{"key":"18_CR41","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Proc. of TACAS (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3","DOI":"10.1007\/978-3-540-78800-3"},{"key":"18_CR42","doi-asserted-by":"publisher","unstructured":"Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: resource analysis for probabilistic programs. In: Proc. of PLDI (2018). https:\/\/doi.org\/10.1145\/3192366.3192394","DOI":"10.1145\/3192366.3192394"},{"key":"18_CR43","doi-asserted-by":"publisher","unstructured":"Takisaka, T., Oyabu, Y., Urabe, N., Hasuo, I.: Ranking and repulsing supermartingales for reachability in probabilistic programs. In: Proc. of ATVA (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_28","DOI":"10.1007\/978-3-030-01090-4_28"},{"key":"18_CR44","doi-asserted-by":"publisher","unstructured":"Yamada, A., Kusakari, K., Sakabe, T.: Nagoya termination tool. In: Proc. of RTA-TLCA (2014). https:\/\/doi.org\/10.1007\/978-3-319-08918-8_32","DOI":"10.1007\/978-3-319-08918-8_32"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72019-3_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,25]],"date-time":"2021-10-25T03:07:48Z","timestamp":1635131268000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-72019-3_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720186","9783030720193"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72019-3_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"79","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"24","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-5","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference took place virtually due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}