{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T10:17:18Z","timestamp":1770977838166,"version":"3.50.1"},"publisher-location":"Cham","reference-count":67,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986789","type":"print"},{"value":"9783031986796","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T00:00:00Z","timestamp":1753142400000},"content-version":"vor","delay-in-days":202,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We present the first supermartingale certificate for quantitative <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\omega $$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c9<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>-regular properties of discrete-time infinite-state stochastic systems. Our certificate is defined on the product of the stochastic system and a limit-deterministic B\u00fcchi automaton that specifies the property of interest; hence we call it a limit-deterministic B\u00fcchi supermartingale (LDBSM). Previously known supermartingale certificates applied only to quantitative reachability, safety, or reach-avoid properties, and to qualitative (i.e., probability\u00a01) <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\omega $$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c9<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>-regular properties.We also present fully automated algorithms for the template-based synthesis of LDBSMs, for the case when the stochastic system dynamics and the controller can be represented in terms of polynomial inequalities. Our experiments demonstrate the ability of our method to solve verification and control tasks for stochastic systems that were beyond the reach of previous supermartingale-based approaches.<\/jats:p>","DOI":"10.1007\/978-3-031-98679-6_2","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T09:20:17Z","timestamp":1753089617000},"page":"29-55","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Supermartingale Certificates for\u00a0Quantitative Omega-Regular Verification and\u00a0Control"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2985-7724","authenticated-orcid":false,"given":"Thomas A.","family":"Henzinger","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9864-7475","authenticated-orcid":false,"given":"Kaushik","family":"Mallik","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0007-2417-8005","authenticated-orcid":false,"given":"Pouya","family":"Sadeghi","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":[[2025,7,22]]},"reference":[{"key":"2_CR1","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":"2_CR2","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. (eds.) CAV 2021. LNCS, vol. 12760, pp. 3\u201326. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_1"},{"key":"2_CR3","doi-asserted-by":"publisher","unstructured":"Abate, A., Giacobbe, M., Roy, D.: Stochastic omega-regular verification and control with supermartingales. In: International Conference on Computer Aided Verification, pp. 395\u2013419. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-65633-0_18","DOI":"10.1007\/978-3-031-65633-0_18"},{"key":"2_CR4","doi-asserted-by":"publisher","unstructured":"Ansaripour, M., Chatterjee, K., Henzinger, T.A., Lechner, M., \u017dikeli\u0107, \u0110.: Learning provably stabilizing neural controllers for discrete-time stochastic systems. In: International Symposium on Automated Technology for Verification and Analysis, pp. 357\u2013379. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-45329-8_17","DOI":"10.1007\/978-3-031-45329-8_17"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Asadi, A., Chatterjee, K., Fu, H., Goharshady, A.K., Mahdavi, M.: Polynomial reachability witnesses via stellens\u00e4tze. In: PLDI, pp. 772\u2013787. ACM (2021)","DOI":"10.1145\/3453483.3454076"},{"key":"2_CR6","unstructured":"\u00c5str\u00f6m, K.J.: Introduction to Stochastic Control Theory. Courier Corporation, Chelmsford (2012)"},{"key":"2_CR7","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT press, Cambridge (2008)"},{"key":"2_CR8","doi-asserted-by":"publisher","unstructured":"Barthe, G., Gaboardi, M., Gr\u00e9goire, B., Hsu, J., Strub, P.: Proving differential privacy via probabilistic couplings. In: Grohe, M., Koskinen, E., Shankar, N. (eds.) Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS \u201916, New York, NY, USA, 5\u20138 July 2016, pp. 749\u2013758. ACM (2016). https:\/\/doi.org\/10.1145\/2933575.2934554","DOI":"10.1145\/2933575.2934554"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Beutner, R., Ong, C.L., Zaiser, F.: Guaranteed bounds for posterior inference in universal probabilistic programming. In: PLDI, pp. 536\u2013551. ACM (2022)","DOI":"10.1145\/3519939.3523721"},{"key":"2_CR10","doi-asserted-by":"publisher","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R.: The mathsat 4 smt solver: Tool paper. In: Computer Aided Verification: 20th International Conference, CAV 2008 Princeton, NJ, USA, 7\u201314 July 2008 Proceedings 20, pp. 299\u2013303. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_28","DOI":"10.1007\/978-3-540-70545-1_28"},{"key":"2_CR11","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":"2_CR12","doi-asserted-by":"publisher","unstructured":"Chakarov, A., Sankaranarayanan, S.: Expectation Invariants for Probabilistic Program Loops as Fixed Points, pp. 85\u2013100. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-319-10936-7_6","DOI":"10.1007\/978-3-319-10936-7_6"},{"key":"2_CR13","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":"2_CR14","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":"2_CR15","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":"2_CR16","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Goharshady, A.K., Meggendorfer, T., \u017dikeli\u0107, \u0110.: Sound and complete certificates for quantitative termination analysis of probabilistic programs. In: International Conference on Computer Aided Verification, pp. 55\u201378. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_4","DOI":"10.1007\/978-3-031-13185-1_4"},{"issue":"OOPSLA1","key":"2_CR17","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1145\/3649824","volume":"8","author":"K Chatterjee","year":"2024","unstructured":"Chatterjee, K., Goharshady, A.K., Meggendorfer, T., \u017dikeli\u0107, \u0110: Quantitative bounds on resource usage of probabilistic programs. Proc. ACM Program. Lang. 8(OOPSLA1), 362\u2013391 (2024)","journal-title":"Proc. ACM Program. Lang."},{"key":"2_CR18","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Henzinger, T.A., Lechner, M., \u017dikeli\u0107, \u0110.: A learner-verifier framework for neural network controllers and certificates of stochastic systems. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 3\u201325. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_1","DOI":"10.1007\/978-3-031-30823-9_1"},{"key":"2_CR19","unstructured":"Chatterjee, K., et al.: Polyqent: a polynomial quantified entailment solver. arXiv e-prints pp. arXiv\u20132408 (2024)"},{"issue":"2","key":"2_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3585391","volume":"35","author":"K Chatterjee","year":"2023","unstructured":"Chatterjee, K., Kafshdar Goharshady, E., Novotn\u1ef3, P., Z\u00e1rev\u00facky, J., \u017dikeli\u0107, \u0110: On lexicographic proof rules for probabilistic termination. Formal Aspects Comput. 35(2), 1\u201325 (2023)","journal-title":"Formal Aspects Comput."},{"key":"2_CR21","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Novotn\u00fd, P., Zikelic, D.: Stochastic invariants for probabilistic termination. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 18\u201320 January 2017, pp. 145\u2013160. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009873","DOI":"10.1145\/3009837.3009873"},{"key":"2_CR22","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":"2_CR23","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":"2_CR24","doi-asserted-by":"crossref","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857\u2013907 (1995)","DOI":"10.1145\/210332.210339"},{"key":"2_CR25","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":"2_CR26","doi-asserted-by":"publisher","DOI":"10.1016\/j.nahs.2022.101204","volume":"45","author":"M Dutreix","year":"2022","unstructured":"Dutreix, M., Huh, J., Coogan, S.: Abstraction-based synthesis for stochastic systems with omega-regular objectives. Nonlinear Anal. Hybrid Syst 45, 101204 (2022)","journal-title":"Nonlinear Anal. Hybrid Syst"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Esmaeil Zadeh\u00a0Soudjani, S., Abate, A.: Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes. SIAM J. Appl. Dyn. Syst. 12(2), 921\u2013956 (2013)","DOI":"10.1137\/120871456"},{"issue":"124","key":"2_CR28","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 J.) 1902(124), 1\u201327 (1902)","journal-title":"Journal f\u00fcr die reine und angewandte Mathematik (Crelles J.)"},{"issue":"4","key":"2_CR29","doi-asserted-by":"publisher","first-page":"1151","DOI":"10.1137\/S0363012993252309","volume":"33","author":"P Florchinger","year":"1995","unstructured":"Florchinger, P.: Lyapunov-like techniques for stochastic stability. SIAM J. Control. Optim. 33(4), 1151\u20131169 (1995)","journal-title":"SIAM J. Control. Optim."},{"key":"2_CR30","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":"2_CR31","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"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"Gehr, T., Misailovic, S., Vechev, M.T.: PSI: exact symbolic inference for probabilistic programs. In: CAV (2016)","DOI":"10.1007\/978-3-319-41528-4_4"},{"issue":"7553","key":"2_CR33","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). https:\/\/doi.org\/10.1038\/nature14541","journal-title":"Nature"},{"key":"2_CR34","doi-asserted-by":"crossref","unstructured":"Kalman, R.E., Bertram, J.E.: Control system analysis and design via the \u201csecond method\u201d of lyapunov: I\u2014continuous-time systems (1960)","DOI":"10.1115\/1.3662604"},{"key":"2_CR35","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":"2_CR36","unstructured":"LaSalle, J., Lefschetz, S.: Stability by Lyapunov\u2019s Second Method with Applications. Academic Press, New York (1961)"},{"key":"2_CR37","doi-asserted-by":"crossref","unstructured":"Lechner, M., \u017dikeli\u0107, \u0110., Chatterjee, K., Henzinger, T.A.: Stability verification in stochastic control systems via neural network supermartingales. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a036, pp. 7326\u20137336 (2022)","DOI":"10.1609\/aaai.v36i7.20695"},{"key":"2_CR38","doi-asserted-by":"publisher","DOI":"10.1016\/j.nahs.2023.101430","volume":"51","author":"R Majumdar","year":"2024","unstructured":"Majumdar, R., Mallik, K., Schmuck, A.K., Soudjani, S.: Symbolic control for stochastic systems via finite parity games. Nonlinear Anal. Hybrid Syst 51, 101430 (2024)","journal-title":"Nonlinear Anal. Hybrid Syst"},{"key":"2_CR39","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Sathiyanarayana, V.: Sound and complete proof rules for probabilistic termination. Proc. ACM Program. Lang. 9(POPL), 1871\u20131902 (2025)","DOI":"10.1145\/3704899"},{"key":"2_CR40","doi-asserted-by":"crossref","unstructured":"Mallik, K., Soudjani, S.E.Z., Schmuck, A.K., Majumdar, R.: Compositional construction of finite state abstractions for stochastic control systems. In: 2017 IEEE 56th Annual Conference on Decision and Control (CDC), pp. 550\u2013557. IEEE (2017)","DOI":"10.1109\/CDC.2017.8263720"},{"key":"2_CR41","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1109\/LCSYS.2022.3229865","volume":"7","author":"FB Mathiesen","year":"2022","unstructured":"Mathiesen, F.B., Calvert, S.C., Laurenti, L.: Safety certification for stochastic systems via neural barrier functions. IEEE Control Syst. Lett. 7, 973\u2013978 (2022)","journal-title":"IEEE Control Syst. Lett."},{"key":"2_CR42","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, Heidelberg (2005)"},{"key":"2_CR43","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.P.: A new proof rule for almost-sure termination. Proc. ACM Program. Lang. 2(POPL), 1\u201328 (2017)","DOI":"10.1145\/3158121"},{"key":"2_CR44","unstructured":"Nagumo, M.: \u00dcber die lage der integralkurven gew\u00f6hnlicher differentialgleichungen. Proc. Physico-Math. Soc. Jpn. 3rd Series 24, 551\u2013559 (1942)"},{"key":"2_CR45","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2022.110513","volume":"145","author":"A Nejati","year":"2022","unstructured":"Nejati, A., Soudjani, S., Zamani, M.: Compositional construction of control barrier functions for continuous-time stochastic hybrid systems. Automatica 145, 110513 (2022)","journal-title":"Automatica"},{"key":"2_CR46","doi-asserted-by":"crossref","unstructured":"Neustroev, G., Giacobbe, M., Lukina, A.: Neural continuous-time supermartingale certificates. In: AAAI, pp. 27538\u201327546. AAAI Press (2025)","DOI":"10.1609\/aaai.v39i26.34966"},{"issue":"4","key":"2_CR47","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1145\/3296979.3192394","volume":"53","author":"VC Ngo","year":"2018","unstructured":"Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: resource analysis for probabilistic programs. ACM SIGPLAN Not. 53(4), 496\u2013512 (2018)","journal-title":"ACM SIGPLAN Not."},{"key":"2_CR48","doi-asserted-by":"publisher","unstructured":"Olmedo, F., Kaminski, B.L., Katoen, J.P., Matheja, C.: Reasoning about recursive probabilistic programs. In: LICS, pp. 672\u2013681 (2016). https:\/\/doi.org\/10.1145\/2933575.2935317","DOI":"10.1145\/2933575.2935317"},{"key":"2_CR49","doi-asserted-by":"crossref","unstructured":"Papachristodoulou, A., Prajna, S.: A tutorial on sum of squares techniques for systems analysis. In: Proceedings of the 2005, American Control Conference, 2005, pp. 2686\u20132700. IEEE (2005)","DOI":"10.1109\/ACC.2005.1470374"},{"key":"2_CR50","unstructured":"Parrilo, P.A.: Structured semidefinite programs and semialgebraic geometry methods in robustness and optimization. California Institute of Technology (2000)"},{"key":"2_CR51","doi-asserted-by":"crossref","unstructured":"Prajna, S., Jadbabaie, A., Pappas, G.J.: Stochastic safety verification using barrier certificates. In: 2004 43rd IEEE Conference on Decision and Control (CDC)(IEEE Cat. No. 04CH37601), vol.\u00a01, pp. 929\u2013934. IEEE (2004)","DOI":"10.1109\/CDC.2004.1428804"},{"key":"2_CR52","doi-asserted-by":"publisher","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics. Wiley, Hoboken (1994). https:\/\/doi.org\/10.1002\/9780470316887","DOI":"10.1002\/9780470316887"},{"issue":"3","key":"2_CR53","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 Univ. Math. J. 42(3), 969\u2013984 (1993)","journal-title":"Indiana Univ. Math. J."},{"key":"2_CR54","doi-asserted-by":"publisher","unstructured":"Sankaranarayanan, S., Chakarov, A., Gulwani, S.: Static analysis for probabilistic programs: inferring whole program properties from finitely many paths. In: Boehm, H., Flanagan, C. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201913, Seattle, WA, USA, 16\u201319 June 2013, pp. 447\u2013458. ACM (2013). https:\/\/doi.org\/10.1145\/2491956.2462179","DOI":"10.1145\/2491956.2462179"},{"key":"2_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-44667-2_6","volume-title":"Lectures on Formal Methods and PerformanceAnalysis","author":"R Segala","year":"2001","unstructured":"Segala, R.: Verification of randomized distributed algorithms. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) EEF School 2000. LNCS, vol. 2090, pp. 232\u2013260. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44667-2_6"},{"key":"2_CR56","doi-asserted-by":"crossref","unstructured":"Sloth, C.: On the computation of lyapunov functions for interconnected systems. In: 2016 IEEE Conference on Computer Aided Control System Design (CACSD), pp. 850\u2013855. IEEE (2016)","DOI":"10.1109\/CACSD.2016.7602545"},{"issue":"7","key":"2_CR57","doi-asserted-by":"publisher","first-page":"901","DOI":"10.1177\/0278364912444146","volume":"31","author":"J Steinhardt","year":"2012","unstructured":"Steinhardt, J., Tedrake, R.: Finite-time regional verification of stochastic non-linear systems. Int. J. Rob. Res. 31(7), 901\u2013923 (2012)","journal-title":"Int. J. Rob. Res."},{"issue":"2","key":"2_CR58","doi-asserted-by":"publisher","first-page":"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. (TOPLAS) 43(2), 1\u201346 (2021)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"2_CR59","doi-asserted-by":"publisher","unstructured":"Wang, J., Sun, Y., Fu, H., Chatterjee, K., Goharshady, A.K.: Quantitative analysis of assertion violations in probabilistic programs. In: Freund, S.N., Yahav, E. (eds.) PLDI \u201921: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, 20\u201325 June 2021, pp. 1171\u20131186. ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454102","DOI":"10.1145\/3453483.3454102"},{"key":"2_CR60","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, 22\u201326 June 2019, pp. 204\u2013220. ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314581","DOI":"10.1145\/3314221.3314581"},{"key":"2_CR61","doi-asserted-by":"crossref","unstructured":"Wang, P., Yang, T., Fu, H., Li, G., Ong, C.L.: Static posterior inference of bayesian probabilistic programming via polynomial solving. Proc. ACM Program. Lang. 8(PLDI), 1361\u20131386 (2024)","DOI":"10.1145\/3656432"},{"key":"2_CR62","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)"},{"key":"2_CR63","doi-asserted-by":"crossref","unstructured":"Xue, B., Zhan, N., Fr\u00e4nzle, M.: Reach-avoid analysis for polynomial stochastic differential equations. IEEE Trans. Autom. Control (2023)","DOI":"10.1109\/TAC.2023.3332570"},{"issue":"12","key":"2_CR64","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"},{"key":"2_CR65","doi-asserted-by":"publisher","unstructured":"Zhi, D., Wang, P., Liu, S., Ong, C.L., Zhang, M.: Unifying qualitative and quantitative safety verification of dnn-controlled systems. In: CAV (2). Lecture Notes in Computer Science, vol. 14682, pp. 401\u2013426. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-65630-9_20","DOI":"10.1007\/978-3-031-65630-9_20"},{"key":"2_CR66","doi-asserted-by":"crossref","unstructured":"\u017dikeli\u0107, \u0110., Lechner, M., Henzinger, T.A., Chatterjee, K.: Learning control policies for stochastic systems with reach-avoid guarantees. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a037, pp. 11926\u201311935 (2023)","DOI":"10.1609\/aaai.v37i10.26407"},{"key":"2_CR67","unstructured":"\u017dikeli\u0107, \u0110., Lechner, M., Verma, A., Chatterjee, K., Henzinger, T.: Compositional policy learning in stochastic control systems with formal guarantees. Adv. Neural Inf. Process. Syst. 36 (2024)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98679-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,7]],"date-time":"2025-09-07T16:18:09Z","timestamp":1757261889000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98679-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986789","9783031986796"],"references-count":67,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98679-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"22 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}