{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:49:18Z","timestamp":1767833358417,"version":"3.49.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","license":[{"start":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T00:00:00Z","timestamp":1570492800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["SHF 1736323, CNS 1739328"],"award-info":[{"award-number":["SHF 1736323, CNS 1739328"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-18-C-0089"],"award-info":[{"award-number":["FA8750-18-C-0089"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"crossref","award":["FA9550-18-1-0122"],"award-info":[{"award-number":["FA9550-18-1-0122"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2019,10,31]]},"abstract":"<jats:p>This paper proposes a new forward reachability analysis approach to verify safety of cyber-physical systems (CPS) with reinforcement learning controllers. The foundation of our approach lies on two efficient, exact and over-approximate reachability algorithms for neural network control systems using star sets, which is an efficient representation of polyhedra. Using these algorithms, we determine the initial conditions for which a safety-critical system with a neural network controller is safe by incrementally searching a critical initial condition where the safety of the system cannot be established. Our approach produces tight over-approximation error and it is computationally efficient, which allows the application to practical CPS with learning enable components (LECs). We implement our approach in NNV, a recent verification tool for neural networks and neural network control systems, and evaluate its advantages and applicability by verifying safety of a practical Advanced Emergency Braking System (AEBS) with a reinforcement learning (RL) controller trained using the deep deterministic policy gradient (DDPG) method. The experimental results show that our new reachability algorithms are much less conservative than existing polyhedra-based approaches. We successfully determine the entire region of the initial conditions of the AEBS with the RL controller such that the safety of the system is guaranteed, while a polyhedra-based approach cannot prove the safety properties of the system.<\/jats:p>","DOI":"10.1145\/3358230","type":"journal-article","created":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T13:13:05Z","timestamp":1570713185000},"page":"1-22","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":94,"title":["Safety Verification of Cyber-Physical Systems with Reinforcement Learning Control"],"prefix":"10.1145","volume":"18","author":[{"given":"Hoang-Dung","family":"Tran","sequence":"first","affiliation":[{"name":"Vanderbilt University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Feiyang","family":"Cai","sequence":"additional","affiliation":[{"name":"Vanderbilt University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manzanas Lopez","family":"Diego","sequence":"additional","affiliation":[{"name":"Vanderbilt University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrick","family":"Musau","sequence":"additional","affiliation":[{"name":"Vanderbilt University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8021-9923","authenticated-orcid":false,"given":"Taylor T.","family":"Johnson","sequence":"additional","affiliation":[{"name":"Vanderbilt University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xenofon","family":"Koutsoukos","sequence":"additional","affiliation":[{"name":"Vanderbilt University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,10,8]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"53rd IEEE Conference on Decision and Control. IEEE, 1424--1431","author":"Akametalu Anayo K.","unstructured":"Anayo K. Akametalu , Jaime F. Fisac , Jeremy H. Gillula , Shahab Kaynama , Melanie N. Zeilinger , and Claire J. Tomlin . 2014. Reachability-based safe learning with Gaussian processes . In 53rd IEEE Conference on Decision and Control. IEEE, 1424--1431 . Anayo K. Akametalu, Jaime F. Fisac, Jeremy H. Gillula, Shahab Kaynama, Melanie N. Zeilinger, and Claire J. Tomlin. 2014. Reachability-based safe learning with Gaussian processes. In 53rd IEEE Conference on Decision and Control. IEEE, 1424--1431."},{"key":"e_1_2_1_2_1","volume-title":"Proc. of the Workshop on Applied Verification for Continuous and Hybrid Systems.","author":"Althoff Matthias","year":"2015","unstructured":"Matthias Althoff . 2015 . An introduction to CORA 2015 . In Proc. of the Workshop on Applied Verification for Continuous and Hybrid Systems. Matthias Althoff. 2015. An introduction to CORA 2015. In Proc. of the Workshop on Applied Verification for Continuous and Hybrid Systems."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2008.4738704"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_20"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. ACM, 23--32","author":"Bak Stanley","unstructured":"Stanley Bak , Hoang-Dung Tran , and Taylor T. Johnson . 2019. Numerical verification of affine systems with up to a billion dimensions . In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. ACM, 23--32 . Stanley Bak, Hoang-Dung Tran, and Taylor T. Johnson. 2019. Numerical verification of affine systems with up to a billion dimensions. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. ACM, 23--32."},{"key":"e_1_2_1_6_1","volume-title":"2006 World Automation Congress. IEEE, 1--6.","author":"Valentina","unstructured":"Valentina E. Balas and Marius M. Balas. 2006. Driver assisting by inverse time to collision . In 2006 World Automation Congress. IEEE, 1--6. Valentina E. Balas and Marius M. Balas. 2006. Driver assisting by inverse time to collision. In 2006 World Automation Congress. IEEE, 1--6."},{"key":"e_1_2_1_7_1","volume-title":"Davide Del Testa","author":"Bojarski Mariusz","year":"2016","unstructured":"Mariusz Bojarski , Davide Del Testa , Daniel Dworakowski, Bernhard Firner , Beat Flepp, Prasoon Goyal, Lawrence D. Jackel, Mathew Monfort, Urs Muller, Jiakai Zhang, et al. 2016 . End to end learning for self-driving cars. arXiv preprint arXiv:1604.07316 (2016). Mariusz Bojarski, Davide Del Testa, Daniel Dworakowski, Bernhard Firner, Beat Flepp, Prasoon Goyal, Lawrence D. Jackel, Mathew Monfort, Urs Muller, Jiakai Zhang, et al. 2016. End to end learning for self-driving cars. arXiv preprint arXiv:1604.07316 (2016)."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_18"},{"key":"e_1_2_1_9_1","volume-title":"CARLA: An open urban driving simulator. arXiv preprint arXiv:1711.03938","author":"Dosovitskiy Alexey","year":"2017","unstructured":"Alexey Dosovitskiy , German Ros , Felipe Codevilla , Antonio Lopez , and Vladlen Koltun . 2017 . CARLA: An open urban driving simulator. arXiv preprint arXiv:1711.03938 (2017). Alexey Dosovitskiy, German Ros, Felipe Codevilla, Antonio Lopez, and Vladlen Koltun. 2017. CARLA: An open urban driving simulator. arXiv preprint arXiv:1711.03938 (2017)."},{"key":"e_1_2_1_10_1","volume-title":"Seshia","author":"Dreossi Tommaso","year":"2017","unstructured":"Tommaso Dreossi , Alexandre Donz\u00e9 , and Sanjit A . Seshia . 2017 . Compositional falsification of cyber-physical systems with machine learning components. In NASA Formal Methods Symposium. Springer , 357--372. Tommaso Dreossi, Alexandre Donz\u00e9, and Sanjit A. Seshia. 2017. Compositional falsification of cyber-physical systems with machine learning components. In NASA Formal Methods Symposium. Springer, 357--372."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ifacol.2018.08.026"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/2789272.2886795"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the 2013 International Conference on Autonomous Agents and Multi-Agent Systems. International Foundation for Autonomous Agents and Multiagent Systems, 1037--1044","author":"Gehring Clement","year":"2013","unstructured":"Clement Gehring and Doina Precup . 2013 . Smart exploration in reinforcement learning using absolute temporal difference errors . In Proceedings of the 2013 International Conference on Autonomous Agents and Multi-Agent Systems. International Foundation for Autonomous Agents and Multiagent Systems, 1037--1044 . Clement Gehring and Doina Precup. 2013. Smart exploration in reinforcement learning using absolute temporal difference errors. In Proceedings of the 2013 International Conference on Autonomous Agents and Multi-Agent Systems. International Foundation for Autonomous Agents and Multiagent Systems, 1037--1044."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622519.1622522"},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the 2011 American Control Conference. IEEE, 3393--3398","author":"Geramifard Alborz","unstructured":"Alborz Geramifard , Joshua Redding , Nicholas Roy , and Jonathan P. How . 2011. UAV cooperative control with stochastic risk models . In Proceedings of the 2011 American Control Conference. IEEE, 3393--3398 . Alborz Geramifard, Joshua Redding, Nicholas Roy, and Jonathan P. How. 2011. UAV cooperative control with stochastic risk models. In Proceedings of the 2011 American Control Conference. IEEE, 3393--3398."},{"key":"e_1_2_1_16_1","volume-title":"Hybrid Systems: Computation and Control","author":"Girard Antoine","unstructured":"Antoine Girard . 2005. Reachability of uncertain linear systems using zonotopes . In Hybrid Systems: Computation and Control . Springer , 291--305. Antoine Girard. 2005. Reachability of uncertain linear systems using zonotopes. In Hybrid Systems: Computation and Control. Springer, 291--305."},{"key":"e_1_2_1_17_1","volume-title":"Anton Maximilian Sch\u00e4fer, and Steffen Udluft","author":"Hans Alexander","year":"2008","unstructured":"Alexander Hans , Daniel Schneega\u00df , Anton Maximilian Sch\u00e4fer, and Steffen Udluft . 2008 . Safe exploration for reinforcement learning. In ESANN. 143--148. Alexander Hans, Daniel Schneega\u00df, Anton Maximilian Sch\u00e4fer, and Steffen Udluft. 2008. Safe exploration for reinforcement learning. In ESANN. 143--148."},{"key":"e_1_2_1_18_1","volume-title":"Palmer","author":"Hertz John","year":"1991","unstructured":"John Hertz , Anders Krogh , and Richard G . Palmer . 1991 . Introduction to the Theory of Neural Computation. Addison-Wesley\/Addison Wesley Longman . John Hertz, Anders Krogh, and Richard G. Palmer. 1991. Introduction to the Theory of Neural Computation. Addison-Wesley\/Addison Wesley Longman."},{"key":"e_1_2_1_19_1","volume-title":"Verisig: Verifying safety properties of hybrid systems with neural network controllers. In Hybrid Systems: Computation and Control (HSCC).","author":"Ivanov Radoslav","year":"2019","unstructured":"Radoslav Ivanov , James Weimer , Rajeev Alur , George J. Pappas , and Insup Lee . 2019 . Verisig: Verifying safety properties of hybrid systems with neural network controllers. In Hybrid Systems: Computation and Control (HSCC). Radoslav Ivanov, James Weimer, Rajeev Alur, George J. Pappas, and Insup Lee. 2019. Verisig: Verifying safety properties of hybrid systems with neural network controllers. In Hybrid Systems: Computation and Control (HSCC)."},{"key":"e_1_2_1_20_1","volume-title":"Owen","author":"Julian Kyle D.","year":"2018","unstructured":"Kyle D. Julian , Mykel J. Kochenderfer , and Michael P . Owen . 2018 . Deep neural network compression for aircraft collision avoidance systems. arXiv preprint arXiv:1810.04240 (2018). Kyle D. Julian, Mykel J. Kochenderfer, and Michael P. Owen. 2018. Deep neural network compression for aircraft collision avoidance systems. arXiv preprint arXiv:1810.04240 (2018)."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2018.8619572"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.4271\/2011-01-0576"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1068\/p050437"},{"key":"e_1_2_1_24_1","volume-title":"Continuous control with deep reinforcement learning. arXiv preprint arXiv:1509.02971","author":"Lillicrap Timothy P.","year":"2015","unstructured":"Timothy P. Lillicrap , Jonathan J. Hunt , Alexander Pritzel , Nicolas Heess , Tom Erez , Yuval Tassa , David Silver , and Daan Wierstra . 2015. Continuous control with deep reinforcement learning. arXiv preprint arXiv:1509.02971 ( 2015 ). Timothy P. Lillicrap, Jonathan J. Hunt, Alexander Pritzel, Nicolas Heess, Tom Erez, Yuval Tassa, David Silver, and Daan Wierstra. 2015. Continuous control with deep reinforcement learning. arXiv preprint arXiv:1509.02971 (2015)."},{"key":"e_1_2_1_25_1","volume-title":"Safe exploration in Markov decision processes. arXiv preprint arXiv:1205.4810","author":"Moldovan Teodor Mihai","year":"2012","unstructured":"Teodor Mihai Moldovan and Pieter Abbeel . 2012. Safe exploration in Markov decision processes. arXiv preprint arXiv:1205.4810 ( 2012 ). Teodor Mihai Moldovan and Pieter Abbeel. 2012. Safe exploration in Markov decision processes. arXiv preprint arXiv:1205.4810 (2012)."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2016.282"},{"key":"e_1_2_1_27_1","unstructured":"Sriram Sankaranarayanan Souradeep Dutta and Xin Chen. 2019. Reachability analysis for neural feedback systems using regressive polynomial rule inference. In Hybrid Systems: Computation and Control (HSCC).  Sriram Sankaranarayanan Souradeep Dutta and Xin Chen. 2019. Reachability analysis for neural feedback systems using regressive polynomial rule inference. In Hybrid Systems: Computation and Control (HSCC)."},{"key":"e_1_2_1_28_1","unstructured":"Xiaowu Sun Haitham Khedr and Yasser Shoukry. 2019. Formal verification of neural network controlled autonomous systems. In Hybrid Systems: Computation and Control (HSCC).  Xiaowu Sun Haitham Khedr and Yasser Shoukry. 2019. Formal verification of neural network controlled autonomous systems. In Hybrid Systems: Computation and Control (HSCC)."},{"key":"e_1_2_1_29_1","volume-title":"7th International Conference on Formal Methods in Software Engineering (FormaliSE2019)","author":"Tran Hoang-Dung","unstructured":"Hoang-Dung Tran , Patrick Musau , Diego Manzanas Lopez , Xiaodong Yang , Luan Viet Nguyen , Weiming Xiang , and Taylor T. Johnson . 2019. Parallelizable reachability analysis algorithms for feed-forward neural networks . In 7th International Conference on Formal Methods in Software Engineering (FormaliSE2019) , Montreal, Canada. Hoang-Dung Tran, Patrick Musau, Diego Manzanas Lopez, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang, and Taylor T. Johnson. 2019. Parallelizable reachability analysis algorithms for feed-forward neural networks. In 7th International Conference on Formal Methods in Software Engineering (FormaliSE2019), Montreal, Canada."},{"key":"e_1_2_1_30_1","volume-title":"Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang, and Taylor T. Johnson.","author":"Tran Hoang-Dung","year":"2019","unstructured":"Hoang-Dung Tran , Patrick Musau , Diego Manzanas Lopez , Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang, and Taylor T. Johnson. 2019 . Star-based reachability analsysis for deep neural networks. In 23rd International Symposisum on Formal Methods (FM\u201919). Springer International Publishing . Hoang-Dung Tran, Patrick Musau, Diego Manzanas Lopez, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang, and Taylor T. Johnson. 2019. Star-based reachability analsysis for deep neural networks. In 23rd International Symposisum on Formal Methods (FM\u201919). Springer International Publishing."},{"key":"e_1_2_1_31_1","volume-title":"17th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS\u201919)","author":"Tran Hoang-Dung","unstructured":"Hoang-Dung Tran , Luan Viet Nguyen , Nathaniel Hamilton , Weiming Xiang , and Taylor T. Johnson . 2019. Reachability analysis for high-index linear differential algebraic equations (DAEs) . In 17th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS\u201919) . Springer International Publishing. Hoang-Dung Tran, Luan Viet Nguyen, Nathaniel Hamilton, Weiming Xiang, and Taylor T. Johnson. 2019. Reachability analysis for high-index linear differential algebraic equations (DAEs). In 17th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS\u201919). Springer International Publishing."},{"key":"e_1_2_1_32_1","volume-title":"Patrick Musau, Weiming Xiang, and Taylor T. Johnson.","author":"Tran Hoang-Dung","year":"2019","unstructured":"Hoang-Dung Tran , Luan Viet Nguyen , Patrick Musau, Weiming Xiang, and Taylor T. Johnson. 2019 . Decentralized real-time safety verification for distributed cyber-physical systems. In Formal Techniques for Distributed Objects, Components, and Systems (FORTE\u201919), Jorge A. P\u00e9rez and Nobuko Yoshida (Eds.). Springer International Publishing , Cham, 261--277. Hoang-Dung Tran, Luan Viet Nguyen, Patrick Musau, Weiming Xiang, and Taylor T. Johnson. 2019. Decentralized real-time safety verification for distributed cyber-physical systems. In Formal Techniques for Distributed Objects, Components, and Systems (FORTE\u201919), Jorge A. P\u00e9rez and Nobuko Yoshida (Eds.). Springer International Publishing, Cham, 261--277."},{"key":"e_1_2_1_33_1","volume-title":"Simulation-based adversarial test generation for autonomous vehicles with machine learning components. arXiv preprint arXiv:1804.06760","author":"Tuncali Cumhur Erkan","year":"2018","unstructured":"Cumhur Erkan Tuncali , Georgios Fainekos , Hisahiro Ito , and James Kapinski . 2018. Simulation-based adversarial test generation for autonomous vehicles with machine learning components. arXiv preprint arXiv:1804.06760 ( 2018 ). Cumhur Erkan Tuncali, Georgios Fainekos, Hisahiro Ito, and James Kapinski. 2018. Simulation-based adversarial test generation for autonomous vehicles with machine learning components. arXiv preprint arXiv:1804.06760 (2018)."},{"key":"e_1_2_1_34_1","volume-title":"Patrick Musau, and Taylor T. Johnson.","author":"Xiang Weiming","year":"2019","unstructured":"Weiming Xiang , Diego Manzanas Lopez , Patrick Musau, and Taylor T. Johnson. 2019 . Reachable set estimation and verification for neural network models of nonlinear dynamic systems. In Safe, Autonomous and Intelligent Vehicles. Springer , 123--144. Weiming Xiang, Diego Manzanas Lopez, Patrick Musau, and Taylor T. Johnson. 2019. Reachable set estimation and verification for neural network models of nonlinear dynamic systems. In Safe, Autonomous and Intelligent Vehicles. Springer, 123--144."},{"key":"e_1_2_1_35_1","volume-title":"Johnson","author":"Xiang Weiming","year":"2017","unstructured":"Weiming Xiang , Hoang-Dung Tran , and Taylor T . Johnson . 2017 . Reachable set computation and safety verification for neural networks with ReLU activations. arXiv preprint arXiv:1712.08163 (2017). Weiming Xiang, Hoang-Dung Tran, and Taylor T. Johnson. 2017. Reachable set computation and safety verification for neural networks with ReLU activations. arXiv preprint arXiv:1712.08163 (2017)."},{"key":"e_1_2_1_36_1","volume-title":"Johnson","author":"Xiang Weiming","year":"2018","unstructured":"Weiming Xiang , Hoang-Dung Tran , Joel A. Rosenfeld , and Taylor T . Johnson . 2018 . Reachable set estimation and safety verification for piecewise linear systems with neural network controllers. arXiv preprint arXiv:1802.06981 (2018). Weiming Xiang, Hoang-Dung Tran, Joel A. Rosenfeld, and Taylor T. Johnson. 2018. Reachable set estimation and safety verification for piecewise linear systems with neural network controllers. arXiv preprint arXiv:1802.06981 (2018)."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3358230","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3358230","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3358230","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:23:07Z","timestamp":1750202587000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3358230"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,8]]},"references-count":36,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2019,10,31]]}},"alternative-id":["10.1145\/3358230"],"URL":"https:\/\/doi.org\/10.1145\/3358230","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,8]]},"assertion":[{"value":"2019-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-10-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}