{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T19:34:28Z","timestamp":1757619268640,"version":"3.44.0"},"publisher-location":"Cham","reference-count":97,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031986789"},{"type":"electronic","value":"9783031986796"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T00:00:00Z","timestamp":1753142400000},"content-version":"vor","delay-in-days":202,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We consider the verification of neural network policies for discrete-time stochastic systems with respect to reach-avoid specifications. We use a learner-verifier procedure that learns a certificate for the specification, represented as a neural network. Verifying that this neural network certificate is a so-called reach-avoid supermartingale (RASM) proves the satisfaction of a reach-avoid specification. Existing approaches for such a verification task rely on computed Lipschitz constants of neural networks. These approaches struggle with large Lipschitz constants, especially for reach-avoid specifications with high threshold probabilities. We present two key contributions to obtain smaller Lipschitz constants than existing approaches. First, we introduce logarithmic RASMs (logRASMs), which take exponentially smaller values than RASMs and hence have lower theoretical Lipschitz constants. Second, we present a fast method to compute tighter upper bounds on Lipschitz constants based on weighted norms. Our empirical evaluation shows we can consistently verify the satisfaction of reach-avoid specifications with probabilities as high as\u00a0<jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$99.9999\\%$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mn>99.9999<\/mml:mn>\n                    <mml:mo>%<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>.<\/jats:p>","DOI":"10.1007\/978-3-031-98679-6_16","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T09:19:49Z","timestamp":1753089589000},"page":"349-375","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Policy Verification in\u00a0Stochastic Dynamical Systems Using Logarithmic Neural Certificates"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5235-1967","authenticated-orcid":false,"given":"Thom","family":"Badings","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9945-1992","authenticated-orcid":false,"given":"Wietze","family":"Koops","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0978-8466","authenticated-orcid":false,"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1318-8973","authenticated-orcid":false,"given":"Nils","family":"Jansen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Abate, A., Ahmed, D., Edwards, A., Giacobbe, M., Peruffo, A.: FOSSIL: a software tool for the formal synthesis of Lyapunov functions and barrier certificates using neural networks. In: HSCC, pp. 24:1\u201324:11. ACM (2021)","DOI":"10.1145\/3447928.3456646"},{"issue":"3","key":"16_CR2","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":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-319-96145-3_15","volume-title":"Computer Aided Verification","author":"A Abate","year":"2018","unstructured":"Abate, A., David, C., Kesseli, P., Kroening, D., Polgreen, E.: Counterexample guided inductive synthesis modulo theories. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 270\u2013288. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_15"},{"key":"16_CR4","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":"16_CR5","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":"16_CR6","doi-asserted-by":"publisher","unstructured":"Abate, A., Giacobbe, M., Roy, D.: Stochastic omega-regular verification and control with supermartingales. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 14683, pp. 395\u2013419. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65633-0_18","DOI":"10.1007\/978-3-031-65633-0_18"},{"issue":"11","key":"16_CR7","doi-asserted-by":"publisher","first-page":"2724","DOI":"10.1016\/j.automatica.2008.03.027","volume":"44","author":"A Abate","year":"2008","unstructured":"Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44(11), 2724\u20132734 (2008)","journal-title":"Automatica"},{"key":"16_CR8","unstructured":"Achiam, J., Held, D., Tamar, A., Abbeel, P.: Constrained policy optimization. In: ICML. Proceedings of Machine Learning Research, vol.\u00a070, pp. 22\u201331. PMLR (2017)"},{"key":"16_CR9","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":"16_CR10","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":"16_CR11","doi-asserted-by":"crossref","unstructured":"Altman, E.: Constrained Markov Decision Processes. Routledge (2021)","DOI":"10.1201\/9781315140223"},{"issue":"8","key":"16_CR12","doi-asserted-by":"publisher","first-page":"3861","DOI":"10.1109\/TAC.2016.2638961","volume":"62","author":"AD Ames","year":"2017","unstructured":"Ames, A.D., Xu, X., Grizzle, J.W., Tabuada, P.: Control barrier function based quadratic programs for safety critical systems. IEEE Trans. Autom. Control 62(8), 3861\u20133876 (2017)","journal-title":"IEEE Trans. Autom. Control"},{"key":"16_CR13","unstructured":"Amodei, D., Olah, C., Steinhardt, J., Christiano, P.F., Schulman, J., Man\u00e9, D.: Concrete problems in AI safety. CoRR abs\/1606.06565 (2016)"},{"key":"16_CR14","doi-asserted-by":"publisher","unstructured":"Ansaripour, M., Chatterjee, K., Henzinger, T.A., Lechner, M., Zikelic, D.: Learning provably stabilizing neural controllers for discrete-time stochastic systems. In: Andr\u00e9, \u00c9, Sun, J. (eds.) ATVA 2023. LNCS, vol. 14215. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-45329-8_17","DOI":"10.1007\/978-3-031-45329-8_17"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Avant, T., Morgansen, K.A.: Analytical bounds on the local Lipschitz constants of ReLU networks. IEEE Trans. Neural Netw. Learn. Syst. (2023)","DOI":"10.1109\/TNNLS.2023.3273228"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Badings, T., Koops, W., Junges, S., Jansen, N.: Policy verification in stochastic dynamical systems using logarithmic neural certificates (extended version). Technical report, CoRR, abs\/2406.00826 (2025)","DOI":"10.1007\/978-3-031-98679-6_16"},{"key":"16_CR17","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1613\/jair.1.14253","volume":"76","author":"TS Badings","year":"2023","unstructured":"Badings, T.S., et al.: Robust control for dynamical systems with non-Gaussian noise via formal abstractions. J. Artif. Intell. Res. 76, 341\u2013391 (2023)","journal-title":"J. Artif. Intell. Res."},{"key":"16_CR18","first-page":"1","volume":"4","author":"JB Baillon","year":"1978","unstructured":"Baillon, J.B., Bruck, R.E., Reich, S.: On the asymptotic behavior of nonexpansive mappings and semigroups in Banach spaces. Houston J. Math. 4, 1\u20139 (1978)","journal-title":"Houston J. Math."},{"key":"16_CR19","unstructured":"Berkenkamp, F., Turchetta, M., Schoellig, A.P., Krause, A.: Safe model-based reinforcement learning with stability guarantees. In: NIPS, pp. 908\u2013918 (2017)"},{"key":"16_CR20","unstructured":"Bertsekas, D.: Reinforcement Learning and Optimal Control, vol.\u00a01. Athena Scientific (2019)"},{"key":"16_CR21","unstructured":"Bertsekas, D.P., Shreve, S.E.: Stochastic Optimal Control: The Discrete-time Case. Athena Scientific (1978)"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-030-86380-7_13","volume-title":"Artificial Neural Networks and Machine Learning \u2013 ICANN 2021","author":"A Bhowmick","year":"2021","unstructured":"Bhowmick, A., D\u2019Souza, M., Raghavan, G.S.: LipBaB: computing exact Lipschitz constant of ReLU networks. In: Farka\u0161, I., Masulli, P., Otte, S., Wermter, S. (eds.) ICANN 2021. LNCS, vol. 12894, pp. 151\u2013162. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86380-7_13"},{"key":"16_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-642-40994-3_25","volume-title":"Machine Learning and Knowledge Discovery in Databases","author":"B Biggio","year":"2013","unstructured":"Biggio, B., et al.: Evasion attacks against machine learning at test time. In: Blockeel, H., Kersting, K., Nijssen, S., \u017delezn\u00fd, F. (eds.) ECML PKDD 2013. LNCS (LNAI), vol. 8190, pp. 387\u2013402. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40994-3_25"},{"key":"16_CR24","unstructured":"Bradbury, J., et al.: JAX: composable transformations of Python+NumPy programs (2018). http:\/\/github.com\/google\/jax"},{"key":"16_CR25","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":"16_CR26","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1146\/annurev-control-042920-020211","volume":"5","author":"L Brunke","year":"2022","unstructured":"Brunke, L., et al.: Safe learning in robotics: from learning-based control to safe reinforcement learning. Annu. Rev. Control. Robotics Auton. Syst. 5, 411\u2013444 (2022)","journal-title":"Annu. Rev. Control. Robotics Auton. Syst."},{"key":"16_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-030-75549-2_25","volume-title":"Scale Space and Variational Methods in Computer Vision","author":"L Bungert","year":"2021","unstructured":"Bungert, L., Raab, R., Roith, T., Schwinn, L., Tenbrinck, D.: CLIP: cheap Lipschitz training of neural networks. In: Elmoataz, A., Fadili, J., Qu\u00e9au, Y., Rabin, J., Simon, L. (eds.) SSVM 2021. LNCS, vol. 12679, pp. 307\u2013319. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-75549-2_25"},{"key":"16_CR28","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1016\/j.arcontrol.2018.09.005","volume":"46","author":"L Busoniu","year":"2018","unstructured":"Busoniu, L., de Bruin, T., Tolic, D., Kober, J., Palunko, I.: Reinforcement learning for control: performance, stability, and deep approximators. Annu. Rev. Control. 46, 8\u201328 (2018)","journal-title":"Annu. Rev. Control."},{"key":"16_CR29","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":"16_CR30","unstructured":"Chang, Y., Roohi, N., Gao, S.: Neural Lyapunov control. In: NeurIPS, pp. 3240\u20133249 (2019)"},{"key":"16_CR31","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, T.A., Lechner, M., Zikelic, 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)","DOI":"10.1007\/978-3-031-30823-9_1"},{"key":"16_CR32","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Novotn\u00fd, P., Zikelic, D.: Stochastic invariants for probabilistic termination. In: POPL, pp. 145\u2013160. ACM (2017)","DOI":"10.1145\/3009837.3009873"},{"key":"16_CR33","doi-asserted-by":"crossref","unstructured":"Choi, J.J., Casta\u00f1eda, F., Tomlin, C.J., Sreenath, K.: Reinforcement learning for safety-critical control under model uncertainty, using control Lyapunov functions and control barrier functions. Rob. Sci. Syst. (2020)","DOI":"10.15607\/RSS.2020.XVI.088"},{"key":"16_CR34","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2021.109688","volume":"130","author":"A Clark","year":"2021","unstructured":"Clark, A.: Control barrier functions for stochastic systems. Automatica 130, 109688 (2021)","journal-title":"Automatica"},{"issue":"5","key":"16_CR35","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"issue":"2","key":"16_CR36","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1137\/19M1272780","volume":"2","author":"PL Combettes","year":"2020","unstructured":"Combettes, P.L., Pesquet, J.C.: Lipschitz certificates for layered network structures driven by averaged activation operators. SIAM J. Math. Data Sci. 2(2), 529\u2013557 (2020)","journal-title":"SIAM J. Math. Data Sci."},{"key":"16_CR37","unstructured":"Dalrymple, D., et al.: Towards guaranteed safe AI: a framework for ensuring robust and reliable AI systems. CoRR abs\/2405.06624 (2024)"},{"issue":"3","key":"16_CR38","doi-asserted-by":"publisher","first-page":"1749","DOI":"10.1109\/TRO.2022.3232542","volume":"39","author":"C Dawson","year":"2023","unstructured":"Dawson, C., Gao, S., Fan, C.: Safe control with learned certificates: a survey of neural Lyapunov, barrier, and contraction methods for robotics and control. IEEE Trans. Rob. 39(3), 1749\u20131767 (2023)","journal-title":"IEEE Trans. Rob."},{"key":"16_CR39","doi-asserted-by":"publisher","unstructured":"De\u00a0Queiroz, M.S., Dawson, D.M., Nagarkatti, S.P., Zhang, F.: Lyapunov-based control of mechanical systems. Springer Science & Business Media, Boston (2000). https:\/\/doi.org\/10.1007\/978-1-4612-1352-9","DOI":"10.1007\/978-1-4612-1352-9"},{"key":"16_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-540-75454-1_10","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"H Dierks","year":"2007","unstructured":"Dierks, H., Kupferschmid, S., Larsen, K.G.: Automatic abstraction refinement for timed automata. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 114\u2013129. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75454-1_10"},{"key":"16_CR41","unstructured":"Duan, Y., Chen, X., Houthooft, R., Schulman, J., Abbeel, P.: Benchmarking deep reinforcement learning for continuous control. In: ICML. JMLR Workshop and Conference Proceedings, vol.\u00a048, pp. 1329\u20131338. JMLR.org (2016)"},{"key":"16_CR42","unstructured":"Durrett, R.: Stochastic Calculus: A Practical Introduction, 1st edn. CRC Press (1996)"},{"key":"16_CR43","unstructured":"Eiras, F., et al.: ANCER: anisotropic certification via sample-wise volume maximization. Trans. Mach. Learn. Res. 2022 (2022)"},{"key":"16_CR44","unstructured":"Fazlyab, M., Robey, A., Hassani, H., Morari, M., Pappas, G.J.: Efficient and accurate estimation of Lipschitz constants for deep neural networks. In: NeurIPS, pp. 11423\u201311434 (2019)"},{"key":"16_CR45","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\/2676726.2677001"},{"key":"16_CR46","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning Meanings to Programs, pp. 65\u201381 (1993)","DOI":"10.1007\/978-94-011-1793-7_4"},{"key":"16_CR47","first-page":"1437","volume":"16","author":"J Garc\u00eda","year":"2015","unstructured":"Garc\u00eda, J., Fern\u00e1ndez, F.: A comprehensive survey on safe reinforcement learning. J. Mach. Learn. Res. 16, 1437\u20131480 (2015)","journal-title":"J. Mach. Learn. Res."},{"key":"16_CR48","doi-asserted-by":"crossref","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.T.: AI2: safety and robustness certification of neural networks with abstract interpretation. In: IEEE Symposium on Security and Privacy, pp. 3\u201318. IEEE Computer Society (2018)","DOI":"10.1109\/SP.2018.00058"},{"key":"16_CR49","unstructured":"G\u00f3mez, F.L., Rolland, P., Cevher, V.: Lipschitz constant estimation of neural networks via sparse polynomial optimization. In: ICLR. OpenReview.net (2020)"},{"issue":"2","key":"16_CR50","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/s10994-020-05929-w","volume":"110","author":"H Gouk","year":"2021","unstructured":"Gouk, H., Frank, E., Pfahringer, B., Cree, M.J.: Regularisation of neural networks by enforcing Lipschitz continuity. Mach. Learn. 110(2), 393\u2013416 (2021)","journal-title":"Mach. Learn."},{"key":"16_CR51","unstructured":"Gowal, S., et al.: On the effectiveness of interval bound propagation for training verifiably robust models. CoRR abs\/1810.12715 (2018)"},{"key":"16_CR52","unstructured":"Gracia, I., Laurenti, L., Jr., M.M., Abate, A., Lahijanian, M.: Temporal logic control for nonlinear stochastic systems under unknown disturbances (2024)"},{"key":"16_CR53","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosrev.2020.100270","volume":"37","author":"X Huang","year":"2020","unstructured":"Huang, X., et al.: A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability. Comput. Sci. Rev. 37, 100270 (2020)","journal-title":"Comput. Sci. Rev."},{"key":"16_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-63387-9_1","volume-title":"Computer Aided Verification","author":"X Huang","year":"2017","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 3\u201329. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_1"},{"key":"16_CR55","doi-asserted-by":"crossref","unstructured":"Jackson, J., Laurenti, L., Frew, E.W., Lahijanian, M.: Strategy synthesis for partially-known switched stochastic systems. In: HSCC, pp. 6:1\u20136:11. ACM (2021)","DOI":"10.1145\/3447928.3456649"},{"issue":"7","key":"16_CR56","doi-asserted-by":"publisher","first-page":"3097","DOI":"10.1109\/TAC.2020.3013916","volume":"66","author":"P Jagtap","year":"2021","unstructured":"Jagtap, P., Soudjani, S., Zamani, M.: Formal synthesis of stochastic systems via control barrier certificates. IEEE Trans. Autom. Control 66(7), 3097\u20133110 (2021)","journal-title":"IEEE Trans. Autom. Control"},{"key":"16_CR57","unstructured":"Jordan, M., Dimakis, A.G.: Exactly computing the local Lipschitz constant of ReLU networks. In: NeurIPS (2020)"},{"key":"16_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-319-63387-9_5","volume-title":"Computer Aided Verification","author":"G Katz","year":"2017","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 97\u2013117. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5"},{"key":"16_CR59","volume-title":"Nonlinear Systems","author":"HK Khalil","year":"2002","unstructured":"Khalil, H.K., Grizzle, J.W.: Nonlinear Systems, vol. 3. Prentice hall Upper Saddle River, NJ (2002)"},{"key":"16_CR60","doi-asserted-by":"crossref","unstructured":"Kurakin, A., Goodfellow, I.J., Bengio, S.: Adversarial examples in the physical world. In: ICLR (Workshop). OpenReview.net (2017)","DOI":"10.1201\/9781351251389-8"},{"issue":"8","key":"16_CR61","doi-asserted-by":"publisher","first-page":"2031","DOI":"10.1109\/TAC.2015.2398883","volume":"60","author":"M Lahijanian","year":"2015","unstructured":"Lahijanian, M., Andersson, S.B., Belta, C.: Formal verification and synthesis for discrete-time stochastic systems. IEEE Trans. Autom. Control 60(8), 2031\u20132045 (2015)","journal-title":"IEEE Trans. Autom. Control"},{"key":"16_CR62","doi-asserted-by":"crossref","unstructured":"Lechner, M., Zikelic, 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":"16_CR63","unstructured":"Lillicrap, T.P., et al.: Continuous control with deep reinforcement learning. In: ICLR (Poster) (2016)"},{"issue":"1","key":"16_CR64","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1109\/LCSYS.2018.2853182","volume":"3","author":"L Lindemann","year":"2019","unstructured":"Lindemann, L., Dimarogonas, D.V.: Control barrier functions for signal temporal logic tasks. IEEE Control. Syst. Lett. 3(1), 96\u2013101 (2019)","journal-title":"IEEE Control. Syst. Lett."},{"key":"16_CR65","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1109\/LCSYS.2022.3229865","volume":"7","author":"FB Mathiesen","year":"2023","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 (2023)","journal-title":"IEEE Control. Syst. Lett."},{"key":"16_CR66","unstructured":"Mazouz, R., Mathiesen, F.B., Laurenti, L., Lahijanian, M.: Piecewise stochastic barrier functions. CoRR abs\/2404.16986 (2024)"},{"key":"16_CR67","unstructured":"Mazouz, R., Muvvala, K., Ratheesh, A., Laurenti, L., Lahijanian, M.: Safety guarantees for neural network dynamic systems via stochastic barrier functions. In: NeurIPS (2022)"},{"key":"16_CR68","unstructured":"Nadali, A., Zhong, B., Trivedi, A., Zamani, M.: Transfer learning for control systems via neural simulation relations. CoRR abs\/2412.01783 (2024)"},{"key":"16_CR69","unstructured":"Neustroev, G., Giacobbe, M., Lukina, A.: Neural continuous-time supermartingale certificates (2024). https:\/\/arxiv.org\/abs\/2412.17432"},{"key":"16_CR70","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1109\/LCSYS.2021.3050444","volume":"6","author":"P Pauli","year":"2022","unstructured":"Pauli, P., Koch, A., Berberich, J., Kohler, P., Allg\u00f6wer, F.: Training robust neural networks using Lipschitz bounds. IEEE Control. Syst. Lett. 6, 121\u2013126 (2022)","journal-title":"IEEE Control. Syst. Lett."},{"key":"16_CR71","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"},{"issue":"8","key":"16_CR72","doi-asserted-by":"publisher","first-page":"1415","DOI":"10.1109\/TAC.2007.902736","volume":"52","author":"S Prajna","year":"2007","unstructured":"Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Autom. Control 52(8), 1415\u20131428 (2007)","journal-title":"IEEE Trans. Autom. Control"},{"key":"16_CR73","doi-asserted-by":"crossref","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics, Wiley (1994)","DOI":"10.1002\/9780470316887"},{"key":"16_CR74","unstructured":"Raffin, A., Hill, A., Gleave, A., Kanervisto, A., Ernestus, M., Dormann, N.: Stable-Baselines3: reliable reinforcement learning implementations. J. Mach. Learn. Res. 22, 268:1\u2013268:8 (2021)"},{"key":"16_CR75","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1146\/annurev-control-053018-023825","volume":"2","author":"B Recht","year":"2019","unstructured":"Recht, B.: A tour of reinforcement learning: the view from continuous control. Annu. Rev. Control. Robotics Auton. Syst. 2, 253\u2013279 (2019)","journal-title":"Annu. Rev. Control. Robotics Auton. Syst."},{"key":"16_CR76","unstructured":"Richards, S.M., Berkenkamp, F., Krause, A.: The Lyapunov neural network: adaptive stability certification for safe learning of dynamical systems. In: CoRL. Proceedings of Machine Learning Research, vol.\u00a087, pp. 466\u2013476. PMLR (2018)"},{"key":"16_CR77","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2020.109439","volume":"125","author":"C Santoyo","year":"2021","unstructured":"Santoyo, C., Dutreix, M., Coogan, S.: A barrier function approach to finite-time stochastic system verification and control. Automatica 125, 109439 (2021)","journal-title":"Automatica"},{"key":"16_CR78","unstructured":"Schulman, J., Wolski, F., Dhariwal, P., Radford, A., Klimov, O.: Proximal policy optimization algorithms. CoRR abs\/1707.06347 (2017)"},{"key":"16_CR79","unstructured":"Shi, Z., Jin, Q., Kolter, Z., Jana, S., Hsieh, C., Zhang, H.: Neural network verification with branch-and-bound for general nonlinearities. CoRR abs\/2405.21063 (2024)"},{"key":"16_CR80","unstructured":"Shi, Z., Wang, Y., Zhang, H., Kolter, J.Z., Hsieh, C.: Efficiently computing local Lipschitz constants of neural networks via bound propagation. In: NeurIPS (2022)"},{"key":"16_CR81","doi-asserted-by":"crossref","unstructured":"Steinhardt, J., Tedrake, R.: Finite-time regional verification of stochastic nonlinear systems. In: Robotics: Science and Systems (2011)","DOI":"10.15607\/RSS.2011.VII.041"},{"issue":"12","key":"16_CR82","doi-asserted-by":"publisher","first-page":"1951","DOI":"10.1016\/j.automatica.2010.08.006","volume":"46","author":"S Summers","year":"2010","unstructured":"Summers, S., Lygeros, J.: Verification of discrete time stochastic hybrid systems: a stochastic reach-avoid decision problem. Automatica 46(12), 1951\u20131961 (2010)","journal-title":"Automatica"},{"key":"16_CR83","unstructured":"Szegedy, C., et al.: Intriguing properties of neural networks. In: ICLR (Poster) (2014)"},{"key":"16_CR84","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":"16_CR85","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/3-540-45873-5_36","volume-title":"Hybrid Systems: Computation and Control","author":"A Tiwari","year":"2002","unstructured":"Tiwari, A., Khanna, G.: Series of abstractions for hybrid automata. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 465\u2013478. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45873-5_36"},{"key":"16_CR86","unstructured":"Virmaux, A., Scaman, K.: Lipschitz regularity of deep neural networks: analysis and efficient estimation. In: NeurIPS, pp. 3839\u20133848 (2018)"},{"key":"16_CR87","unstructured":"Wang, Z., et al.: On the scalability and memory efficiency of semidefinite programs for Lipschitz constant estimation of neural networks. In: ICLR (2024)"},{"key":"16_CR88","unstructured":"Weng, T., et al.: Towards fast computation of certified robustness for ReLU networks. In: ICML. Proceedings of Machine Learning Research, vol.\u00a080, pp. 5273\u20135282. PMLR (2018)"},{"key":"16_CR89","unstructured":"Williams, D.: Probability with Martingales. Cambridge Mathematical Textbooks. Cambridge University Press (1991)"},{"key":"16_CR90","unstructured":"Wu, J., Clark, A., Kantaros, Y., Vorobeychik, Y.: Neural Lyapunov control for discrete-time systems. In: NeurIPS (2023)"},{"issue":"12","key":"16_CR91","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":"16_CR92","doi-asserted-by":"crossref","unstructured":"Zhang, H., Zhang, P., Hsieh, C.: RecurJac: an efficient recursive algorithm for bounding Jacobian matrix of neural networks and its applications. In: AAAI, pp. 5757\u20135764. AAAI Press (2019)","DOI":"10.1609\/aaai.v33i01.33015757"},{"issue":"6","key":"16_CR93","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."},{"key":"16_CR94","unstructured":"Zhou, R., Quartz, T., Sterck, H.D., Liu, J.: Neural Lyapunov control of unknown nonlinear systems with stability guarantees. In: NeurIPS (2022)"},{"key":"16_CR95","doi-asserted-by":"crossref","unstructured":"Zikelic, D., Lechner, M., Henzinger, T.A., Chatterjee, K.: Learning control policies for stochastic systems with reach-avoid guarantees. In: AAAI, pp. 11926\u201311935. AAAI Press (2023)","DOI":"10.1609\/aaai.v37i10.26407"},{"key":"16_CR96","unstructured":"Zikelic, D., Lechner, M., Verma, A., Chatterjee, K., Henzinger, T.A.: Compositional policy learning in stochastic control systems with formal guarantees. In: NeurIPS (2023)"},{"key":"16_CR97","doi-asserted-by":"crossref","unstructured":"Z\u00fchlke, M.M., Kudenko, D.: Adversarial robustness of neural networks from the perspective of Lipschitz calculus: a survey. ACM Comput. Surv. (2024)","DOI":"10.1145\/3648351"}],"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_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,7]],"date-time":"2025-09-07T16:18:46Z","timestamp":1757261926000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98679-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986789","9783031986796"],"references-count":97,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98679-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"22 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}