{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T19:33:56Z","timestamp":1757619236565,"version":"3.44.0"},"publisher-location":"Cham","reference-count":63,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031986789"},{"type":"electronic","value":"9783031986796"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T00:00:00Z","timestamp":1753142400000},"content-version":"vor","delay-in-days":202,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This paper introduces <jats:italic>k<\/jats:italic>-d PCPs \u2013 the class of <jats:italic>probabilistic counter programs<\/jats:italic> with <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$k \\in \\mathbb {N}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>k<\/mml:mi>\n                    <mml:mo>\u2208<\/mml:mo>\n                    <mml:mi>N<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> counter variables inducing possibly infinite-state Markov chains. We show that the universal (positive) almost-sure termination problem is <jats:italic>undecidable<\/jats:italic> for <jats:italic>k<\/jats:italic>-d PCPs in general, yet <jats:italic>decidable<\/jats:italic> for 1-d PCPs. We present an efficient decision procedure for the latter leveraging the technique of <jats:italic>Markov chain finitization<\/jats:italic>. Moreover, we identify several classes of <jats:italic>k<\/jats:italic>-d PCPs that are reducible to 1-d PCPs \u2013 thus their termination properties can be inferred automatically. Experiments demonstrate that our decision procedure can certify (positive) almost-sure termination \u2013 without resorting to invariants or supermartingales \u2013 of non-trivial probabilistic programs beyond the scope of existing tools.<\/jats:p>","DOI":"10.1007\/978-3-031-98679-6_4","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T09:19:04Z","timestamp":1753089544000},"page":"82-104","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["On the\u00a0Almost-Sure Termination of\u00a0Probabilistic Counter Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-5934-0806","authenticated-orcid":false,"given":"Sergei","family":"Novozhilov","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0004-5304-6763","authenticated-orcid":false,"given":"Mingqi","family":"Yang","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9663-7441","authenticated-orcid":false,"given":"Mingshuai","family":"Chen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0000-5632-9479","authenticated-orcid":false,"given":"Zhiyang","family":"Li","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4703-7348","authenticated-orcid":false,"given":"Jianwei","family":"Yin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"4_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":"4_CR2","doi-asserted-by":"publisher","first-page":"963","DOI":"10.1007\/978-3-319-10575-8_28","volume-title":"Handbook of Model Checking","author":"C Baier","year":"2018","unstructured":"Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Handbook of Model Checking, pp. 963\u2013999. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Barthe, G., Katoen, J., Silva, A. (eds.): Foundations of Probabilistic Programming. Cambridge University Press (2020)","DOI":"10.1017\/9781108770750"},{"key":"4_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-8176-8421-1","volume-title":"An Introduction to Queueing Theory: Modeling and Analysis in Applications","author":"UN Bhat","year":"2015","unstructured":"Bhat, U.N.: An Introduction to Queueing Theory: Modeling and Analysis in Applications. Statistics for Industry and Technology, Birkh\u00e4user, Boston, MA (2015)"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Bohnenkamp, H.C., van\u00a0der Stok, P., Hermanns, H., Vaandrager, F.W.: Cost-optimization of the IPV4 Zeroconf protocol. In: DSN, pp. 531\u2013540. IEEE Computer Society (2003)","DOI":"10.1109\/DSN.2003.1209963"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Bozga, M., Iosif, R., Konecn\u00fd, F.: Deciding conditional termination. Log. Methods Comput. Sci. 10(3), 252\u2013266 (2014)","DOI":"10.2168\/LMCS-10(3:8)2014"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/11817963_34","volume-title":"Computer Aided Verification","author":"M Braverman","year":"2006","unstructured":"Braverman, M.: Termination of integer linear programs. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 372\u2013385. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_34"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Brozek, V., Etessami, K., Kucera, A., Wojtczak, D.: One-counter Markov decision processes. In: SODA, pp. 863\u2013874. SIAM (2010)","DOI":"10.1137\/1.9781611973075.70"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-22110-1_18","volume-title":"Computer Aided Verification","author":"T Br\u00e1zdil","year":"2011","unstructured":"Br\u00e1zdil, T., Kiefer, S., Ku\u010dera, A.: Efficient analysis of probabilistic programs with an unbounded counter. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 208\u2013224. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_18"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-642-39799-8_34","volume-title":"Computer Aided Verification","author":"A Chakarov","year":"2013","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 511\u2013526. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-41528-4_1","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2016","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic programs through Positivstellensatz\u2019s. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 3\u201322. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_1"},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Goharshady, A.K., Meggendorfer, T., Zikelic, D.: Sound and complete certificates for quantitative termination analysis of probabilistic programs. In: CAV (1). LNCS, vol. 13371, pp. 55\u201378. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_4","DOI":"10.1007\/978-3-031-13185-1_4"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Novotn\u00fd, P., Zikelic, D.: Stochastic invariants for probabilistic termination. In: POPL, pp. 145\u2013160. ACM (2017)","DOI":"10.1145\/3009837.3009873"},{"issue":"2","key":"4_CR14","doi-asserted-by":"publisher","first-page":"345","DOI":"10.2307\/2371045","volume":"58","author":"A Church","year":"1936","unstructured":"Church, A.: An unsolvable problem of elementary number theory. Am. J. Math. 58(2), 345\u2013363 (1936)","journal-title":"Am. J. Math."},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"MA Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420\u2013432. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_39"},{"issue":"1","key":"4_CR16","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/BF02011875","volume":"19","author":"M Coppo","year":"1978","unstructured":"Coppo, M., Dezani-Ciancaglini, M.: A new type assignment for $$\\lambda $$-terms. Arch. Math. Log. 19(1), 139\u2013156 (1978)","journal-title":"Arch. Math. Log."},{"issue":"2\u20136","key":"4_CR17","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1002\/malq.19810270205","volume":"27","author":"M Coppo","year":"1981","unstructured":"Coppo, M., Dezani-Ciancaglini, M., Venneri, B.: Functional characters of solvable terms. Math. Log. Q. 27(2\u20136), 45\u201358 (1981)","journal-title":"Math. Log. Q."},{"key":"4_CR18","unstructured":"Dudenhefner, A.: Certified decision procedures for two-counter machines. In: FSCD. LIPIcs, vol.\u00a0228, pp. 16:1\u201316:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"4_CR19","unstructured":"Ershov, A.P.: On operator algorithms. Doklady Akademii Nauk SSSR 122, 967\u2013970 (1958). English translation in Automat. Express 1, 20\u201323 (1959)"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Esparza, J., Kucera, A., Mayr, R.: Model checking probabilistic pushdown automata. In: LICS, pp. 12\u201321. IEEE Computer Society (2004)","DOI":"10.1109\/LICS.2004.1319596"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Etessami, K., Yannakakis, M.: Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. J. ACM 56(1), 1:1\u20131:66 (2009)","DOI":"10.1145\/1462153.1462154"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Everest, G., van\u00a0der Poorten, A.J., Shparlinski, I.E., Ward, T.: Recurrence Sequences, Mathematical surveys and monographs, vol.\u00a0104. American Mathematical Society (2003)","DOI":"10.1090\/surv\/104"},{"issue":"OOPSLA1","key":"4_CR23","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1145\/3586051","volume":"7","author":"S Feng","year":"2023","unstructured":"Feng, S., Chen, M., Su, H., Kaminski, B.L., Katoen, J., Zhan, N.: Lower bounds for possibly divergent probabilistic programs. Proc. ACM Program. Lang. 7(OOPSLA1), 696\u2013726 (2023)","journal-title":"Proc. ACM Program. Lang."},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/978-3-030-25543-5_24","volume-title":"Computer Aided Verification","author":"F Frohn","year":"2019","unstructured":"Frohn, F., Giesl, J.: Termination of triangular integer loops is decidable. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 426\u2013444. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_24"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-030-29436-6_16","volume-title":"Automated Deduction \u2013 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.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 269\u2013286. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_16"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: FOSE, pp. 167\u2013181. ACM (2014)","DOI":"10.1145\/2593882.2593900"},{"issue":"1","key":"4_CR27","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/s10998-020-00363-w","volume":"83","author":"K Gryszka","year":"2021","unstructured":"Gryszka, K.: From biased coin to any discrete distribution. Period. Math. Hung. 83(1), 71\u201380 (2021)","journal-title":"Period. Math. Hung."},{"key":"4_CR28","unstructured":"Hagberg, A.A., Schult, D.A., Swart, P.J.: Exploring network structure, dynamics, and function using networkX. Tech. rep, Los Alamos National Laboratory (LANL), Los Alamos, NM, USA (2008)"},{"issue":"3","key":"4_CR29","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1016\/j.dam.2005.10.009","volume":"154","author":"V Halava","year":"2006","unstructured":"Halava, V., Harju, T., Hirvensalo, M.: Positivity of second order linear recurrent sequences. Discret. Appl. Math. 154(3), 447\u2013451 (2006)","journal-title":"Discret. Appl. Math."},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-58085-9_75","volume-title":"Types for Proofs and Programs","author":"L Helmink","year":"1994","unstructured":"Helmink, L., Sellink, M., Vaandrager, F.W.: Proof-checking a data link protocol. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 127\u2013165. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58085-9_75"},{"key":"4_CR31","unstructured":"Hermes, H.: Die universalit\u00e4t programmgesteuerter rechenmaschinen. Mathematisch-Physikalische Semesterberichte 4, 42\u201353 (1954)"},{"issue":"4","key":"4_CR32","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1080\/07468342.1997.11973878","volume":"28","author":"HP Hirst","year":"1997","unstructured":"Hirst, H.P., Macey, W.T.: Bounding the roots of polynomials. Coll. Math. J. 28(4), 292\u2013295 (1997)","journal-title":"Coll. Math. J."},{"key":"4_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"781","DOI":"10.1007\/978-3-642-31424-7_64","volume-title":"Computer Aided Verification","author":"J Hoffmann","year":"2012","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Resource aware ML. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 781\u2013786. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_64"},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"Holtzen, S., den Broeck, G.V., Millstein, T.D.: Scaling exact inference for discrete probabilistic programs. Proc. ACM Program. Lang. 4(OOPSLA), 140:1\u2013140:31 (2020)","DOI":"10.1145\/3428208"},{"issue":"3","key":"4_CR35","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/s00236-018-0321-1","volume":"56","author":"BL Kaminski","year":"2019","unstructured":"Kaminski, B.L., Katoen, J., Matheja, C.: On the hardness of analyzing probabilistic programs. Acta Informatica 56(3), 255\u2013285 (2019)","journal-title":"Acta Informatica"},{"key":"4_CR36","unstructured":"Knuth, D.E., Yao, A.C.: The complexity of nonuniform random number generation. In: Algorithms and Complexity: New Directions and Recent Results. Academic Press (1976)"},{"issue":"2","key":"4_CR37","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/S0304-3975(96)00080-1","volume":"168","author":"I Korec","year":"1996","unstructured":"Korec, I.: Small universal register machines. Theor. Comput. Sci. 168(2), 267\u2013301 (1996)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"4_CR38","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1016\/0022-0000(81)90036-2","volume":"22","author":"D Kozen","year":"1981","unstructured":"Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328\u2013350 (1981)","journal-title":"J. Comput. Syst. Sci."},{"issue":"3","key":"4_CR39","doi-asserted-by":"publisher","first-page":"295","DOI":"10.4153\/CMB-1961-032-6","volume":"4","author":"J Lambek","year":"1961","unstructured":"Lambek, J.: How to program an infinite abacus. Math. Bull. 4(3), 295\u2013302 (1961)","journal-title":"Math. Bull."},{"key":"4_CR40","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898719734","volume-title":"Introduction to Matrix Analytic Methods in Stochastic Modeling","author":"G Latouche","year":"1999","unstructured":"Latouche, G., Ramaswami, V.: Introduction to Matrix Analytic Methods in Stochastic Modeling. SIAM, ASA-SIAM Series on Statistics and Applied Mathematics (1999)"},{"key":"4_CR41","doi-asserted-by":"publisher","unstructured":"Lommen, N., Meyer, \u00c9., Giesl, J.: Control-flow refinement for complexity analysis of probabilistic programs in Koat (short paper). In: IJCAR (1). LNCS, vol. 14739, pp. 233\u2013243. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_14","DOI":"10.1007\/978-3-031-63498-7_14"},{"key":"4_CR42","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Sathiyanarayana, V.R.: Positive almost-sure termination: complexity and proof rules. Proc. ACM Program. Lang. 8(POPL), 1089\u20131117 (2024)","DOI":"10.1145\/3632879"},{"key":"4_CR43","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":"4_CR44","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C.: Abstraction, refinement and proof for probabilistic systems. Monographs in Computer Science, Springer (2005). https:\/\/doi.org\/10.1007\/b138392","DOI":"10.1007\/b138392"},{"key":"4_CR45","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C.: Introduction to PGCL: its logic and its model. In: Refinement Techniques in Software Engineering. Springer (2005). https:\/\/doi.org\/10.1007\/0-387-27006-X_1","DOI":"10.1007\/0-387-27006-X_1"},{"key":"4_CR46","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":"4_CR47","unstructured":"van\u00a0de Meent, J.W., Paige, B., Yang, H., Wood, F.: An introduction to probabilistic programming (2021). https:\/\/arxiv.org\/abs\/1809.10756"},{"key":"4_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-030-72016-2_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Meyer","year":"2021","unstructured":"Meyer, F., Hark, M., Giesl, J.: Inferring expected runtimes of probabilistic integer programs using expected sizes. In: TACAS 2021. LNCS, vol. 12651, pp. 250\u2013269. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_14"},{"key":"4_CR49","unstructured":"Meyer, P.J.: Probably: probabilistic guarded command language (PGCL) documentation (2023). https:\/\/philipp15b.github.io\/probably\/pgcl.html. Accessed 25 Oct 2023"},{"key":"4_CR50","unstructured":"Minsky, M.: Recursive unsolvability of post\u2019s problem. Tech. Rep. 54G-0023, Massachusetts Institute of Technology, Lincoln Laboratory (1954)"},{"key":"4_CR51","volume-title":"Computation: Finite and Infinite Machines","author":"ML Minsky","year":"1967","unstructured":"Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall, Englewood Cliffs, NJ, USA (1967)"},{"key":"4_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1007\/978-3-030-90870-6_36","volume-title":"Formal Methods","author":"M Moosbrugger","year":"2021","unstructured":"Moosbrugger, M., Bartocci, E., Katoen, J.-P., Kov\u00e1cs, L.: The probabilistic termination tool amber. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 667\u2013675. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_36"},{"key":"4_CR53","doi-asserted-by":"crossref","unstructured":"Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: resource analysis for probabilistic programs. In: PLDI, pp. 496\u2013512. ACM (2018)","DOI":"10.1145\/3192366.3192394"},{"key":"4_CR54","unstructured":"Novozhilov, S., Yang, M., Chen, M., Li, Z., Yin, J.: On the almost-sure termination of probabilistic counter programs (2025). https:\/\/hal.science\/hal-05082395, hal preprint hal-05082395"},{"key":"4_CR55","doi-asserted-by":"crossref","unstructured":"Olmedo, F., Gretz, F., Jansen, N., Kaminski, B.L., Katoen, J., McIver, A.: Conditioning in probabilistic programming. ACM Trans. Program. Lang. Syst. 40(1), 4:1\u20134:50 (2018)","DOI":"10.1145\/3156018"},{"key":"4_CR56","doi-asserted-by":"publisher","unstructured":"Ost, A.: Quasi-birth-and-death processes. In: Performance of Communication Systems: A Model-Based Approach with Matrix-Geometric Methods, pp. 51\u2013102. Springer, Berlin, Heidelberg (2001). https:\/\/doi.org\/10.1007\/978-3-662-04421-6_4","DOI":"10.1007\/978-3-662-04421-6_4"},{"issue":"2","key":"4_CR57","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1145\/2766189.2766191","volume":"2","author":"J Ouaknine","year":"2015","unstructured":"Ouaknine, J., Worrell, J.: On linear recurrence sequences and loop termination. ACM SIGLOG News 2(2), 4\u201313 (2015)","journal-title":"ACM SIGLOG News"},{"key":"4_CR58","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Sousa-Pinto, J., Worrell, J.: On termination of integer linear loops 2015 (2014)","DOI":"10.1137\/1.9781611973730.65"},{"key":"4_CR59","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1111\/j.1746-8361.1958.tb01470.x","volume":"12","author":"R P\u00e9ter","year":"1958","unstructured":"P\u00e9ter, R.: Graphschemata und rekursive funktionen. Dialectica 12, 373 (1958)","journal-title":"Dialectica"},{"issue":"2","key":"4_CR60","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/321160.321170","volume":"10","author":"JC Shepherdson","year":"1963","unstructured":"Shepherdson, J.C., Sturgis, H.E.: Computability of recursive functions. J. ACM 10(2), 217\u2013255 (1963)","journal-title":"J. ACM"},{"key":"4_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-540-27813-9_6","volume-title":"Computer Aided Verification","author":"A Tiwari","year":"2004","unstructured":"Tiwari, A.: Termination of linear programs. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 70\u201382. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_6"},{"key":"4_CR62","doi-asserted-by":"crossref","unstructured":"Turing, A.M.: On computable numbers, with an application to the entscheidungs problem. Proc. London Math. Soc. s2-42(1), 230\u2013265 (1937)","DOI":"10.1112\/plms\/s2-42.1.230"},{"key":"4_CR63","doi-asserted-by":"crossref","unstructured":"Virtanen, P., et al.: SciPy 1.0 Contributors: SciPy 1.0: Fundamental algorithms for scientific computing in Python. Nat. Methods 17, 261\u2013272 (2020)","DOI":"10.1038\/s41592-020-0772-5"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98679-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,7]],"date-time":"2025-09-07T16:18:05Z","timestamp":1757261885000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98679-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986789","9783031986796"],"references-count":63,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98679-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"22 July 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":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","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":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}