{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:01:49Z","timestamp":1779087709244,"version":"3.51.4"},"publisher-location":"Cham","reference-count":64,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031377082","type":"print"},{"value":"9783031377099","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T00:00:00Z","timestamp":1689552000000},"content-version":"vor","delay-in-days":197,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Markov decision processes can be viewed as transformers of probability distributions. While this view is useful from a practical standpoint to reason about trajectories of distributions, basic reachability and safety problems are known to be computationally intractable (i.e., Skolem-hard) to solve in such models. Further, we show that even for simple examples of MDPs, strategies for safety objectives over distributions can require infinite memory and randomization.<\/jats:p><jats:p>In light of this, we present a novel overapproximation approach to synthesize strategies in an MDP, such that a safety objective over the distributions is met. More precisely, we develop a new framework for template-based synthesis of certificates as affine distributional and inductive invariants for safety objectives in MDPs. We provide two algorithms within this framework. One can only synthesize memoryless strategies, but has relative completeness guarantees, while the other can synthesize general strategies. The runtime complexity of both algorithms is in PSPACE. We implement these algorithms and show that they can solve several non-trivial examples.\n<\/jats:p>","DOI":"10.1007\/978-3-031-37709-9_5","type":"book-chapter","created":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:21Z","timestamp":1689501681000},"page":"86-112","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["MDPs as\u00a0Distribution Transformers: Affine Invariant Synthesis for\u00a0Safety Objectives"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2471-5997","authenticated-orcid":false,"given":"S.","family":"Akshay","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4561-241X","authenticated-orcid":false,"given":"Krishnendu","family":"Chatterjee","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1712-2165","authenticated-orcid":false,"given":"Tobias","family":"Meggendorfer","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4681-1699","authenticated-orcid":false,"given":"\u0110or\u0111e","family":"\u017dikeli\u0107","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,7,17]]},"reference":[{"issue":"1","key":"5_CR1","doi-asserted-by":"publisher","first-page":"2:1","DOI":"10.1145\/2629417","volume":"62","author":"M Agrawal","year":"2015","unstructured":"Agrawal, M., Akshay, S., Genest, B., Thiagarajan, P.S.: Approximate verification of the symbolic dynamics of Markov chains. J. ACM 62(1), 2:1-2:34 (2015). https:\/\/doi.org\/10.1145\/2629417","journal-title":"J. ACM"},{"key":"5_CR2","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/3158122","DOI":"10.1145\/3158122"},{"issue":"2","key":"5_CR3","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/j.ipl.2014.08.013","volume":"115","author":"S Akshay","year":"2015","unstructured":"Akshay, S., Antonopoulos, T., Ouaknine, J., Worrell, J.: Reachability problems for Markov chains. Inf. Process. Lett. 115(2), 155\u2013158 (2015). https:\/\/doi.org\/10.1016\/j.ipl.2014.08.013","journal-title":"Inf. Process. Lett."},{"key":"5_CR4","unstructured":"Akshay, S., Chatterjee, K., Meggendorfer, T., \u0110or\u0111e \u017dikeli\u0107: MDPs as distribution transformers: affine invariant synthesis for safety objectives (2023). https:\/\/arxiv.org\/abs\/2305.16796"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Akshay, S., Genest, B., Vyas, N.: Distribution-based objectives for markov decision processes. In: Dawar, A., Gr\u00e4del, E. (eds.) Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09\u201312, 2018, pp. 36\u201345. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209185","DOI":"10.1145\/3209108.3209185"},{"key":"5_CR6","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":"5_CR7","doi-asserted-by":"publisher","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: Irlbeck, M., Peled, D.A., Pretschner, A. (eds.) Dependable Software Systems Engineering, NATO Science for Peace and Security Series, D: Information and Communication Security, vol. 40, pp. 1\u201325. IOS Press (2015). https:\/\/doi.org\/10.3233\/978-1-61499-495-4-1","DOI":"10.3233\/978-1-61499-495-4-1"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Asadi, A., Chatterjee, K., Fu, H., Goharshady, A.K., Mahdavi, M.: Polynomial reachability witnesses via stellens\u00e4tze. In: Freund, S.N., Yahav, E. (eds.) PLDI 2021: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20\u201325, 2021, pp. 772\u2013787. ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454076","DOI":"10.1145\/3453483.3454076"},{"key":"5_CR9","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Batz, K., Chen, M., Junges, S., Kaminski, B.L., Katoen, J., Matheja, C.: Probabilistic program verification via inductive synthesis of inductive invariants. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023, Part II. LNCS, vol. 13994, pp. 410\u2013429. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_25","DOI":"10.1007\/978-3-031-30820-8_25"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1007\/978-3-030-81688-9_25","volume-title":"Computer Aided Verification","author":"K Batz","year":"2021","unstructured":"Batz, K., Chen, M., Kaminski, B.L., Katoen, J.-P., Matheja, C., Schr\u00f6er, P.: Latticed k-induction with an application to probabilistic programs. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 524\u2013549. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_25"},{"issue":"4","key":"5_CR12","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1093\/logcom\/exl004","volume":"16","author":"D Beauquier","year":"2006","unstructured":"Beauquier, D., Rabinovich, A.M., Slissenko, A.: A logic of probability with decidable model checking. J. Log. Comput. 16(4), 461\u2013487 (2006). https:\/\/doi.org\/10.1093\/logcom\/exl004","journal-title":"J. Log. Comput."},{"key":"5_CR13","volume-title":"Probability and Measure","author":"P Billingsley","year":"2008","unstructured":"Billingsley, P.: Probability and Measure. Wiley, New York (2008)"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/11513988_48","volume-title":"Computer Aided Verification","author":"AR Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 491\u2013504. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_48"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Canny, J.F.: Some algebraic and geometric computations in PSPACE. In: Simon, J. (ed.) Proceedings of the 20th Annual ACM Symposium on Theory of Computing, May 2\u20134, 1988, Chicago, Illinois, USA, pp. 460\u2013467. ACM (1988). https:\/\/doi.org\/10.1145\/62212.62257","DOI":"10.1145\/62212.62257"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: Grove, D., Blackburn, S.M. (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15\u201317, 2015, pp. 467\u2013478. ACM (2015). https:\/\/doi.org\/10.1145\/2737924.2737955","DOI":"10.1145\/2737924.2737955"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Chadha, R., Korthikanti, V.A., Viswanathan, M., Agha, G., Kwon, Y.: Model checking MDPs with a unique compact invariant set of distributions. In: Eighth International Conference on Quantitative Evaluation of Systems, QEST 2011, Aachen, Germany, 5\u20138 September, 2011, pp. 121\u2013130. IEEE Computer Society (2011). https:\/\/doi.org\/10.1109\/QEST.2011.22","DOI":"10.1109\/QEST.2011.22"},{"key":"5_CR18","doi-asserted-by":"publisher","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 (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"5_CR19","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":"5_CR20","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K., Goharshady, E.K.: Polynomial invariant generation for non-deterministic recursive programs. In: Donaldson, A.F., Torlak, E. (eds.) Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15\u201320, 2020, pp. 672\u2013687. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3385969","DOI":"10.1145\/3385412.3385969"},{"key":"5_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. TOPLAS 40(2), 7:1\u20137:45 (2018). https:\/\/doi.org\/10.1145\/3174800","DOI":"10.1145\/3174800"},{"key":"5_CR22","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: Shoham, S., Vizel, Y. (eds.) CAV 2022, Part I. LNCS, vol. 13371, pp. 55\u201378. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_4","DOI":"10.1007\/978-3-031-13185-1_4"},{"key":"5_CR23","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Goharshady, E.K., Novotn\u00fd, P., \u017dikeli\u0107, \u0110.: Proving non-termination by program reversal. In: Freund, S.N., Yahav, E. (eds.) PLDI 2021: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20\u201325, 20211, pp. 1033\u20131048. ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454093","DOI":"10.1145\/3453483.3454093"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1007\/978-3-030-90870-6_33","volume-title":"Formal Methods","author":"K Chatterjee","year":"2021","unstructured":"Chatterjee, K., Goharshady, E.K., Novotn\u00fd, P., Z\u00e1rev\u00facky, J., \u017dikeli\u0107, \u0110: On lexicographic proof rules for probabilistic termination. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 619\u2013639. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_33"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Novotn\u00fd, P., \u017dikeli\u0107, \u0110.: Stochastic invariants for probabilistic termination. In: POPL, pp. 145\u2013160 (2017). https:\/\/doi.org\/10.1145\/3009837.3009873","DOI":"10.1145\/3009837.3009873"},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"key":"5_CR27","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"},{"key":"5_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-45319-9_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"MA Col\u00f3on","year":"2001","unstructured":"Col\u00f3on, M.A., Sipma, H.B.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 67\u201381. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45319-9_6"},{"key":"5_CR29","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: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pp. 238\u2013252. ACM (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"5_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P Cousot","year":"2005","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The ASTRE\u00c9 analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21\u201330. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31987-0_3"},{"issue":"124","key":"5_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1515\/crll.1902.124.1","volume":"1902","author":"J Farkas","year":"1902","unstructured":"Farkas, J.: Theorie der einfachen ungleichungen. Journal f\u00fcr die reine und angewandte Mathematik (Crelles Journal) 1902(124), 1\u201327 (1902)","journal-title":"Journal f\u00fcr die reine und angewandte Mathematik (Crelles Journal)"},{"key":"5_CR32","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z.: Compositional recurrence analysis. In: Kaivola, R., Wahl, T. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, September 27\u201330, 2015, pp. 57\u201364. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"5_CR33","doi-asserted-by":"publisher","unstructured":"Feautrier, P., Gonnord, L.: Accelerated invariant generation for C programs with aspic and c2fsm. In: Delmas, D., Rival, X. (eds.) Proceedings of the Tools for Automatic Program AnalysiS, TAPAS@SAS 2010, Perpignan, France, September 17, 2010. Electronic Notes in Theoretical Computer Science, vol. 267, pp. 3\u201313. Elsevier (2010). https:\/\/doi.org\/10.1016\/j.entcs.2010.09.014","DOI":"10.1016\/j.entcs.2010.09.014"},{"key":"5_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-319-08867-9_5","volume-title":"Computer Aided Verification","author":"P Garg","year":"2014","unstructured":"Garg, P., L\u00f6ding, C., Madhusudan, P., Neider, D.: ICE:\u00a0a\u00a0robust\u00a0framework\u00a0for\u00a0learning\u00a0invariants. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 69\u201387. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_5"},{"key":"5_CR35","doi-asserted-by":"publisher","unstructured":"Garg, P., Neider, D., Madhusudan, P., Roth, D.: Learning invariants using decision trees and implication counterexamples. In: Bod\u00edk, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20\u201322, 2016, pp. 499\u2013512. ACM (2016). https:\/\/doi.org\/10.1145\/2837614.2837664","DOI":"10.1145\/2837614.2837664"},{"key":"5_CR36","unstructured":"Gario, M., Micheli, A.: Pysmt: a solver-agnostic library for fast prototyping of SMT-based algorithms. In: SMT Workshop, vol. 2015 (2015)"},{"key":"5_CR37","series-title":"Universitext","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30717-4","volume-title":"Understanding and using linear programming","author":"B G\u00e4rtner","year":"2007","unstructured":"G\u00e4rtner, B., Matousek, J.: Understanding and using linear programming. Universitext, Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-30717-4"},{"issue":"1","key":"5_CR38","doi-asserted-by":"publisher","first-page":"35","DOI":"10.2140\/pjm.1988.132.35","volume":"132","author":"D Handelman","year":"1988","unstructured":"Handelman, D.: Representing polynomials by positive linear functions on compact convex Polyhedra. Pacific J. Math. 132(1), 35\u201362 (1988)","journal-title":"Pacific J. Math."},{"key":"5_CR39","doi-asserted-by":"publisher","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst. 34(3), 14:1\u201314:62 (2012). https:\/\/doi.org\/10.1145\/2362389.2362393","DOI":"10.1145\/2362389.2362393"},{"key":"5_CR40","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":"5_CR41","doi-asserted-by":"publisher","unstructured":"Karimov, T., Kelmendi, E., Ouaknine, J., Worrell, J.: What\u2019s decidable about discrete linear dynamical systems? In: Raskin, J., Chatterjee, K., Doyen, L., Majumdar, R. (eds.) Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 13660, pp. 21\u201338. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-22337-2_2","DOI":"10.1007\/978-3-031-22337-2_2"},{"key":"5_CR42","doi-asserted-by":"publisher","unstructured":"Kincaid, Z., Breck, J., Boroujeni, A.F., Reps, T.W.: Compositional recurrence analysis revisited. In: Cohen, A., Vechev, M.T. (eds.) Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18\u201323, 2017, pp. 248\u2013262. ACM (2017). https:\/\/doi.org\/10.1145\/3062341.3062373","DOI":"10.1145\/3062341.3062373"},{"key":"5_CR43","doi-asserted-by":"publisher","unstructured":"Kincaid, Z., Cyphert, J., Breck, J., Reps, T.W.: Non-linear reasoning for invariant synthesis. Proc. ACM Program. Lang. 2(POPL), 54:1\u201354:33 (2018). https:\/\/doi.org\/10.1145\/3158142","DOI":"10.1145\/3158142"},{"key":"5_CR44","doi-asserted-by":"publisher","unstructured":"Korthikanti, V.A., Viswanathan, M., Agha, G., Kwon, Y.: Reasoning about MDPs as transformers of probability distributions. In: QEST 2010, Seventh International Conference on the Quantitative Evaluation of Systems, Williamsburg, Virginia, USA, 15\u201318 September 2010, pp. 199\u2013208. IEEE Computer Society (2010). https:\/\/doi.org\/10.1109\/QEST.2010.35","DOI":"10.1109\/QEST.2010.35"},{"key":"5_CR45","doi-asserted-by":"publisher","unstructured":"Kozen, D.: A probabilistic PDL. In: Johnson, D.S., et al. (eds.) Proceedings of the 15th Annual ACM Symposium on Theory of Computing, 25\u201327 April, 1983, Boston, Massachusetts, USA, pp. 291\u2013297. ACM (1983). https:\/\/doi.org\/10.1145\/800061.808758","DOI":"10.1145\/800061.808758"},{"key":"5_CR46","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T.: Conditional value-at-risk for reachability and mean payoff in Markov decision processes. In: Dawar, A., Gr\u00e4del, E. (eds.) Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09\u201312, 2018, pp. 609\u2013618. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209176","DOI":"10.1145\/3209108.3209176"},{"issue":"1","key":"5_CR47","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1109\/TSE.2010.80","volume":"37","author":"Y Kwon","year":"2011","unstructured":"Kwon, Y., Agha, G.A.: Verifying the evolution of probability distributions governed by a DTMC. IEEE Trans. Software Eng. 37(1), 126\u2013141 (2011). https:\/\/doi.org\/10.1109\/TSE.2010.80","journal-title":"IEEE Trans. Software Eng."},{"key":"5_CR48","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science, Springer, Cham (2005). https:\/\/doi.org\/10.1007\/b138392","DOI":"10.1007\/b138392"},{"key":"5_CR49","doi-asserted-by":"crossref","unstructured":"Meggendorfer, T.: Risk-aware stochastic shortest path. In: Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty-Fourth Conference on Innovative Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educational Advances in Artificial Intelligence, EAAI 2022 Virtual Event, February 22 - March 1, 2022, pp. 9858\u20139867. AAAI Press (2022). https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/view\/21222","DOI":"10.1609\/aaai.v36i9.21222"},{"key":"5_CR50","doi-asserted-by":"publisher","DOI":"10.7717\/peerj-cs.103","volume":"3","author":"A Meurer","year":"2017","unstructured":"Meurer, A., et al.: Sympy: symbolic computing in python. PeerJ Comput. Sci. 3, e103 (2017). https:\/\/doi.org\/10.7717\/peerj-cs.103","journal-title":"PeerJ Comput. Sci."},{"key":"5_CR51","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511616488","volume-title":"Performance Analysis of Communications Networks and Systems","author":"PV Mieghem","year":"2006","unstructured":"Mieghem, P.V.: Performance Analysis of Communications Networks and Systems. Cambridge University Press, Cambridge (2006)"},{"issue":"3","key":"5_CR52","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. 18(3), 325\u2013353 (1996). https:\/\/doi.org\/10.1145\/229542.229547","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"5_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"5_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-33512-9_3","volume-title":"Reachability Problems","author":"J Ouaknine","year":"2012","unstructured":"Ouaknine, J., Worrell, J.: Decision problems for linear recurrence sequences. In: Finkel, A., Leroux, J., Potapov, I. (eds.) RP 2012. LNCS, vol. 7550, pp. 21\u201328. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33512-9_3"},{"key":"5_CR55","doi-asserted-by":"publisher","unstructured":"Ouaknine, J., Worrell, J.: Positivity problems for low-order linear recurrence sequences. In: Chekuri, C. (ed.) Proceedings of the Twenty-Fifth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2014, Portland, Oregon, USA, January 5\u20137, 2014, pp. 366\u2013379. SIAM (2014). https:\/\/doi.org\/10.1137\/1.9781611973402.27","DOI":"10.1137\/1.9781611973402.27"},{"issue":"2","key":"5_CR56","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). https:\/\/doi.org\/10.1145\/2766189.2766191","journal-title":"ACM SIGLOG News"},{"key":"5_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239\u2013251. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_20"},{"key":"5_CR58","doi-asserted-by":"publisher","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics, Wiley (1994). https:\/\/doi.org\/10.1002\/9780470316887","DOI":"10.1002\/9780470316887"},{"issue":"3","key":"5_CR59","doi-asserted-by":"publisher","first-page":"969","DOI":"10.1512\/iumj.1993.42.42045","volume":"42","author":"M Putinar","year":"1993","unstructured":"Putinar, M.: Positive polynomials on compact semi-algebraic sets. Indiana University Math. J. 42(3), 969\u2013984 (1993)","journal-title":"Indiana University Math. J."},{"key":"5_CR60","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Sci. Comput. Program. 64(1), 54\u201375 (2007). https:\/\/doi.org\/10.1016\/j.scico.2006.03.003","DOI":"10.1016\/j.scico.2006.03.003"},{"key":"5_CR61","unstructured":"Si, X., Dai, H., Raghothaman, M., Naik, M., Song, L.: Learning loop invariants for program verification. In: Bengio, S., Wallach, H.M., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018(December), pp. 3\u20138, 2018. Montr\u00e9al, Canada, pp. 7762\u20137773 (2018). https:\/\/proceedings.neurips.cc\/paper\/2018\/hash\/65b1e92c585fd4c2159d5f33b5030ff2-Abstract.html"},{"issue":"2","key":"5_CR62","doi-asserted-by":"publisher","first-page":"5:1","DOI":"10.1145\/3450967","volume":"43","author":"T Takisaka","year":"2021","unstructured":"Takisaka, T., Oyabu, Y., Urabe, N., Hasuo, I.: Ranking and repulsing supermartingales for reachability in randomized programs. ACM Trans. Program. Lang. Syst. 43(2), 5:1-5:46 (2021). https:\/\/doi.org\/10.1145\/3450967","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"5_CR63","doi-asserted-by":"publisher","unstructured":"Wang, P., Fu, H., Goharshady, A.K., Chatterjee, K., Qin, X., Shi, W.: Cost analysis of nondeterministic probabilistic programs. In: McKinley, K.S., Fisher, K. (eds.) Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22\u201326, 2019, pp. 204\u2013220. ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314581","DOI":"10.1145\/3314221.3314581"},{"key":"5_CR64","doi-asserted-by":"publisher","unstructured":"Zikelic, D., Chang, B.E., Bolignano, P., Raimondi, F.: Differential cost analysis with simultaneous potentials and anti-potentials. In: Jhala, R., Dillig, I. (eds.) 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2022, San Diego, CA, USA, 13\u201317 June 2022, pp. 442\u2013457. ACM (2022). https:\/\/doi.org\/10.1145\/3519939.3523435","DOI":"10.1145\/3519939.3523435"}],"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-37709-9_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:02:01Z","timestamp":1689501721000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37709-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377082","9783031377099"],"references-count":64,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37709-9_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","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":"67","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":"26% - 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":"11","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)"}}]}}