{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,4]],"date-time":"2025-12-04T10:08:26Z","timestamp":1764842906574,"version":"3.40.3"},"publisher-location":"Cham","reference-count":69,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031656323"},{"type":"electronic","value":"9783031656330"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present for the first time a supermartingale certificate for <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\omega $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c9<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-regular specifications. We leverage the Robbins &amp; Siegmund convergence theorem to characterize supermartingale certificates for the almost-sure acceptance of Streett conditions on general stochastic processes, which we call Streett supermartingales. This enables effective verification and control of discrete-time stochastic dynamical models with infinite state space under <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\omega $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c9<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-regular and linear temporal logic specifications. Our result generalises reachability, safety, reach-avoid, persistence and recurrence specifications; our contribution applies to discrete-time stochastic dynamical models and probabilistic programs with discrete and continuous state spaces and distributions, and carries over to deterministic models and programs. We provide a synthesis algorithm for control policies and Streett supermartingales as proof certificates for <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\omega $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c9<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-regular objectives, which is sound and complete for supermartingales and control policies with polynomial templates and any stochastic dynamical model whose post-expectation is expressible as a polynomial. We additionally provide an optimisation of our algorithm that reduces the problem to satisfiability modulo theories, under the assumption that templates and post-expectation are in piecewise linear form. We have built a prototype and have demonstrated the efficacy of our approach on several exemplar <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\omega $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c9<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-regular verification and control synthesis problems.\n\n<\/jats:p>","DOI":"10.1007\/978-3-031-65633-0_18","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:08Z","timestamp":1721890988000},"page":"395-419","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Stochastic Omega-Regular Verification and\u00a0Control with\u00a0Supermartingales"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5627-9093","authenticated-orcid":false,"given":"Alessandro","family":"Abate","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8180-0904","authenticated-orcid":false,"given":"Mirco","family":"Giacobbe","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0003-4306-2076","authenticated-orcid":false,"given":"Diptarko","family":"Roy","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"issue":"3","key":"18_CR1","doi-asserted-by":"publisher","first-page":"773","DOI":"10.1109\/LCSYS.2020.3005328","volume":"5","author":"A Abate","year":"2021","unstructured":"Abate, A., Ahmed, D., Giacobbe, M., Peruffo, A.: Formal synthesis of Lyapunov Neural Networks. IEEE Control. Syst. Lett. 5(3), 773\u2013778 (2021)","journal-title":"IEEE Control. Syst. Lett."},{"key":"18_CR2","unstructured":"Abate, A., Edwards, A., Giacobbe, M., Punchihewa, H., Roy, D.: Quantitative verification with neural networks. In: CONCUR. LIPIcs, vol.\u00a0279, pp. 22:1\u201322:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023)"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-81688-9_1","volume-title":"Computer Aided Verification","author":"A Abate","year":"2021","unstructured":"Abate, A., Giacobbe, M., Roy, D.: Learning probabilistic termination proofs. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 3\u201326. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_1"},{"key":"18_CR4","doi-asserted-by":"publisher","unstructured":"Abate, A., Giacobbe, M., Schnitzer, Y.: Bisimulation learning. In: Ganesh, V., Gurfinkel, A. (eds.) CAV 2024. LNCS, vol. 14683, pp. 161\u2013183. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65633-0_8","DOI":"10.1007\/978-3-031-65633-0_8"},{"issue":"6","key":"18_CR5","doi-asserted-by":"publisher","first-page":"624","DOI":"10.3166\/ejc.16.624-641","volume":"16","author":"A Abate","year":"2010","unstructured":"Abate, A., Katoen, J., Lygeros, J., Prandini, M.: Approximate model checking of stochastic hybrid systems. Eur. J. Control. 16(6), 624\u2013641 (2010)","journal-title":"Eur. J. Control."},{"key":"18_CR6","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":"18_CR7","doi-asserted-by":"crossref","unstructured":"Alshiekh, M., Bloem, R., Ehlers, R., K\u00f6nighofer, B., Niekum, S., Topcu, U.: Safe reinforcement learning via shielding. In: AAAI, pp. 2669\u20132678. AAAI Press (2018)","DOI":"10.1609\/aaai.v32i1.11797"},{"key":"18_CR8","doi-asserted-by":"publisher","DOI":"10.1016\/j.nahs.2023.101427","volume":"51","author":"M Anand","year":"2024","unstructured":"Anand, M., Lavaei, A., Zamani, M.: Compositional synthesis of control barrier certificates for networks of stochastic systems against $$\\omega $$-regular specifications. Nonlinear Anal. Hybrid Syst 51, 101427 (2024)","journal-title":"Nonlinear Anal. Hybrid Syst"},{"issue":"5","key":"18_CR9","doi-asserted-by":"publisher","first-page":"1018","DOI":"10.1214\/aos\/1176343602","volume":"4","author":"D Anbar","year":"1976","unstructured":"Anbar, D.: An application of a theorem of Robbins and Siegmund. Ann. Stat. 4(5), 1018\u20131021 (1976)","journal-title":"Ann. Stat."},{"key":"18_CR10","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Batz, K., Biskup, T.J., Katoen, J., Winkler, T.: Programmatic strategy synthesis: resolving nondeterminism in probabilistic programs. Proc. ACM Program. Lang. 8(POPL), 2792\u20132820 (2024)","DOI":"10.1145\/3632935"},{"key":"18_CR12","unstructured":"Bertsekas, D.P., Tsitsiklis, J.N.: Neuro-Dynamic Programming. Optimization and Neural Computation Series, vol.\u00a03. Athena Scientific (1996)"},{"issue":"2","key":"18_CR13","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/s10703-012-0166-0","volume":"43","author":"T Br\u00e1zdil","year":"2013","unstructured":"Br\u00e1zdil, T., Esparza, J., Kiefer, S., Kucera, A.: Analyzing probabilistic pushdown automata. Formal Methods Syst. Des. 43(2), 124\u2013163 (2013)","journal-title":"Formal Methods Syst. Des."},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-540-31856-9_12","volume-title":"STACS 2005","author":"T Br\u00e1zdil","year":"2005","unstructured":"Br\u00e1zdil, T., Ku\u010dera, A., Stra\u017eovsk\u00fd, O.: On the decidability of temporal properties of probabilistic pushdown automata. In: Diekert, V., Durand, B. (eds.) STACS 2005. LNCS, vol. 3404, pp. 145\u2013157. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31856-9_12"},{"key":"18_CR15","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":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-319-10936-7_6","volume-title":"Static Analysis","author":"A Chakarov","year":"2014","unstructured":"Chakarov, A., Sankaranarayanan, S.: Expectation invariants for probabilistic program loops as fixed points. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 85\u2013100. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10936-7_6"},{"key":"18_CR17","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":"18_CR18","unstructured":"Chang, Y., Roohi, N., Gao, S.: Neural Lyapunov control. In: NeurIPS, pp. 3240\u20133249 (2019)"},{"key":"18_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":"18_CR20","doi-asserted-by":"crossref","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)","DOI":"10.1145\/3174800"},{"key":"18_CR21","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-031-13185-1_4","volume-title":"CAV (2022","author":"K Chatterjee","year":"2022","unstructured":"Chatterjee, K., Goharshady, A.K., Meggendorfer, T., \u017dikeli\u0107, D.: Sound and complete certificates for quantitative termination analysis of probabilistic programs. In: Shoham, S., Vizel, Y. (eds.) CAV (2022. LNCS, vol. 13371, pp. 55\u201378. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_4"},{"key":"18_CR22","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-031-30823-9_1","volume-title":"TACAS 2023","author":"K Chatterjee","year":"2023","unstructured":"Chatterjee, K., Henzinger, T.A., Lechner, M., \u017dikeli\u0107, D.: A learner-verifier framework for neural network controllers and certificates of stochastic systems. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13993, pp. 3\u201325. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_1"},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Novotn\u00fd, P., \u017dikeli\u0107, D.: Stochastic invariants for probabilistic termination. In: POPL, pp. 145\u2013160. ACM (2017)","DOI":"10.1145\/3093333.3009873"},{"issue":"3","key":"18_CR24","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1145\/1086837.1086852","volume":"8","author":"GE Collins","year":"1974","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition-preliminary report. SIGSAM Bull. 8(3), 80\u201390 (1974)","journal-title":"SIGSAM Bull."},{"key":"18_CR25","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":"18_CR26","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":"18_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/3-540-45657-0_36","volume-title":"Computer Aided Verification","author":"MA Col\u00f3n","year":"2002","unstructured":"Col\u00f3n, M.A., Sipma, H.B.: Practical methods for proving program termination. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 442\u2013454. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_36"},{"key":"18_CR28","doi-asserted-by":"crossref","unstructured":"Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.Y.: Proving that programs eventually do something good. In: POPL, pp. 265\u2013276. ACM (2007)","DOI":"10.1145\/1190215.1190257"},{"key":"18_CR29","doi-asserted-by":"crossref","unstructured":"Desharnais, J., Laviolette, F., Tracol, M.: Approximate analysis of probabilistic processes: logic, simulation and games. In: QEST, pp. 264\u2013273. IEEE Computer Society (2008)","DOI":"10.1109\/QEST.2008.42"},{"key":"18_CR30","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., et al.: From spot 2.0 to spot 2.10: what\u2019s new? In: Shoham, S., Vizel, Y. (eds.) CAV 2022. LNCS, vol. 13372, pp. 174\u2013187. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"18_CR31","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511779398","volume-title":"Probability: Theory and Examples","author":"R Durrett","year":"2010","unstructured":"Durrett, R.: Probability: Theory and Examples, 4th edn. Cambridge University Press, Cambridge (2010)","edition":"4"},{"issue":"1\u20133","key":"18_CR32","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst, M.D., et al.: The daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1\u20133), 35\u201345 (2007)","journal-title":"Sci. Comput. Program."},{"key":"18_CR33","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":"18_CR34","doi-asserted-by":"crossref","unstructured":"Fioriti, L.M.F., Hermanns, H.: Probabilistic termination: soundness, completeness, and compositionality. In: POPL, pp. 489\u2013501. ACM (2015)","DOI":"10.1145\/2775051.2677001"},{"key":"18_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-319-41528-4_4","volume-title":"Computer Aided Verification","author":"T Gehr","year":"2016","unstructured":"Gehr, T., Misailovic, S., Vechev, M.: PSI: exact symbolic inference for probabilistic programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 62\u201383. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_4"},{"key":"18_CR36","doi-asserted-by":"crossref","unstructured":"Giacobbe, M., Kroening, D., Parsert, J.: Neural termination analysis. In: ESEC\/SIGSOFT FSE, pp. 633\u2013645. ACM (2022)","DOI":"10.1145\/3554332"},{"issue":"4","key":"18_CR37","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/s10009-021-00633-z","volume":"24","author":"C Hensel","year":"2022","unstructured":"Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589\u2013610 (2022)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3\/4","key":"18_CR38","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1145\/2429135.2429155","volume":"46","author":"D Jovanovic","year":"2012","unstructured":"Jovanovic, D., de Moura, L.: Solving non-linear arithmetic. ACM Commun. Comput. Algebra 46(3\/4), 104\u2013105 (2012)","journal-title":"ACM Commun. Comput. Algebra"},{"key":"18_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1007\/978-3-319-96145-3_30","volume-title":"Computer Aided Verification","author":"J K\u0159et\u00ednsk\u00fd","year":"2018","unstructured":"K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S., Ziegler, C.: Rabinizer 4: from LTL to your favourite deterministic automaton. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 567\u2013577. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_30"},{"key":"18_CR40","doi-asserted-by":"crossref","unstructured":"Kucera, A., Esparza, J., Mayr, R.: Model checking probabilistic pushdown automata. Log. Methods Comput. Sci. 2(1) (2006)","DOI":"10.2168\/LMCS-2(1:2)2006"},{"key":"18_CR41","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":"18_CR42","doi-asserted-by":"crossref","unstructured":"Lavaei, A., Soudjani, S., Abate, A., Zamani, M.: Automated verification and synthesis of stochastic hybrid systems: a survey. Automatica 146(12) (2022)","DOI":"10.1016\/j.automatica.2022.110617"},{"key":"18_CR43","doi-asserted-by":"crossref","unstructured":"Lechner, M., \u017dikeli\u0107, D., Chatterjee, K., Henzinger, T.A.: Stability verification in stochastic control systems via neural network supermartingales. In: AAAI, pp. 7326\u20137336. AAAI Press (2022)","DOI":"10.1609\/aaai.v36i7.20695"},{"key":"18_CR44","doi-asserted-by":"crossref","unstructured":"Mangasarian, O.L.: Nonlinear Programming. Society for Industrial and Applied Mathematics (1994)","DOI":"10.1137\/1.9781611971255"},{"key":"18_CR45","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: PODC, pp. 377\u2013410. ACM (1990)","DOI":"10.1145\/93385.93442"},{"key":"18_CR46","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems - Safety","author":"Z Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems - Safety. Springer, New York (1995). https:\/\/doi.org\/10.1007\/978-1-4612-4222-2"},{"key":"18_CR47","volume":"4","author":"A Meurer","year":"2016","unstructured":"Meurer, A., et al.: SymPy: symbolic computing in Python. PeerJ Prepr. 4, e2083 (2016)","journal-title":"PeerJ Prepr."},{"key":"18_CR48","doi-asserted-by":"crossref","unstructured":"Meyn, S., Tweedie, R.L., Glynn, P.W.: Markov Chains and Stochastic Stability, 2nd edn. Cambridge Mathematical Library. Cambridge University Press, New York (2009)","DOI":"10.1017\/CBO9780511626630"},{"key":"18_CR49","volume-title":"Foundations of Machine Learning. Adaptive computation and Machine Learning","author":"M Mohri","year":"2012","unstructured":"Mohri, M., Rostamizadeh, A., Talwalkar, A.: Foundations of Machine Learning. Adaptive computation and Machine Learning. MIT Press, Cambridge (2012)"},{"key":"18_CR50","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":"18_CR51","doi-asserted-by":"crossref","unstructured":"Murali, V., Trivedi, A., Zamani, M.: Closure certificates. In: HSCC, pp. 10:1\u201310:11. ACM (2024)","DOI":"10.1145\/3641513.3650120"},{"key":"18_CR52","doi-asserted-by":"crossref","unstructured":"Nadali, A., Murali, V., Trivedi, A., Zamani, M.: Neural closure certificates. In: AAAI, pp. 21446\u201321453. AAAI Press (2024)","DOI":"10.1609\/aaai.v38i19.30141"},{"key":"18_CR53","doi-asserted-by":"crossref","unstructured":"Nguyen, T., Kapur, D., Weimer, W., Forrest, S.: DIG: a dynamic invariant generator for polynomial and array invariants. ACM Trans. Softw. Eng. Methodol. 23(4), 30:1\u201330:30 (2014)","DOI":"10.1145\/2556782"},{"key":"18_CR54","doi-asserted-by":"crossref","unstructured":"Pollard, D.: A User\u2019s Guide to Measure Theoretic Probability. Cambridge Series in Statistical and Probabilistic Mathematics. Cambridge University Press, New York (2001)","DOI":"10.1017\/CBO9780511811555"},{"key":"18_CR55","first-page":"233","volume":"1971","author":"H Robbins","year":"1971","unstructured":"Robbins, H., Siegmund, D.: A convergence theorem for non negative almost supermartingales and some applications. Optim. Methods Stat. 1971, 233\u2013257 (1971)","journal-title":"Optim. Methods Stat."},{"key":"18_CR56","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of omega-automata. In: FOCS, pp. 319\u2013327. IEEE Computer Society (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"18_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-540-27864-1_7","volume-title":"Static Analysis","author":"S Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constraint-based linear-relations analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 53\u201368. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27864-1_7"},{"issue":"2","key":"18_CR58","doi-asserted-by":"publisher","first-page":"921","DOI":"10.1137\/120871456","volume":"12","author":"SEZ Soudjani","year":"2012","unstructured":"Soudjani, S.E.Z., Abate, A.: Adaptive and sequential gridding for abstraction and verification of stochastic processes. SIAM J. Appl. Dyn. Syst. 12(2), 921\u2013956 (2012)","journal-title":"SIAM J. Appl. Dyn. Syst."},{"key":"18_CR59","doi-asserted-by":"crossref","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\u20135:46 (2021)","DOI":"10.1145\/3450967"},{"key":"18_CR60","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2013.09.032","volume":"515","author":"I Tkachev","year":"2014","unstructured":"Tkachev, I., Abate, A.: Characterization and computation of infinite horizon specifications over markov processes. Theoret. Comput. Sci. 515, 1\u201318 (2014)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"18_CR61","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ic.2016.11.006","volume":"253","author":"I Tkachev","year":"2017","unstructured":"Tkachev, I., Mereacre, A., Katoen, J.P., Abate, A.: Quantitative model checking of controlled discrete-time markov processes. Inf. Comput. 253(1), 1\u201335 (2017)","journal-title":"Inf. Comput."},{"key":"18_CR62","doi-asserted-by":"crossref","unstructured":"Tkachev, I., Abate, A.: Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems. In: HSCC, pp. 283\u2013292. ACM (2013)","DOI":"10.1145\/2461328.2461372"},{"issue":"1\u20132","key":"18_CR63","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0168-0072(91)90066-U","volume":"51","author":"MY Vardi","year":"1991","unstructured":"Vardi, M.Y.: Verification of concurrent programs: the automata-theoretic framework. Ann. Pure Appl. Log. 51(1\u20132), 79\u201398 (1991)","journal-title":"Ann. Pure Appl. Log."},{"key":"18_CR64","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-031-30820-8_16","volume-title":"TACAS 2023","author":"Y Wang","year":"2023","unstructured":"Wang, Y., Zhu, H.: Verification-guided programmatic controller synthesis. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13994, pp. 229\u2013250. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_16"},{"key":"18_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-030-99253-8_23","volume-title":"Foundations of Software Science and Computation Structures","author":"T Winkler","year":"2022","unstructured":"Winkler, T., Gehnen, C., Katoen, J.-P.: Model checking temporal properties of recursive probabilistic programs. In: FoSSaCS 2022. LNCS, vol. 13242, pp. 449\u2013469. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99253-8_23"},{"key":"18_CR66","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-031-37706-8_16","volume-title":"CAV 2023","author":"Z Yang","year":"2023","unstructured":"Yang, Z., Zhang, L., Zeng, X., Tang, X., Peng, C., Zeng, Z.: Hybrid controller synthesis for nonlinear systems subject to reach-avoid constraints. In: Enea, C., Lal, A. (eds.) CAV 2023. LNCS, vol. 13964, pp. 304\u2013325. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37706-8_16"},{"key":"18_CR67","doi-asserted-by":"crossref","unstructured":"Yannakakis, M., Etessami, K.: Checking LTL properties of recursive markov chains. In: QEST, pp. 155\u2013165. IEEE Computer Society (2005)","DOI":"10.1109\/QEST.2005.8"},{"issue":"12","key":"18_CR68","doi-asserted-by":"publisher","first-page":"3135","DOI":"10.1109\/TAC.2014.2351652","volume":"59","author":"M Zamani","year":"2014","unstructured":"Zamani, M., Esfahani, P.M., Majumdar, R., Abate, A., Lygeros, J.: Symbolic control of stochastic systems via approximately bisimilar finite abstractions. IEEE Trans. Autom. Control 59(12), 3135\u20133150 (2014)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"6","key":"18_CR69","doi-asserted-by":"publisher","first-page":"572","DOI":"10.3166\/EJC.18.572-587","volume":"18","author":"L Zhang","year":"2012","unstructured":"Zhang, L., She, Z., Ratschan, S., Hermanns, H., Hahn, E.M.: Safety verification for probabilistic hybrid systems. Eur. J. Control. 18(6), 572\u2013587 (2012)","journal-title":"Eur. J. Control."}],"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-65633-0_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:07:14Z","timestamp":1721891234000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65633-0_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656323","9783031656330"],"references-count":69,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65633-0_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","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":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}