{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:58:39Z","timestamp":1764403119904,"version":"3.40.3"},"publisher-location":"Cham","reference-count":80,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030908690"},{"type":"electronic","value":"9783030908706"}],"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:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-90870-6_33","type":"book-chapter","created":{"date-parts":[[2021,11,10]],"date-time":"2021-11-10T00:06:44Z","timestamp":1636502804000},"page":"619-639","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["On Lexicographic Proof Rules for Probabilistic Termination"],"prefix":"10.1007","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[]},{"given":"Ehsan Kafshdar","family":"Goharshady","sequence":"additional","affiliation":[]},{"given":"Petr","family":"Novotn\u00fd","sequence":"additional","affiliation":[]},{"given":"Ji\u0159\u00ed","family":"Z\u00e1rev\u00facky","sequence":"additional","affiliation":[]},{"given":"\u0110or\u0111e","family":"\u017dikeli\u0107","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,11,10]]},"reference":[{"key":"33_CR1","doi-asserted-by":"crossref","unstructured":"Agrawal, S., Chatterjee, K., Novotn\u00fd, P.: Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. PACMPL 2(POPL), 34:1\u201334:32 (2018)","DOI":"10.1145\/3158122"},{"key":"33_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-642-15769-1_8","volume-title":"Static Analysis","author":"C Alias","year":"2010","unstructured":"Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 117\u2013133. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15769-1_8"},{"key":"33_CR3","unstructured":"Ash, R., Dol\u00e9ans-Dade, C.: Probability and Measure Theory. Harcourt\/Academic Press, Boston (2000)"},{"key":"33_CR4","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Dal Lago, U., Ghyselen, A.: Type-based complexity analysis of probabilistic functional programs. In: 2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 1\u201313 (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785725","DOI":"10.1109\/LICS.2019.8785725"},{"key":"33_CR5","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2019.102338","volume":"185","author":"M Avanzini","year":"2020","unstructured":"Avanzini, M., Lago, U.D., Yamada, A.: On probabilistic term rewriting. Sci. Comput. Program. 185, 102338 (2020). https:\/\/doi.org\/10.1016\/j.scico.2019.102338","journal-title":"Sci. Comput. Program."},{"key":"33_CR6","doi-asserted-by":"crossref","unstructured":"Avanzini, M., Moser, G., Schaper, M.: A modular cost analysis for probabilistic programs. In: Proceedings of the ACM on Programming Languages, vol. 4 ((Proceedings of OOPSLA 2020)), pp. 1\u201330 (2020)","DOI":"10.1145\/3428240"},{"key":"33_CR7","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"key":"33_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-319-41528-4_3","volume-title":"Computer Aided Verification","author":"G Barthe","year":"2016","unstructured":"Barthe, G., Espitau, T., Ferrer Fioriti, L.M., Hsu, J.: Synthesizing probabilistic invariants via Doob\u2019s decomposition. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 43\u201361. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_3"},{"key":"33_CR9","doi-asserted-by":"publisher","unstructured":"Barthe, G., Gaboardi, M., Gr\u00e9goire, B., Hsu, J., Strub, P.Y.: Proving differential privacy via probabilistic couplings. In: Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 749\u2013758, LICS 2016. ACM, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2933575.2934554","DOI":"10.1145\/2933575.2934554"},{"key":"33_CR10","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gaboardi, M., Hsu, J., Pierce, B.: Programming language techniques for differential privacy. ACM SIGLOG News 3(1), 34\u201353 (2016)","DOI":"10.1145\/2893582.2893591"},{"key":"33_CR11","doi-asserted-by":"publisher","unstructured":"Ben-Amram, A.M., Genaim, S.: 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, pp. 51\u201362, POPL 2013. ACM, New York, NY, USA (2013). https:\/\/doi.org\/10.1145\/2429069.2429078","DOI":"10.1145\/2429069.2429078"},{"key":"33_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-319-21668-3_18","volume-title":"Computer Aided Verification","author":"AM Ben-Amram","year":"2015","unstructured":"Ben-Amram, A.M., Genaim, S.: Complexity of Bradley-Manna-Sipma lexicographic ranking functions. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 304\u2013321. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_18"},{"key":"33_CR13","unstructured":"Billingsley, P.: Probability and Measure, 3rd edn. Wiley, New York (1995)"},{"key":"33_CR14","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":"33_CR15","doi-asserted-by":"publisher","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, 6\u201310 July 2005, Proceedings, pp. 491\u2013504 (2005). https:\/\/doi.org\/10.1007\/11513988_48","DOI":"10.1007\/11513988_48"},{"key":"33_CR16","doi-asserted-by":"publisher","unstructured":"Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13\u201319, 2013, Proceedings, pp. 413\u2013429 (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_28","DOI":"10.1007\/978-3-642-39799-8_28"},{"key":"33_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-662-49674-9_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Brockschmidt","year":"2016","unstructured":"Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., Piterman, N.: T2: temporal property verification. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 387\u2013393. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_22"},{"key":"33_CR18","doi-asserted-by":"crossref","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: CAV 2013, pp. 511\u2013526 (2013)","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"33_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-662-49674-9_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Chakarov","year":"2016","unstructured":"Chakarov, A., Voronin, Y.-L., Sankaranarayanan, S.: Deductive proofs of almost sure persistence and recurrence properties. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 260\u2013279. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_15"},{"key":"33_CR20","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":"33_CR21","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. 40(2), 7:1\u20137:45 (2018). https:\/\/doi.org\/10.1145\/3174800","DOI":"10.1145\/3174800"},{"key":"33_CR22","unstructured":"Chatterjee, K., Goharshady, E.K., Novotn\u00fd, P., Z\u00e1rev\u00facky, J., \u017dikeli\u0107, D.: On lexicographic proof rules for probabilistic termination (2021). https:\/\/arxiv.org\/abs\/2108.02188"},{"key":"33_CR23","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Novotn\u00fd, P., \u017dikeli\u0107, D.: Stochastic invariants for probabilistic termination. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 145\u2013160, POPL 2017. ACM, New York, NY, USA (2017). https:\/\/doi.org\/10.1145\/3009837.3009873","DOI":"10.1145\/3009837.3009873"},{"key":"33_CR24","doi-asserted-by":"publisher","unstructured":"Chen, J., He, F.: Proving almost-sure termination by omega-regular decomposition. In: Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15\u201320, 2020, pp. 869\u2013882 (2020). https:\/\/doi.org\/10.1145\/3385412.3386002","DOI":"10.1145\/3385412.3386002"},{"key":"33_CR25","doi-asserted-by":"crossref","unstructured":"Claret, G., Rajamani, S.K., Nori, A.V., Gordon, A.D., Borgstr\u00f6m, J.: Bayesian inference using data flow analysis. In: Joint Meeting on Foundations of Software Engineering, pp. 92\u2013102. ACM (2013)","DOI":"10.1145\/2491411.2491423"},{"key":"33_CR26","doi-asserted-by":"publisher","unstructured":"Col\u00f3n, M., Sipma, H.: Synthesis of linear ranking functions. In: Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2\u20136, 2001, Proceedings, pp. 67\u201381 (2001). https:\/\/doi.org\/10.1007\/3-540-45319-9_6","DOI":"10.1007\/3-540-45319-9_6"},{"issue":"6","key":"33_CR27","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1145\/1133255.1134029","volume":"41","author":"B Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. SIGPLAN Not. 41(6), 415\u2013426 (2006)","journal-title":"SIGPLAN Not."},{"issue":"5","key":"33_CR28","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1145\/1941487.1941509","volume":"54","author":"B Cook","year":"2011","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Proving program termination. Commun. ACM 54(5), 88\u201398 (2011)","journal-title":"Commun. ACM"},{"key":"33_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-642-36742-7_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Cook","year":"2013","unstructured":"Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 47\u201361. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_4"},{"key":"33_CR30","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pp. 238\u2013252 (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"33_CR31","doi-asserted-by":"publisher","unstructured":"Dal Lago, U., Faggian, C., Rocca, S.R.D.: Intersection types and (positive) almost-sure termination. Proc. ACM Program. Lang. 5(POPL), 1\u201332 (2021). https:\/\/doi.org\/10.1145\/3434313","DOI":"10.1145\/3434313"},{"key":"33_CR32","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511581274","volume-title":"Concentration of Measure for the Analysis of Randomized Algorithms","author":"D Dubhashi","year":"2009","unstructured":"Dubhashi, D., Panconesi, A.: Concentration of Measure for the Analysis of Randomized Algorithms, 1st edn. Cambridge University Press, New York (2009)","edition":"1"},{"key":"33_CR33","doi-asserted-by":"crossref","unstructured":"Esparza, J., Gaiser, A., Kiefer, S.: Proving termination of probabilistic programs using patterns. In: CAV 2012, pp. 123\u2013138 (2012)","DOI":"10.1007\/978-3-642-31424-7_14"},{"key":"33_CR34","doi-asserted-by":"crossref","unstructured":"Feldman, Y.A.: A decidable propositional dynamic logic with explicit probabilities. Inf. Control 63(1), 11\u201338 (1984)","DOI":"10.1016\/S0019-9958(84)80039-X"},{"key":"33_CR35","doi-asserted-by":"crossref","unstructured":"Feldman, Y.A., Harel, D.: A probabilistic dynamic logic. In: Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, pp. 181\u2013195. ACM (1982)","DOI":"10.1145\/800070.802191"},{"key":"33_CR36","doi-asserted-by":"publisher","unstructured":"Fioriti, L.M.F., Hermanns, H.: Probabilistic termination: soundness, completeness, and compositionality. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15\u201317, 2015, pp. 489\u2013501 (2015). https:\/\/doi.org\/10.1145\/2676726.2677001","DOI":"10.1145\/2676726.2677001"},{"key":"33_CR37","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume":"19","author":"RW Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. Math. Aspects Comput. Sci. 19, 19\u201333 (1967)","journal-title":"Math. Aspects Comput. Sci."},{"issue":"3","key":"33_CR38","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1214\/aoms\/1177728976","volume":"24","author":"FG Foster","year":"1953","unstructured":"Foster, F.G.: On the stochastic matrices associated with certain queuing processes. Ann. Math. Stat. 24(3), 355\u2013360 (1953)","journal-title":"Ann. Math. Stat."},{"key":"33_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-662-49498-1_12","volume-title":"Programming Languages and Systems","author":"N Foster","year":"2016","unstructured":"Foster, N., Kozen, D., Mamouras, K., Reitblatt, M., Silva, A.: Probabilistic NetKAT. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 282\u2013309. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_12"},{"key":"33_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1007\/978-3-030-11245-5_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H Fu","year":"2019","unstructured":"Fu, H., Chatterjee, K.: Termination of nondeterministic probabilistic programs. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 468\u2013490. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-11245-5_22"},{"issue":"7553","key":"33_CR41","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1038\/nature14541","volume":"521","author":"Z Ghahramani","year":"2015","unstructured":"Ghahramani, Z.: Probabilistic machine learning and artificial intelligence. Nature 521(7553), 452\u2013459 (2015)","journal-title":"Nature"},{"key":"33_CR42","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, Cham (2019)"},{"key":"33_CR43","doi-asserted-by":"publisher","unstructured":"Gonnord, L., Monniaux, D., Radanne, G.: Synthesis of ranking functions using extremal counterexamples. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 608\u2013618, PLDI 2015. ACM, New York, NY, USA (2015). https:\/\/doi.org\/10.1145\/2737924.2737976","DOI":"10.1145\/2737924.2737976"},{"issue":"1","key":"33_CR44","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/2480359.2429119","volume":"48","author":"AD Gordon","year":"2013","unstructured":"Gordon, A.D., Aizatulin, M., Borgstrom, J., Claret, G., Graepel, T., Nori, A.V., Rajamani, S.K., Russo, C.: A model-learner pattern for Bayesian reasoning. ACM SIGPLAN Not. 48(1), 403\u2013416 (2013)","journal-title":"ACM SIGPLAN Not."},{"key":"33_CR45","doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: Proceedings of the on Future of Software Engineering, pp. 167\u2013181. ACM (2014)","DOI":"10.1145\/2593882.2593900"},{"key":"33_CR46","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1016\/j.peva.2013.11.004","volume":"73","author":"F Gretz","year":"2014","unstructured":"Gretz, F., Katoen, J.P., McIver, A.: Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Perform. Eval. 73, 110\u2013132 (2014)","journal-title":"Perform. Eval."},{"key":"33_CR47","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. Proc. ACM Program. Lang. 4(POPL), 37:1\u201337:28 (2020). https:\/\/doi.org\/10.1145\/3371105","DOI":"10.1145\/3371105"},{"key":"33_CR48","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-030-02768-1_11","volume-title":"Programming Languages and Systems","author":"M Huang","year":"2018","unstructured":"Huang, M., Fu, H., Chatterjee, K.: New approaches for almost-sure termination of probabilistic programs. In: Ryu, S. (ed.) Programming Languages and Systems, pp. 181\u2013201. Springer, Cham (2018)"},{"key":"33_CR49","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. 3(OOPSLA), 129:1\u2013129:29 (2019). https:\/\/doi.org\/10.1145\/3360555","DOI":"10.1145\/3360555"},{"key":"33_CR50","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1613\/jair.301","volume":"4","author":"LP Kaelbling","year":"1996","unstructured":"Kaelbling, L.P., Littman, M.L., Moore, A.W.: Reinforcement learning: a survey. JAIR 4, 237\u2013285 (1996)","journal-title":"JAIR"},{"key":"33_CR51","doi-asserted-by":"crossref","unstructured":"Kaminski, B.L., Katoen, J.P., Matheja, C.: On the hardness of analyzing probabilistic programs. Acta Informatica 56(3), 1\u201331 (2018)","DOI":"10.1007\/s00236-018-0321-1"},{"key":"33_CR52","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 65(5), 30:1\u201330:68 (2018). https:\/\/doi.org\/10.1145\/3208102","DOI":"10.1145\/3208102"},{"key":"33_CR53","unstructured":"Kobayashi, N., Lago, U.D., Grellois, C.: On the termination problem for probabilistic higher-order recursive programs. Log. Methods Comput. Sci. 16(4), 2:1\u20132:57 (2020). https:\/\/lmcs.episciences.org\/6817"},{"issue":"3","key":"33_CR54","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). https:\/\/doi.org\/10.1016\/0022-0000(81)90036-2","journal-title":"J. Comput. Syst. Sci."},{"key":"33_CR55","doi-asserted-by":"publisher","unstructured":"Kozen, D.: A probabilistic PDL. In: Proceedings of the Fifteenth Annual ACM Symposium on Theory of Computing, pp. 291\u2013297, STOC 1983. ACM, New York, NY, USA (1983). https:\/\/doi.org\/10.1145\/800061.808758","DOI":"10.1145\/800061.808758"},{"key":"33_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"33_CR57","doi-asserted-by":"publisher","unstructured":"Lago, U.D., Grellois, C.: Probabilistic termination by monadic affine sized typing. ACM Trans. Program. Lang. Syst. 41(2), 10:1\u201310:65 (2019). https:\/\/doi.org\/10.1145\/3293605","DOI":"10.1145\/3293605"},{"key":"33_CR58","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C.: Developing and reasoning about probabilistic programs in pGCL. In: PSSE, pp. 123\u2013155 (2004)","DOI":"10.1007\/11889229_4"},{"key":"33_CR59","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, New York (2005). https:\/\/doi.org\/10.1007\/b138392","DOI":"10.1007\/b138392"},{"key":"33_CR60","unstructured":"McIver, A., Morgan, C.: A new rule for almost-certain termination of probabilistic and demonic programs. CoRR abs\/1612.01091 (2016). http:\/\/arxiv.org\/abs\/1612.01091"},{"key":"33_CR61","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.: A new proof rule for almost-sure termination. PACMPL 2(POPL), 33:1\u201333:28 (2018). https:\/\/doi.org\/10.1145\/3158121","DOI":"10.1145\/3158121"},{"key":"33_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/3-540-47764-0_7","volume-title":"Static Analysis","author":"D Monniaux","year":"2001","unstructured":"Monniaux, D.: An abstract analysis of the probabilistic termination of programs. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 111\u2013126. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-47764-0_7"},{"key":"33_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-030-72019-3_18","volume-title":"Programming Languages and Systems","author":"M Moosbrugger","year":"2021","unstructured":"Moosbrugger, M., Bartocci, E., Katoen, J.-P., Kov\u00e1cs, L.: Automated termination analysis of polynomial probabilistic programs. In: ESOP 2021. LNCS, vol. 12648, pp. 491\u2013518. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72019-3_18"},{"key":"33_CR64","unstructured":"Morgan, C., McIver, A.: pGCL: formal reasoning for random algorithms (1999)"},{"issue":"3","key":"33_CR65","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1145\/229542.229547","volume":"18","author":"C Morgan","year":"1996","unstructured":"Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Trans. Program. Lang. Syst. (TOPLAS) 18(3), 325\u2013353 (1996)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"33_CR66","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511814075","volume-title":"Randomized Algorithms","author":"R Motwani","year":"1995","unstructured":"Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press, New York (1995)"},{"key":"33_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-540-74407-8_28","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"MR Neuh\u00e4u\u00dfer","year":"2007","unstructured":"Neuh\u00e4u\u00dfer, M.R., Katoen, J.-P.: Bisimulation and logical preservation for continuous-time Markov decision processes. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 412\u2013427. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74407-8_28"},{"key":"33_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-642-00596-1_26","volume-title":"Foundations of Software Science and Computational Structures","author":"MR Neuh\u00e4u\u00dfer","year":"2009","unstructured":"Neuh\u00e4u\u00dfer, M.R., Stoelinga, M., Katoen, J.-P.: Delayed nondeterminism in continuous-time Markov Decision Processes. In: de Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 364\u2013379. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00596-1_26"},{"key":"33_CR69","doi-asserted-by":"crossref","unstructured":"Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: resource analysis for probabilistic programs. In: PLDI 2018, pp. 496\u2013512 (2018)","DOI":"10.1145\/3296979.3192394"},{"key":"33_CR70","doi-asserted-by":"publisher","unstructured":"Olmedo, F., Kaminski, B.L., Katoen, J.P., Matheja, C.: Reasoning about recursive probabilistic programs. In: Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 672\u2013681, LICS 2016. ACM, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2933575.2935317","DOI":"10.1145\/2933575.2935317"},{"key":"33_CR71","doi-asserted-by":"publisher","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: 5th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2004, Venice, January 11\u201313, 2004, Proceedings, pp. 239\u2013251 (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_20","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"33_CR72","doi-asserted-by":"publisher","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, pp. 32\u201341, LICS 2004. IEEE Computer Society, Washington, DC, USA (2004). https:\/\/doi.org\/10.1109\/LICS.2004.50","DOI":"10.1109\/LICS.2004.50"},{"key":"33_CR73","unstructured":"Roy, D., Mansinghka, V., Goodman, N., Tenenbaum, J.: A stochastic programming perspective on nonparametric Bayes. In: Nonparametric Bayesian Workshop, International Conference on Machine Learning, vol. 22, p. 26 (2008)"},{"issue":"12","key":"33_CR74","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1145\/2887747.2804317","volume":"50","author":"A \u015acibior","year":"2015","unstructured":"\u015acibior, A., Ghahramani, Z., Gordon, A.D.: Practical probabilistic programming with monads. ACM SIGPLAN Not. 50(12), 165\u2013176 (2015)","journal-title":"ACM SIGPLAN Not."},{"key":"33_CR75","doi-asserted-by":"crossref","unstructured":"Smolka, S., Kumar, P., Foster, N., Kozen, D., Silva, A.: Cantor meets Scott: semantic foundations for probabilistic networks. In: POPL 2017, pp. 557\u2013571 (2017)","DOI":"10.1145\/3093333.3009843"},{"key":"33_CR76","doi-asserted-by":"publisher","unstructured":"Sohn, K., Gelder, A.V.: Termination detection in logic programs using argument sizes. In: Proceedings of the Tenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, May 29\u201331, 1991, Denver, Colorado, USA, pp. 216\u2013226 (1991). https:\/\/doi.org\/10.1145\/113413.113433","DOI":"10.1145\/113413.113433"},{"issue":"3","key":"33_CR77","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1145\/504729.504754","volume":"45","author":"S Thrun","year":"2002","unstructured":"Thrun, S.: Probabilistic robotics. Commun. ACM 45(3), 52\u201357 (2002)","journal-title":"Commun. ACM"},{"key":"33_CR78","doi-asserted-by":"crossref","unstructured":"Wang, D., Hoffmann, J., Reps, T.W.: PMAF: an algebraic framework for static analysis of probabilistic programs. In: PLDI 2018, pp. 513\u2013528 (2018)","DOI":"10.1145\/3296979.3192408"},{"key":"33_CR79","doi-asserted-by":"crossref","unstructured":"Wang, P., Fu, H., Goharshady, A.K., Chatterjee, K., Qin, X., Shi, W.: Cost analysis of nondeterministic probabilistic programs. In: PLDI 2019, pp. 204\u2013220 (2019)","DOI":"10.1145\/3314221.3314581"},{"key":"33_CR80","series-title":"Cambridge Mathematical Textbooks","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511813658","volume-title":"Probability with Martingales","author":"D Williams","year":"1991","unstructured":"Williams, D.: Probability with Martingales. Cambridge Mathematical Textbooks, Cambridge University Press, Cambridge (1991)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-90870-6_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,10]],"date-time":"2021-11-10T00:12:12Z","timestamp":1636503132000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-90870-6_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030908690","9783030908706"],"references-count":80,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-90870-6_33","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":"10 November 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 November 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 November 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/formalmethods2021.csp.escience.cn\/dct\/page\/1","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":"131","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":"40","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":"2","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":"31% - 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","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":"9","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":"Additionally, this includes 4 invited full papers.","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)"}}]}}