{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T03:46:09Z","timestamp":1777866369672,"version":"3.51.4"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031982071","type":"print"},{"value":"9783031982088","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,7,9]],"date-time":"2025-07-09T00:00:00Z","timestamp":1752019200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,7,9]],"date-time":"2025-07-09T00:00:00Z","timestamp":1752019200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-031-98208-8_1","type":"book-chapter","created":{"date-parts":[[2025,7,13]],"date-time":"2025-07-13T17:57:09Z","timestamp":1752429429000},"page":"3-10","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Safeguarding Neural Network-Controlled Systems via\u00a0Formal Methods: From Safety-by-Design to\u00a0Runtime Assurance (Invited Talk)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1938-2902","authenticated-orcid":false,"given":"Min","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,7,9]]},"reference":[{"issue":"6","key":"1_CR1","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.P., 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":"1_CR2","doi-asserted-by":"crossref","unstructured":"Althoff, M., Stursberg, O., Buss, M.: Reachability analysis of nonlinear systems with uncertain parameters using conservative linearization. In: IEEE Conference on Decision and Control (ICDC 2008), pp. 4042\u20134048. IEEE (2008)","DOI":"10.1109\/CDC.2008.4738704"},{"issue":"6","key":"1_CR3","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1109\/MSP.2017.2743240","volume":"34","author":"K Arulkumaran","year":"2017","unstructured":"Arulkumaran, K., Deisenroth, M.P., Brundage, M., Bharath, A.A.: Deep reinforcement learning: a brief survey. IEEE Signal Process. Mag. 34(6), 26\u201338 (2017)","journal-title":"IEEE Signal Process. Mag."},{"key":"1_CR4","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Chen, C., et al.: Toward a thousand lights: decentralized deep reinforcement learning for large-scale traffic signal control. In: Proceedings of the AAAI Conference on Artificial Intelligence (AAAI 2020), pp. 3414\u20133421 (2020)","DOI":"10.1609\/aaai.v34i04.5744"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Computer Aided Verification: 12th International Conference (CAV 2000), pp. 154\u2013169. Springer (2000)","DOI":"10.1007\/10722167_15"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Abstract interpretation based formal methods and future challenges. In: Informatics: 10 Years Back, 10 Years Ahead, pp. 138\u2013156. Springer (2001)","DOI":"10.1007\/3-540-44577-3_10"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Dawson, C., Gao, S., Fan, C.: Safe control with learned certificates: a survey of neural lyapunov, barrier, and contraction methods. arXiv:2202.11762 (2022)","DOI":"10.1109\/TRO.2022.3232542"},{"key":"1_CR9","unstructured":"Hobbs, J.R.: Granularity. In: International Joint Conference on Artificial Intelligence (IJCAI 1985), pp. 432\u2013435 (1985)"},{"key":"1_CR10","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"},{"issue":"5s","key":"1_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3358228","volume":"18","author":"C Huang","year":"2019","unstructured":"Huang, C., Fan, J., Li, W., Chen, X., Zhu, Q.: Reachnn: reachability analysis of neural-network controlled systems. ACM Trans. Embed. Comput. Syst. (TECS) 18(5s), 1\u201322 (2019)","journal-title":"ACM Trans. Embed. Comput. Syst. (TECS)"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Jin, P., Tian, J., Zhi, D., Wen, X., Zhang, M.: Trainify: a cegar-driven training and verification framework for safe deep reinforcement learning. In: International Conference on Computer Aided Verification (CAV 2022), pp. 193\u2013218. Springer (2022)","DOI":"10.1007\/978-3-031-13185-1_10"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Jin, P., Wang, Y., Zhang, M.: Efficient LTL model checking of deep reinforcement learning systems using policy extraction. In: International Conference on Software Engineering and Knowledge Engineering (SEKE 2022), pp. 357\u2013362 (2022)","DOI":"10.18293\/SEKE2022-029"},{"issue":"8","key":"1_CR14","doi-asserted-by":"publisher","first-page":"4919","DOI":"10.1109\/TITS.2020.2984033","volume":"22","author":"N Kumar","year":"2021","unstructured":"Kumar, N., Rahman, S.S., Dhakad, N.: Fuzzy inference enabled deep reinforcement learning-based traffic light control for intelligent transportation system. IEEE Trans. Intell. Transp. Syst. 22(8), 4919\u20134928 (2021)","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"issue":"14s","key":"1_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3596444","volume":"55","author":"M Landers","year":"2023","unstructured":"Landers, M., Doryab, A.: Deep reinforcement learning verification: a survey. ACM Comput. Surv. 55(14s), 1\u201331 (2023)","journal-title":"ACM Comput. Surv."},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Peruffo, A., Ahmed, D., Abate, A.: Automated and formal synthesis of neural barrier certificates for dynamical models. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021), pp. 370\u2013388. Springer (2021)","DOI":"10.1007\/978-3-030-72016-2_20"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: International Workshop on Hybrid Systems: Computation and Control, pp. 477\u2013492. Springer (2004)","DOI":"10.1007\/978-3-540-24743-2_32"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Tian, J., Zhi, D., Liu, S., Wang, P., Chen, C., Zhang, M.: Boosting verification of deep reinforcement learning via piece-wise linear decision neural networks. In: Advances in Neural Information Processing Systems (NeurIPS 2023), vol. 36, pp. 10022\u201310037 (2023)","DOI":"10.52202\/075280-0438"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Tian, J., Zhi, D., Liu, S., Wang, P., Katz, G., Zhang, M.: Taming reachability analysis of DNN-controlled systems via abstraction-based training. In: International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2023), pp. 73\u201397. Springer (2023)","DOI":"10.1007\/978-3-031-50521-8_4"},{"key":"1_CR20","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: International Joint Conference on Artificial Intelligence (IJCAI 2022), pp. 3954\u20133961 (2022)","DOI":"10.24963\/ijcai.2022\/549"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Wang, L., Theodorou, E.A., Egerstedt, M.: Safe learning of quadrotor dynamics using barrier certificates. In: IEEE International Conference on Robotics and Automation (ICRA 2018), pp. 2460\u20132465 (2018)","DOI":"10.1109\/ICRA.2018.8460471"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Watanabe, K., Kang, E., Lin, C.W., Shiraishi, S.: Runtime monitoring for safety of intelligent vehicles. In: Annual Design Automation Conference (DAC 2018), pp.\u00a01\u20136 (2018)","DOI":"10.1109\/DAC.2018.8465912"},{"key":"1_CR23","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2024.103252","volume":"242","author":"T Woodlief","year":"2025","unstructured":"Woodlief, T., Toledo, F., Elbaum, S.G., Dwyer, M.B.: The SGSM framework: enabling the specification and monitor synthesis of safe driving properties through scene graphs. Sci. Comput. Program. 242, 103252 (2025)","journal-title":"Sci. Comput. Program."},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Yang, J., Zhang, M., Chen, X., Li, Q.: Formal verification of probabilistic deep reinforcement learning policies with abstract training. In: International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2025), pp. 125\u2013147. Springer (2025)","DOI":"10.1007\/978-3-031-82700-6_6"},{"issue":"1","key":"1_CR25","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":"1_CR26","unstructured":"Zhang, H., Chen, H., Boning, D.S., Hsieh, C.: Robust reinforcement learning on state observations with learned optimal adversary. In: International Conference on Learning Representations (ICLR 2021) (2021)"},{"key":"1_CR27","unstructured":"Zhang, H., et al.: Robust deep reinforcement learning against adversarial perturbations on state observations. In: Annual Conference on Neural Information Processing Systems (NeurIPS 2020), pp. 21024\u201321037 (2020)"},{"issue":"5","key":"1_CR28","doi-asserted-by":"publisher","first-page":"6349","DOI":"10.1109\/TII.2022.3195701","volume":"19","author":"W Zhang","year":"2023","unstructured":"Zhang, W., Tu, Z., Liu, W.: Optimal charging control of energy storage systems for pulse power load using deep reinforcement learning in shipboard integrated power systems. IEEE Trans. Ind. Inform. 19(5), 6349\u20136363 (2023)","journal-title":"IEEE Trans. Ind. Inform."},{"key":"1_CR29","unstructured":"Zhi, D., Peixin, W., Zhang, M.: Runtime safeguarding of neural network-controlled systems without backup safety controllers (2025)"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Zhi, D., Wang, P., Chen, C., Zhang, M.: Robustness verification of deep reinforcement learning based control systems using reward martingales. In: Proceedings of the AAAI Conference on Artificial Intelligence (AAAI 2024), vol.\u00a038, pp. 19992\u201320000 (2024)","DOI":"10.1609\/aaai.v38i18.29976"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"Zhi, D., Wang, P., Liu, S., Ong, C.H.L., Zhang, M.: Unifying qualitative and quantitative safety verification of DNN-controlled systems. In: International Conference on Computer Aided Verification (CAV 2024), pp. 401\u2013426. Springer (2024)","DOI":"10.1007\/978-3-031-65630-9_20"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98208-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T08:34:12Z","timestamp":1777538052000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98208-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7,9]]},"ISBN":["9783031982071","9783031982088"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98208-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,7,9]]},"assertion":[{"value":"9 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Theoretical Aspects of Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Limassol","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cyprus","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":"14 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tase2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cyprusconferences.org\/tase2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}