{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,2]],"date-time":"2025-10-02T00:41:12Z","timestamp":1759365672326,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032057914","type":"print"},{"value":"9783032057921","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,2]],"date-time":"2025-10-02T00:00:00Z","timestamp":1759363200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,2]],"date-time":"2025-10-02T00:00:00Z","timestamp":1759363200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-05792-1_15","type":"book-chapter","created":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T10:31:33Z","timestamp":1759314693000},"page":"275-292","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Positive Almost-Sure Termination of\u00a0Polynomial Random Walks"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-0177-2764","authenticated-orcid":false,"given":"Lorenz","family":"Winkler","sequence":"first","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":[[2025,10,2]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Agrawal, S., Chatterjee, K., Novotn\u00fd, P.: Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. Proc. ACM Program. Lang. 2(POPL), 34:1\u201334:32 (2018)","DOI":"10.1145\/3158122"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Avanzini, M., Moser, G., Schaper, M.: A modular cost analysis for probabilistic programs. Proc. ACM Program. Lang. 4(OOPSLA) (2020)","DOI":"10.1145\/3428240"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Bournez, O., Garnier, F.: Proving positive almost-sure termination. In: RTA, pp. 323\u2013337 (2005)","DOI":"10.1007\/978-3-540-32033-3_24"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: CAV, pp. 511\u2013526 (2013)","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic programs through positivstellensatz\u2019s. In: CAV, pp. 3\u201322 (2016)","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Novotn\u00fd, P., \u017dikeli\u0107, D.: Stochastic invariants for probabilistic termination. In: POPL, pp. 145\u2013160 (2017)","DOI":"10.1145\/3009837.3009873"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Durrett, R.: Probability: Theory and Examples. Cambridge University Press (2019)","DOI":"10.1017\/9781108591034"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Fioriti, L.M.F., Hermanns, H.: Probabilistic termination: soundness, completeness, and compositionality. In: POPL, pp. 489\u2013501. ACM (2015)","DOI":"10.1145\/2676726.2677001"},{"key":"15_CR9","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-030-29436-6_16","volume-title":"Automated Deduction - CADE 27","author":"J Giesl","year":"2019","unstructured":"Giesl, J., Giesl, P., Hark, M.: Computing expected runtimes for constant probability programs. In: Fontaine, P. (ed.) Automated Deduction - CADE 27, pp. 269\u2013286. Springer International Publishing, Cham (2019)"},{"key":"15_CR10","unstructured":"Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2025). https:\/\/www.gurobi.com"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Harchol-Balter, M.: Introduction to Probability for Computing. Cambridge University Press (2023)","DOI":"10.1017\/9781009309097"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Hark, M., Kaminski, B.L., Giesl, J., Katoen, J.: Aiming low is harder: induction for lower bounds in probabilistic program verification. Proc. ACM Program. Lang. 4(POPL), 37:1\u201337:28 (2020)","DOI":"10.1145\/3371105"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Kaminski, B.L., Katoen, J.P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM 65(5) (2018)","DOI":"10.1145\/3208102"},{"key":"15_CR14","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1","volume-title":"A probabilistic PDL","author":"D Kozen","year":"1985","unstructured":"Kozen, D.: A probabilistic PDL. J. Comput. Syst, Sci (1985)"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Lommen, N., Meyer, \u00c9., Giesl, J.: Control-flow refinement for complexity analysis of probabilistic programs in KoAT (short paper). In: IJCAR, pp. 233\u2013243 (2024)","DOI":"10.1007\/978-3-031-63498-7_14"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Sathiyanarayana, V.R.: Positive almost-sure termination: Complexity and proof rules. Proc. ACM Program. Lang. 8(POPL) (2024)","DOI":"10.1145\/3632879"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Sathiyanarayana, V.R.: Sound and complete proof rules for probabilistic termination. Proc. ACM Program. Lang. 9(POPL), 1871\u20131902 (2025)","DOI":"10.1145\/3704899"},{"key":"15_CR18","volume-title":"Abstraction","author":"A McIver","year":"2005","unstructured":"McIver, A., Morgan, C.: Abstraction. Springer, Refinement and Proof for Probabilistic Systems (2005)"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.: A new proof rule for almost-sure termination. Proc. ACM Program. Lang. 2(POPL), 33:1\u201333:28 (2018)","DOI":"10.1145\/3158121"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Meyer, F., Hark, M., Giesl, J.: Inferring expected runtimes of probabilistic integer programs using expected sizes. In: TACAS, pp. 250\u2013269 (2021)","DOI":"10.1007\/978-3-030-72016-2_14"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Moosbrugger, M., Bartocci, E., Katoen, J.P., Kov\u00e1cs, L.: The probabilistic termination tool Amber. In: FM, pp. 667\u2013675 (2021)","DOI":"10.1007\/978-3-030-90870-6_36"},{"issue":"OOPSLA2","key":"15_CR22","doi-asserted-by":"publisher","first-page":"1497","DOI":"10.1145\/3563341","volume":"6","author":"M Moosbrugger","year":"2022","unstructured":"Moosbrugger, M., Stankovic, M., Bartocci, E., Kov\u00e1cs, L.: This is the moment for probabilistic loops. Proc. ACM Program. Lang. 6(OOPSLA2), 1497\u20131525 (2022)","journal-title":"Proc. ACM Program. Lang."},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: resource analysis for probabilistic programs. In: PLDI, pp. 496\u2013512 (2018)","DOI":"10.1145\/3192366.3192394"},{"key":"15_CR24","unstructured":"Perron, L., Furnon, V.: Or-tools. https:\/\/developers.google.com\/optimization\/"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Takisaka, T., Zhang, L., Wang, C., Liu, J.: Lexicographic ranking supermartingales with lazy lower bounds. In: CAV, pp. 420\u2013442 (2024)","DOI":"10.1007\/978-3-031-65633-0_19"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Venables, W.N., Ripley, B.D.: Modern Applied Statistics with S. Springer, New York, fourth edn. (2002). https:\/\/www.stats.ox.ac.uk\/pub\/MASS4\/","DOI":"10.1007\/978-0-387-21706-2"},{"key":"15_CR27","unstructured":"Winkler, L., Kov\u00e1cs, L.: Positive Almost-Sure Termination of Polynomial Random Walks (2025). https:\/\/arxiv.org\/abs\/2504.19575"}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-05792-1_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T10:31:39Z","timestamp":1759314699000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-05792-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,2]]},"ISBN":["9783032057914","9783032057921"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-05792-1_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,2]]},"assertion":[{"value":"2 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"QEST+FORMATS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Aarhus","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Denmark","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 August 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 August 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"qest2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.qest-formats.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}