{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:39:36Z","timestamp":1780994376726,"version":"3.54.1"},"publisher-location":"Cham","reference-count":72,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656293","type":"print"},{"value":"9783031656309","type":"electronic"}],"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,25]],"date-time":"2024-07-25T00:00:00Z","timestamp":1721865600000},"content-version":"vor","delay-in-days":206,"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>The rapid advance of deep reinforcement learning techniques enables the oversight of safety-critical systems through the utilization of Deep Neural Networks (DNNs). This underscores the pressing need to promptly establish certified safety guarantees for such DNN-controlled systems. Most of the existing verification approaches rely on qualitative approaches, predominantly employing reachability analysis. However, qualitative verification proves inadequate for DNN-controlled systems as their behaviors exhibit stochastic tendencies when operating in open and adversarial environments. In this paper, we propose a novel framework for unifying both qualitative and quantitative safety verification problems of DNN-controlled systems. This is achieved by formulating the verification tasks as the synthesis of valid neural barrier certificates (NBCs). Initially, the framework seeks to establish almost-sure safety guarantees through qualitative verification. In cases where qualitative verification fails, our quantitative verification method is invoked, yielding precise lower and upper bounds on probabilistic safety across both infinite and finite time horizons. To facilitate the synthesis of NBCs, we introduce their<jats:italic>k<\/jats:italic>-inductive variants. We also devise a simulation-guided approach for training NBCs, aiming to achieve tightness in computing precise certified lower and upper bounds. We prototype our approach into a tool called and showcase its efficacy on four classic DNN-controlled systems.<\/jats:p>","DOI":"10.1007\/978-3-031-65630-9_20","type":"book-chapter","created":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T22:01:56Z","timestamp":1721858516000},"page":"401-426","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Unifying Qualitative and\u00a0Quantitative Safety Verification of\u00a0DNN-Controlled Systems"],"prefix":"10.1007","author":[{"given":"Dapeng","family":"Zhi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3241-0023","authenticated-orcid":false,"given":"Peixin","family":"Wang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3578-7432","authenticated-orcid":false,"given":"Si","family":"Liu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7509-680X","authenticated-orcid":false,"given":"C.-H. Luke","family":"Ong","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1938-2902","authenticated-orcid":false,"given":"Min","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,7,25]]},"reference":[{"key":"20_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 (2021)","DOI":"10.1145\/3447928.3456646"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Abate, A., David, C., Kesseli, P., Kroening, D., Polgreen, E.: Counterexample guided inductive synthesis modulo theories. In: CAV, pp. 270\u2013288 (2018)","DOI":"10.1007\/978-3-319-96145-3_15"},{"key":"20_CR3","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 (2023)"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Ames, A.D., Coogan, S., Egerstedt, M., Notomista, G., Sreenath, K., Tabuada, P.: Control barrier functions: Theory and applications. In: ECC, pp. 3420\u20133431 (2019)","DOI":"10.23919\/ECC.2019.8796030"},{"key":"20_CR5","unstructured":"Amir, G., Schapira, M., Katz, G.: Towards scalable verification of deep reinforcement learning. In: FMCAD, pp. 193\u2013203 (2021)"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Anand, M., Murali, V., Trivedi, A., Zamani, M.: k-inductive barrier certificates for stochastic systems. In: HSCC, pp. 12:1\u201312:11 (2022)","DOI":"10.1145\/3501710.3519532"},{"key":"20_CR7","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 (2021)","DOI":"10.1145\/3453483.3454076"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Bacci, E., Giacobbe, M., Parker, D.: Verifying reinforcement learning up to infinity. In: IJCAI, pp. 2154\u20132160 (2021)","DOI":"10.24963\/ijcai.2021\/297"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Bacci, E., Parker, D.: Probabilistic guarantees for safe deep reinforcement learning. In: FORMATS, pp. 231\u2013248 (2020)","DOI":"10.1007\/978-3-030-57628-8_14"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Bacci, E., Parker, D.: Verified probabilistic policies for deep reinforcement learning. In: NFM, pp. 193\u2013212 (2022)","DOI":"10.1007\/978-3-031-06773-0_10"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Brain, M., Joshi, S., Kroening, D., Schrammel, P.: Safety verification and refutation by k-invariants and k-induction. In: SAS, pp. 145\u2013161 (2015)","DOI":"10.1007\/978-3-662-48288-9_9"},{"key":"20_CR12","unstructured":"Brockman, G., et al.: OpenAI Gym (2016). arXiv:1606.01540"},{"issue":"9","key":"20_CR13","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/2330667.2330686","volume":"55","author":"R Calinescu","year":"2012","unstructured":"Calinescu, R., Ghezzi, C., Kwiatkowska, M., Mirandola, R.: Self-adaptive software needs quantitative verification at runtime. Commun. ACM 55(9), 69\u201377 (2012)","journal-title":"Commun. ACM"},{"key":"20_CR14","doi-asserted-by":"publisher","first-page":"819","DOI":"10.1613\/jair.1.12963","volume":"72","author":"S Carr","year":"2021","unstructured":"Carr, S., Jansen, N., Topcu, U.: Task-aware verifiable RNN-based policies for partially observable markov decision processes. Artif. Intell. Res. 72, 819\u2013847 (2021)","journal-title":"Artif. Intell. Res."},{"key":"20_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":"20_CR16","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. In: POPL, pp. 327\u2013342 (2016)","DOI":"10.1145\/2914770.2837639"},{"issue":"1","key":"20_CR17","doi-asserted-by":"publisher","first-page":"43","DOI":"10.2140\/pjm.1979.82.43","volume":"82","author":"P Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Constructive versions of tarski\u2019s fixed point theorems. Pac. J. Math. 82(1), 43\u201357 (1979)","journal-title":"Pac. J. Math."},{"key":"20_CR18","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. Robot. 39, 1749\u20131767 (2023)","journal-title":"IEEE Trans. Robot."},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"Deshmukh, J., Kapinski, J., Yamaguchi, T., Prokhorov, D.: Learning deep neural network controllers for dynamical systems with safety guarantees. In: ICCAD, pp.\u00a01\u20137 (2019)","DOI":"10.1109\/ICCAD45719.2019.8942130"},{"key":"20_CR20","doi-asserted-by":"crossref","unstructured":"Donaldson, A.F., Haller, L., Kroening, D., R\u00fcmmer, P.: Software verification using k-induction. In: SAS, pp. 351\u2013368 (2011)","DOI":"10.1007\/978-3-642-23702-7_26"},{"issue":"OOPSLA1","key":"20_CR21","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1145\/3586051","volume":"7","author":"S Feng","year":"2023","unstructured":"Feng, S., Chen, M., Su, H., Kaminski, B.L., Katoen, J., Zhan, N.: Lower bounds for possibly divergent probabilistic programs. Proc. ACM Program. Lang. 7(OOPSLA1), 696\u2013726 (2023)","journal-title":"Proc. ACM Program. Lang."},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Feng, S., Chen, M., Xue, B., Sankaranarayanan, S., Zhan, N.: Unbounded-time safety verification of stochastic differential dynamics. In: CAV, pp. 327\u2013348 (2020)","DOI":"10.1007\/978-3-030-53291-8_18"},{"key":"20_CR23","unstructured":"Gowal, S., et al.: On the effectiveness of interval bound propagation for training verifiably robust models. CoRR arXiv: 1810.12715 (2018)"},{"key":"20_CR24","doi-asserted-by":"crossref","unstructured":"Gronwall, T.H.: Note on the derivatives with respect to a parameter of the solutions of a system of differential equations. Annals Math. 292\u2013296 (1919)","DOI":"10.2307\/1967124"},{"key":"20_CR25","doi-asserted-by":"crossref","unstructured":"Hahn, E.M., et al.: The 2019 comparison of tools for the analysis of quantitative formal models: (QComp 2019 competition report). In: TACAS, pp. 69\u201392 (2019)","DOI":"10.1007\/978-3-030-17502-3_5"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Hamers, R., Jongmans, S.: Discourje: Runtime verification of communication protocols in clojure. In: TACAS, pp. 266\u2013284 (2020)","DOI":"10.1007\/978-3-030-45190-5_15"},{"key":"20_CR27","doi-asserted-by":"crossref","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker storm. Inter. J. Softw. Tools Technol. Trans. 1\u201322 (2021)","DOI":"10.1007\/s10009-021-00633-z"},{"key":"20_CR28","doi-asserted-by":"crossref","unstructured":"Hoeffding, W.: Probability inequalities for sums of bounded random variables. The collected works of Wassily Hoeffding, pp. 409\u2013426 (1994)","DOI":"10.1007\/978-1-4612-0865-5_26"},{"key":"20_CR29","doi-asserted-by":"crossref","unstructured":"Huang, C., Fan, J., Chen, X., Li, W., Zhu, Q.: Polar: a polynomial arithmetic framework for verifying neural-network controlled systems. In: ATVA, pp. 414\u2013430 (2022)","DOI":"10.1007\/978-3-031-19992-9_27"},{"key":"20_CR30","doi-asserted-by":"crossref","unstructured":"Ivanov, R., Carpenter, T., Weimer, J., Alur, R., Pappas, G., Lee, I.: Verisig 2.0: Verification of neural network controllers using taylor model preconditioning. In: CAV, pp. 249\u2013262 (2021)","DOI":"10.1007\/978-3-030-81685-8_11"},{"key":"20_CR31","doi-asserted-by":"crossref","unstructured":"Jin, P., Tian, J., Zhi, D., et\u00a0al.: Trainify: a CEGAR-driven training and verification framework for safe deep reinforcement learning. In: CAV, pp. 193\u2013218 (2022)","DOI":"10.1007\/978-3-031-13185-1_10"},{"key":"20_CR32","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Prism 4.0: verification of probabilistic real-time systems. In: CAV, pp. 585\u2013591 (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"20_CR33","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1146\/annurev-control-042820-010947","volume":"5","author":"M Kwiatkowska","year":"2022","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking and autonomy. Annu. Rev. Control Robot. Auton. Syst. 5, 385\u2013410 (2022)","journal-title":"Annu. Rev. Control Robot. Auton. Syst."},{"key":"20_CR34","doi-asserted-by":"crossref","unstructured":"Lavaei, A., Soudjani, S., Frazzoli, E.: Safety barrier certificates for stochastic hybrid systems. In: ACC, pp. 880\u2013885 (2022)","DOI":"10.23919\/ACC53348.2022.9867754"},{"key":"20_CR35","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 (2022)","DOI":"10.1609\/aaai.v36i7.20695"},{"key":"20_CR36","unstructured":"Lillicrap, T., et al.: Continuous control with deep reinforcement learning. CoRR abs\/ arXiv: 1509.02971 (2015)"},{"key":"20_CR37","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":"20_CR38","doi-asserted-by":"crossref","unstructured":"Meng, Y., Qin, Z., Fan, C.: Reactive and safe road user simulations using neural barrier certificates. In: IROS, pp. 6299\u20136306 (2021)","DOI":"10.1109\/IROS51168.2021.9636568"},{"key":"20_CR39","doi-asserted-by":"crossref","unstructured":"Murali, V., Trivedi, A., Zamani, M.: Closure certificates. In: HSCC, pp. 10:1\u201310:11 (2024)","DOI":"10.1145\/3641513.3650120"},{"key":"20_CR40","doi-asserted-by":"crossref","unstructured":"Nadali, A., Murali, V., Trivedi, A., Zamani, M.: Neural closure certificates. In: AAAI, pp. 21446\u201321453 (2024)","DOI":"10.1609\/aaai.v38i19.30141"},{"key":"20_CR41","doi-asserted-by":"crossref","unstructured":"Peruffo, A., Ahmed, D., Abate, A.: Automated and formal synthesis of neural barrier certificates for dynamical models. In: TACAS, pp. 370\u2013388 (2021)","DOI":"10.1007\/978-3-030-72016-2_20"},{"key":"20_CR42","doi-asserted-by":"crossref","unstructured":"Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC, pp. 477\u2013492 (2004)","DOI":"10.1007\/978-3-540-24743-2_32"},{"issue":"8","key":"20_CR43","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. Automat. Contr. 52(8), 1415\u20131428 (2007)","journal-title":"IEEE Trans. Automat. Contr."},{"issue":"1","key":"20_CR44","doi-asserted-by":"publisher","first-page":"526","DOI":"10.3182\/20050703-6-CZ-1902.00743","volume":"38","author":"S Prajna","year":"2005","unstructured":"Prajna, S., Rantzer, A.: On the necessity of barrier certificates. IFAC Proc. Vol. 38(1), 526\u2013531 (2005)","journal-title":"IFAC Proc. Vol."},{"key":"20_CR45","doi-asserted-by":"crossref","unstructured":"Salamati, A., Lavaei, A., Soudjani, S., Zamani, M.: Data-driven safety verification of stochastic systems via barrier certificates. In: ADHS, pp. 7\u201312 (2021)","DOI":"10.1016\/j.ifacol.2021.08.466"},{"issue":"3","key":"20_CR46","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1109\/JPROC.2021.3060483","volume":"109","author":"W Samek","year":"2021","unstructured":"Samek, W., Montavon, G., Lapuschkin, S., et al.: Explaining deep neural networks and beyond: a review of methods and applications. Proc. IEEE 109(3), 247\u2013278 (2021)","journal-title":"Proc. IEEE"},{"issue":"7","key":"20_CR47","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/3503914","volume":"65","author":"SA Seshia","year":"2022","unstructured":"Seshia, S.A., Sadigh, D., Sastry, S.S.: Toward verified artificial intelligence. Commun. ACM 65(7), 46\u201355 (2022)","journal-title":"Commun. ACM"},{"key":"20_CR48","doi-asserted-by":"crossref","unstructured":"Sha, M., et al.: Synthesizing barrier certificates of neural network controlled continuous systems via approximations. In: DAC, pp. 631\u2013636 (2021)","DOI":"10.1109\/DAC18074.2021.9586327"},{"issue":"7","key":"20_CR49","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. Robotics Res. 31(7), 901\u2013923 (2012)","journal-title":"Int. J. Robotics Res."},{"key":"20_CR50","doi-asserted-by":"crossref","unstructured":"Takisaka, T., Oyabu, Y., Urabe, N., Hasuo, I.: Ranking and repulsing supermartingales for reachability in probabilistic programs. In: ATVA, pp. 476\u2013493 (2018)","DOI":"10.1007\/978-3-030-01090-4_28"},{"key":"20_CR51","doi-asserted-by":"crossref","unstructured":"Takisaka, T., Oyabu, Y., Urabe, N., Hasuo, I.: Ranking and repulsing supermartingales for reachability in randomized programs. ACM Trans. Prog. Lang. Syst. 43(2), 5:1\u20135:46 (2021)","DOI":"10.1145\/3450967"},{"key":"20_CR52","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2013.08.016","volume":"517","author":"M Tschaikowski","year":"2014","unstructured":"Tschaikowski, M., Tribastone, M.: Tackling continuous state-space explosion in a markovian process algebra. Theoret. Comput. Sci. 517, 1\u201333 (2014)","journal-title":"Theoret. Comput. Sci."},{"key":"20_CR53","doi-asserted-by":"crossref","unstructured":"Urabe, N., Hara, M., Hasuo, I.: Categorical liveness checking by corecursive algebras. In: LICS, pp. 1\u201312 (2017)","DOI":"10.1109\/LICS.2017.8005151"},{"key":"20_CR54","unstructured":"Ville, J.: Etude critique de la notion de collectif (1939)"},{"key":"20_CR55","doi-asserted-by":"crossref","unstructured":"Wan, X., Zeng, L., Sun, M.: Exploring the vulnerability of deep reinforcement learning-based emergency control for low carbon power systems. In: IJCAI, pp. 3954\u20133961 (2022)","DOI":"10.24963\/ijcai.2022\/549"},{"key":"20_CR56","doi-asserted-by":"crossref","unstructured":"Williams, D.: Probability with martingales. Cambridge university press (1991)","DOI":"10.1017\/CBO9780511813658"},{"key":"20_CR57","doi-asserted-by":"crossref","unstructured":"Winkler, T., Gehnen, C., Katoen, J.: Model checking temporal properties of recursive probabilistic programs. In: FOSSACS, pp. 449\u2013469 (2022)","DOI":"10.1007\/978-3-030-99253-8_23"},{"key":"20_CR58","doi-asserted-by":"crossref","unstructured":"Xia, J., Hu, M., Chen, X., Chen, M.: Accelerated synthesis of neural network-based barrier certificates using collaborative learning. In: Proceedings of the 59th ACM\/IEEE Design Automation Conference, pp. 1201\u20131206 (2022)","DOI":"10.1145\/3489517.3530608"},{"key":"20_CR59","unstructured":"Xu, K., et\u00a0al.: Automatic perturbation analysis for scalable certified robustness and beyond. In: NeurIPS (2020)"},{"key":"20_CR60","unstructured":"Xue, B.: A new framework for bounding reachability probabilities of continuous-time stochastic systems. CoRR abs\/ arxiv: 2312.15843 (2023)"},{"issue":"4","key":"20_CR61","doi-asserted-by":"publisher","first-page":"1468","DOI":"10.1109\/TAC.2019.2923049","volume":"65","author":"B Xue","year":"2020","unstructured":"Xue, B., Fr\u00e4nzle, M., Zhan, N.: Inner-approximating reachable sets for polynomial systems with time-varying uncertainties. IEEE Trans. Autom. Control 65(4), 1468\u20131483 (2020)","journal-title":"IEEE Trans. Autom. Control"},{"key":"20_CR62","doi-asserted-by":"crossref","unstructured":"Xue, B., Li, R., Zhan, N., Fr\u00e4nzle, M.: Reach-avoid analysis for stochastic discrete-time systems. In: ACC, pp. 4879\u20134885 (2021)","DOI":"10.23919\/ACC50511.2021.9483095"},{"key":"20_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"},{"key":"20_CR64","doi-asserted-by":"crossref","unstructured":"Yang, Z., et al.: An iterative scheme of safe reinforcement learning for nonlinear systems via barrier certificate generation. In: CAV, pp. 467\u2013490 (2021)","DOI":"10.1007\/978-3-030-81685-8_22"},{"key":"20_CR65","doi-asserted-by":"crossref","unstructured":"Zeng, X., Yang, Z., Zhang, L., Tang, X., Zeng, Z., Liu, Z.: Safety verification of nonlinear systems with bayesian neural network controllers. In: AAAI, pp. 15278\u201315286 (2023)","DOI":"10.1609\/aaai.v37i12.26782"},{"issue":"1","key":"20_CR66","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/s12083-022-01434-0","volume":"16","author":"H Zhang","year":"2023","unstructured":"Zhang, H., Gu, J., Zhang, Z., Du, L., et al.: Backdoor attacks against deep reinforcement learning based traffic signal control systems. Peer Peer Netw. Appl. 16(1), 466\u2013474 (2023)","journal-title":"Peer Peer Netw. Appl."},{"key":"20_CR67","unstructured":"Zhang, H., Chen, H., Boning, D.S., Hsieh, C.: Robust reinforcement learning on state observations with learned optimal adversary. In: ICLR (2021)"},{"key":"20_CR68","unstructured":"Zhang, H., et al.: Robust deep reinforcement learning against adversarial perturbations on state observations. In: NeurIPS, pp. 21024\u201321037 (2020)"},{"key":"20_CR69","doi-asserted-by":"crossref","unstructured":"Zhao, H., Qi, N., Dehbi, L., Zeng, X., Yang, Z.: Formal synthesis of neural barrier certificates for continuous systems via counterexample guided learning. ACM Trans. Embed. Comput. Syst. 22(5s), 146:1\u2013146:21 (2023)","DOI":"10.1145\/3609125"},{"key":"20_CR70","doi-asserted-by":"crossref","unstructured":"Zhao, H., Zeng, X., Chen, T., Liu, Z.: Synthesizing barrier certificates using neural networks. In: HSCC, pp. 1\u201311 (2020)","DOI":"10.1145\/3365365.3382222"},{"key":"20_CR71","doi-asserted-by":"crossref","unstructured":"Zhi, D., Wang, P., Liu, S., Ong, L., Zhang, M.: Unifying qualitative and quantitative safety verification of dnn-controlled systems. CoRR abs\/ arXiv: 2404.01769 (2024)","DOI":"10.1007\/978-3-031-65630-9_20"},{"key":"20_CR72","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 (2023)","DOI":"10.1609\/aaai.v37i10.26407"}],"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-65630-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,24]],"date-time":"2024-11-24T19:47:06Z","timestamp":1732477626000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65630-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656293","9783031656309"],"references-count":72,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65630-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"25 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"}}]}}