{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:13:52Z","timestamp":1755998032394,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,5,9]],"date-time":"2023-05-09T00:00:00Z","timestamp":1683590400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100016680","name":"Toyota Research Institute, North America","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100016680","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["SHF-2048094","CNS-1932620"],"award-info":[{"award-number":["SHF-2048094","CNS-1932620"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,5,9]]},"DOI":"10.1145\/3576841.3585928","type":"proceedings-article","created":{"date-parts":[[2023,5,4]],"date-time":"2023-05-04T16:18:19Z","timestamp":1683217099000},"page":"98-109","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["A Neurosymbolic Approach to the Verification of Temporal Logic Properties of Learning-enabled Control Systems"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6147-3675","authenticated-orcid":false,"given":"Navid","family":"Hashemi","sequence":"first","affiliation":[{"name":"University of Southern California, Los Angeles, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6255-7566","authenticated-orcid":false,"given":"Bardh","family":"Hoxha","sequence":"additional","affiliation":[{"name":"Toyota Research Institute of North America, Ann Arbor, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0996-5725","authenticated-orcid":false,"given":"Tomoya","family":"Yamaguchi","sequence":"additional","affiliation":[{"name":"Toyota Research Institute of North America, Ann Arbor, United States of America"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6208-4233","authenticated-orcid":false,"given":"Danil","family":"Prokhorov","sequence":"additional","affiliation":[{"name":"Toyota Research Institute of North America, Ann Arbor, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0456-2129","authenticated-orcid":false,"given":"Georgios","family":"Fainekos","sequence":"additional","affiliation":[{"name":"Toyota Research Institute of North America, Ann Arbor, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4683-5540","authenticated-orcid":false,"given":"Jyotirmoy","family":"Deshmukh","sequence":"additional","affiliation":[{"name":"University of Southern California, Los Angeles, United States of America"}]}],"member":"320","published-online":{"date-parts":[[2023,5,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_21"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3216-0_8"},{"volume-title":"Numerical solution of ordinary differential equations","author":"Atkinson Kendall","key":"e_1_3_2_1_3_1","unstructured":"Kendall Atkinson , Weimin Han , and David E Stewart . 2011. Numerical solution of ordinary differential equations . John Wiley & Sons . Kendall Atkinson, Weimin Han, and David E Stewart. 2011. Numerical solution of ordinary differential equations. John Wiley & Sons."},{"key":"e_1_3_2_1_4_1","volume-title":"Analytical bounds on the local lipschitz constants of affine-relu functions. arXiv preprint arXiv:2008.06141","author":"Avant Trevor","year":"2020","unstructured":"Trevor Avant and Kristi A Morgansen . 2020. Analytical bounds on the local lipschitz constants of affine-relu functions. arXiv preprint arXiv:2008.06141 ( 2020 ). Trevor Avant and Kristi A Morgansen. 2020. Analytical bounds on the local lipschitz constants of affine-relu functions. arXiv preprint arXiv:2008.06141 (2020)."},{"key":"e_1_3_2_1_5_1","volume-title":"Deep reinforcement learning in a handful of trials using probabilistic dynamics models. Advances in neural information processing systems 31","author":"Chua Kurtland","year":"2018","unstructured":"Kurtland Chua , Roberto Calandra , Rowan McAllister , and Sergey Levine . 2018. Deep reinforcement learning in a handful of trials using probabilistic dynamics models. Advances in neural information processing systems 31 ( 2018 ). Kurtland Chua, Roberto Calandra, Rowan McAllister, and Sergey Levine. 2018. Deep reinforcement learning in a handful of trials using probabilistic dynamics models. Advances in neural information processing systems 31 (2018)."},{"key":"e_1_3_2_1_6_1","volume-title":"Gaussian processes for data-efficient learning in robotics and control","author":"Deisenroth Marc Peter","year":"2013","unstructured":"Marc Peter Deisenroth , Dieter Fox , and Carl Edward Rasmussen . 2013. Gaussian processes for data-efficient learning in robotics and control . IEEE transactions on pattern analysis and machine intelligence 37, 2 ( 2013 ), 408--423. Marc Peter Deisenroth, Dieter Fox, and Carl Edward Rasmussen. 2013. Gaussian processes for data-efficient learning in robotics and control. IEEE transactions on pattern analysis and machine intelligence 37, 2 (2013), 408--423."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/1885174.1885183"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302504.3311807"},{"key":"e_1_3_2_1_9_1","volume-title":"Output range analysis for deep neural networks. arXiv preprint arXiv:1709.09130","author":"Dutta Souradeep","year":"2017","unstructured":"Souradeep Dutta , Susmit Jha , Sriram Sanakaranarayanan , and Ashish Tiwari . 2017. Output range analysis for deep neural networks. arXiv preprint arXiv:1709.09130 ( 2017 ). Souradeep Dutta, Susmit Jha, Sriram Sanakaranarayanan, and Ashish Tiwari. 2017. Output range analysis for deep neural networks. arXiv preprint arXiv:1709.09130 (2017)."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_19"},{"volume-title":"Formal approaches to software testing and runtime verification","author":"Fainekos Georgios E","key":"e_1_3_2_1_11_1","unstructured":"Georgios E Fainekos and George J Pappas . 2006. Robustness of temporal logic specifications . In Formal approaches to software testing and runtime verification . Springer , 178--192. Georgios E Fainekos and George J Pappas. 2006. Robustness of temporal logic specifications. In Formal approaches to software testing and runtime verification. Springer, 178--192."},{"key":"e_1_3_2_1_12_1","volume-title":"Efficient and accurate estimation of lipschitz constants for deep neural networks. Advances in Neural Information Processing Systems 32","author":"Fazlyab Mahyar","year":"2019","unstructured":"Mahyar Fazlyab , Alexander Robey , Hamed Hassani , Manfred Morari , and George Pappas . 2019. Efficient and accurate estimation of lipschitz constants for deep neural networks. Advances in Neural Information Processing Systems 32 ( 2019 ). Mahyar Fazlyab, Alexander Robey, Hamed Hassani, Manfred Morari, and George Pappas. 2019. Efficient and accurate estimation of lipschitz constants for deep neural networks. Advances in Neural Information Processing Systems 32 (2019)."},{"volume-title":"Deep learning","author":"Goodfellow Ian","key":"e_1_3_2_1_13_1","unstructured":"Ian Goodfellow , Yoshua Bengio , and Aaron Courville . 2016. Deep learning . MIT press . Ian Goodfellow, Yoshua Bengio, and Aaron Courville. 2016. Deep learning. MIT press."},{"key":"e_1_3_2_1_14_1","unstructured":"Navid Hashemi Justin Ruths and Mahyar Fazlyab. 2021. Certifying incremental quadratic constraints for neural networks via convex optimization. In Learning for Dynamics and Control. PMLR 842--853.  Navid Hashemi Justin Ruths and Mahyar Fazlyab. 2021. Certifying incremental quadratic constraints for neural networks via convex optimization. In Learning for Dynamics and Control. PMLR 842--853."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11164-3_15"},{"key":"e_1_3_2_1_16_1","volume-title":"POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems. arXiv preprint arXiv:2106.13867","author":"Huang Chao","year":"2021","unstructured":"Chao Huang , Jiameng Fan , Xin Chen , Wenchao Li , and Qi Zhu . 2021 . POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems. arXiv preprint arXiv:2106.13867 (2021). Chao Huang, Jiameng Fan, Xin Chen, Wenchao Li, and Qi Zhu. 2021. POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems. arXiv preprint arXiv:2106.13867 (2021)."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3358228"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302504.3311806"},{"key":"e_1_3_2_1_20_1","first-page":"7344","article-title":"Exactly computing the local lipschitz constant of relu networks","volume":"33","author":"Jordan Matt","year":"2020","unstructured":"Matt Jordan and Alexandros G Dimakis . 2020 . Exactly computing the local lipschitz constant of relu networks . Advances in Neural Information Processing Systems 33 (2020), 7344 -- 7353 . Matt Jordan and Alexandros G Dimakis. 2020. Exactly computing the local lipschitz constant of relu networks. Advances in Neural Information Processing Systems 33 (2020), 7344--7353.","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"e_1_3_2_1_23_1","volume-title":"Formal verification of cnn-based perception systems. arXiv preprint arXiv:1811.11373","author":"Kouvaros Panagiotis","year":"2018","unstructured":"Panagiotis Kouvaros and Alessio Lomuscio . 2018. Formal verification of cnn-based perception systems. arXiv preprint arXiv:1811.11373 ( 2018 ). Panagiotis Kouvaros and Alessio Lomuscio. 2018. Formal verification of cnn-based perception systems. arXiv preprint arXiv:1811.11373 (2018)."},{"key":"e_1_3_2_1_24_1","volume-title":"Lipschitz constant estimation of neural networks via sparse polynomial optimization. arXiv preprint arXiv:2004.08688","author":"Latorre Fabian","year":"2020","unstructured":"Fabian Latorre , Paul Rolland , and Volkan Cevher . 2020. Lipschitz constant estimation of neural networks via sparse polynomial optimization. arXiv preprint arXiv:2004.08688 ( 2020 ). Fabian Latorre, Paul Rolland, and Volkan Cevher. 2020. Lipschitz constant estimation of neural networks via sparse polynomial optimization. arXiv preprint arXiv:2004.08688 (2020)."},{"volume-title":"International static analysis symposium","author":"Li Jianlin","key":"e_1_3_2_1_25_1","unstructured":"Jianlin Li , Jiangchao Liu , Pengfei Yang , Liqian Chen , Xiaowei Huang , and Lijun Zhang . 2019. Analyzing deep neural networks with symbolic propagation: Towards higher precision and faster verification . In International static analysis symposium . Springer , 296--319. Jianlin Li, Jiangchao Liu, Pengfei Yang, Liqian Chen, Xiaowei Huang, and Lijun Zhang. 2019. Analyzing deep neural networks with symbolic propagation: Towards higher precision and faster verification. In International static analysis symposium. Springer, 296--319."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Changliu Liu Tomer Arnon Christopher Lazarus Christopher Strong Clark Barrett Mykel J Kochenderfer etal 2021. Algorithms for verifying deep neural networks. Foundations and Trends\u00ae in Optimization 4 3--4 (2021) 244--404.  Changliu Liu Tomer Arnon Christopher Lazarus Christopher Strong Clark Barrett Mykel J Kochenderfer et al. 2021. Algorithms for verifying deep neural networks. Foundations and Trends\u00ae in Optimization 4 3--4 (2021) 244--404.","DOI":"10.1561\/2400000035"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/CACSD.2004.1393890"},{"key":"e_1_3_2_1_28_1","volume-title":"An approach to reachability analysis for feed-forward relu neural networks. arXiv preprint arXiv:1706.07351","author":"Lomuscio Alessio","year":"2017","unstructured":"Alessio Lomuscio and Lalit Maganti . 2017. An approach to reachability analysis for feed-forward relu neural networks. arXiv preprint arXiv:1706.07351 ( 2017 ). Alessio Lomuscio and Lalit Maganti. 2017. An approach to reachability analysis for feed-forward relu neural networks. arXiv preprint arXiv:1706.07351 (2017)."},{"volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"Maler Oded","key":"e_1_3_2_1_29_1","unstructured":"Oded Maler and Dejan Nickovic . 2004. Monitoring temporal properties of continuous signals . In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems . Springer , 152--166. Oded Maler and Dejan Nickovic. 2004. Monitoring temporal properties of continuous signals. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. Springer, 152--166."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_24"},{"key":"e_1_3_2_1_31_1","volume-title":"Semidefinite relaxations for certifying robustness to adversarial examples. Advances in Neural Information Processing Systems 31","author":"Raghunathan Aditi","year":"2018","unstructured":"Aditi Raghunathan , Jacob Steinhardt , and Percy S Liang . 2018. Semidefinite relaxations for certifying robustness to adversarial examples. Advances in Neural Information Processing Systems 31 ( 2018 ). Aditi Raghunathan, Jacob Steinhardt, and Percy S Liang. 2018. Semidefinite relaxations for certifying robustness to adversarial examples. Advances in Neural Information Processing Systems 31 (2018)."},{"volume-title":"Summer school on machine learning","author":"Rasmussen Carl Edward","key":"e_1_3_2_1_32_1","unstructured":"Carl Edward Rasmussen . 2003. Gaussian processes in machine learning . In Summer school on machine learning . Springer , 63--71. Carl Edward Rasmussen. 2003. Gaussian processes in machine learning. In Summer school on machine learning. Springer, 63--71."},{"key":"e_1_3_2_1_33_1","volume-title":"Combined left and right temporal robustness for control under stl specifications","author":"Rodionova Al\u00ebna","year":"2022","unstructured":"Al\u00ebna Rodionova , Lars Lindemann , Manfred Morari , and George J Pappas . 2022. Combined left and right temporal robustness for control under stl specifications . IEEE Control Systems Letters ( 2022 ). Al\u00ebna Rodionova, Lars Lindemann, Manfred Morari, and George J Pappas. 2022. Combined left and right temporal robustness for control under stl specifications. IEEE Control Systems Letters (2022)."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302504.3311802"},{"key":"e_1_3_2_1_35_1","volume-title":"Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199","author":"Szegedy Christian","year":"2013","unstructured":"Christian Szegedy , Wojciech Zaremba , Ilya Sutskever , Joan Bruna , Dumitru Erhan , Ian Goodfellow , and Rob Fergus . 2013. Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199 ( 2013 ). Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow, and Rob Fergus. 2013. Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199 (2013)."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_39"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_1"},{"key":"e_1_3_2_1_38_1","volume-title":"Efficient formal safety analysis of neural networks. Advances in Neural Information Processing Systems 31","author":"Wang Shiqi","year":"2018","unstructured":"Shiqi Wang , Kexin Pei , Justin Whitehouse , Junfeng Yang , and Suman Jana . 2018. Efficient formal safety analysis of neural networks. Advances in Neural Information Processing Systems 31 ( 2018 ). Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. 2018. Efficient formal safety analysis of neural networks. Advances in Neural Information Processing Systems 31 (2018)."},{"key":"e_1_3_2_1_39_1","volume-title":"Efficient neural network robustness certification with general activation functions. Advances in neural information processing systems 31","author":"Zhang Huan","year":"2018","unstructured":"Huan Zhang , Tsui-Wei Weng , Pin-Yu Chen , Cho-Jui Hsieh , and Luca Daniel . 2018. Efficient neural network robustness certification with general activation functions. Advances in neural information processing systems 31 ( 2018 ). Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. 2018. Efficient neural network robustness certification with general activation functions. Advances in neural information processing systems 31 (2018)."}],"event":{"name":"ICCPS '23: ACM\/IEEE 14th International Conference on Cyber-Physical Systems (with CPS-IoT Week 2023)","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems","IEEE TCRTS"],"location":"San Antonio TX USA","acronym":"ICCPS '23"},"container-title":["Proceedings of the ACM\/IEEE 14th International Conference on Cyber-Physical Systems (with CPS-IoT Week 2023)"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3576841.3585928","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:27Z","timestamp":1750178847000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3576841.3585928"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5,9]]},"references-count":39,"alternative-id":["10.1145\/3576841.3585928","10.1145\/3576841"],"URL":"https:\/\/doi.org\/10.1145\/3576841.3585928","relation":{},"subject":[],"published":{"date-parts":[[2023,5,9]]},"assertion":[{"value":"2023-05-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}