{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,10]],"date-time":"2025-12-10T09:04:47Z","timestamp":1765357487594,"version":"3.41.0"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2024,4,30]],"date-time":"2024-04-30T00:00:00Z","timestamp":1714435200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"The National Science Foundation","award":["SHF-2048094, CNS-1932620, CNS-2039087, FMitF-1837131, CCF-SHF-1932620"],"award-info":[{"award-number":["SHF-2048094, CNS-1932620, CNS-2039087, FMitF-1837131, CCF-SHF-1932620"]}]},{"name":"Airbus Institute for Engineering Research, and funding by Toyota R&D and Siemens Corporate Research through the USC Center for Autonomy and AI"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Cyber-Phys. Syst."],"published-print":{"date-parts":[[2024,4,30]]},"abstract":"<jats:p>\n            Uncertainty in safety-critical cyber-physical systems can be modeled using a finite number of parameters or parameterized input signals. Given a system specification in Signal Temporal Logic (STL), we would like to verify that for all (infinite) values of the model parameters\/input signals, the system satisfies its specification. Unfortunately, this problem is undecidable in general.\n            <jats:italic>Statistical model checking<\/jats:italic>\n            (SMC) offers a solution by providing guarantees on the correctness of CPS models by statistically reasoning on model simulations. We propose a new approach for statistical verification of CPS models for user-provided distribution on the model parameters. Our technique uses model simulations to learn\n            <jats:italic>surrogate models<\/jats:italic>\n            , and uses\n            <jats:italic>conformal inference<\/jats:italic>\n            to provide probabilistic guarantees on the satisfaction of a given STL property. Additionally, we can provide prediction intervals containing the quantitative satisfaction values of the given STL property for any user-specified confidence level. We compare this prediction interval with the interval we get using risk estimation procedures. We also propose a refinement procedure based on Gaussian Process (GP)-based surrogate models for obtaining fine-grained probabilistic guarantees over sub-regions in the parameter space. This in turn enables the CPS designer to choose assured validity domains in the parameter space for safety-critical applications. Finally, we demonstrate the efficacy of our technique on several CPS models.\n          <\/jats:p>","DOI":"10.1145\/3635160","type":"journal-article","created":{"date-parts":[[2023,12,5]],"date-time":"2023-12-05T12:01:49Z","timestamp":1701777709000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Statistical Verification using Surrogate Models and Conformal Inference and a Comparison with Risk-Aware Verification"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7457-0565","authenticated-orcid":false,"given":"Xin","family":"Qin","sequence":"first","affiliation":[{"name":"University of Southern California, Los Angeles, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0649-3101","authenticated-orcid":false,"given":"Yuan","family":"Xia","sequence":"additional","affiliation":[{"name":"University of Southern California, Los Angeles, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1557-4595","authenticated-orcid":false,"given":"Aditya","family":"Zutshi","sequence":"additional","affiliation":[{"name":"Galois, Inc., Portland, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4671-233X","authenticated-orcid":false,"given":"Chuchu","family":"Fan","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4683-5540","authenticated-orcid":false,"given":"Jyotirmoy V.","family":"Deshmukh","sequence":"additional","affiliation":[{"name":"University of Southern California, Los Angeles, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,5,14]]},"reference":[{"key":"e_1_3_3_2_2","first-page":"1","volume-title":"4th Annual IEEE International Conference on Cyber Technology in Automation, Control and Intelligent Systems","author":"Abbas H.","year":"2014","unstructured":"H. Abbas, B. Hoxha, G. Fainekos, and K. Ueda. 2014. Robustness-guided temporal logic testing and verification for stochastic cyber-physical systems. In 4th Annual IEEE International Conference on Cyber Technology in Automation, Control and Intelligent Systems. IEEE, 1\u20136."},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158668"},{"key":"e_1_3_3_4_2","first-page":"356","volume-title":"CAV","author":"Akazaki Takumi","year":"2015","unstructured":"Takumi Akazaki and Ichiro Hasuo. 2015. Time robustness in MTL and expressivity in hybrid system falsification. In CAV. 356\u2013374."},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","unstructured":"Prithvi Akella Mohamadreza Ahmadi and Aaron D. Ames. 2022. A Scenario Approach to Risk-Aware Safety-Critical System Verification. (2022). 10.48550\/ARXIV.2203.02595","DOI":"10.48550\/ARXIV.2203.02595"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/18.256500"},{"key":"e_1_3_3_7_2","first-page":"197","volume-title":"Proc. of HSCC","author":"Bartocci Ezio","year":"2018","unstructured":"Ezio Bartocci, Thomas Ferr\u00e8re, Niveditha Manjunath, and Dejan Ni\u010dkovi\u0107. 2018. Localizing faults in simulink\/stateflow models with STL. In Proc. of HSCC. 197\u2013206."},{"key":"e_1_3_3_8_2","volume-title":"Pattern Recognition and Machine Learning","author":"Bishop Christopher M.","year":"2006","unstructured":"Christopher M. Bishop. 2006. Pattern Recognition and Machine Learning. Springer."},{"key":"e_1_3_3_9_2","article-title":"Assurance monitoring of cyber-physical systems with machine learning components","author":"Boursinos Dimitrios","year":"2020","unstructured":"Dimitrios Boursinos and Xenofon Koutsoukos. 2020. Assurance monitoring of cyber-physical systems with machine learning components. arXiv preprint arXiv:2001.05014 (2020).","journal-title":"arXiv preprint arXiv:2001.05014"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/SPW50608.2020.00053"},{"key":"e_1_3_3_11_2","first-page":"174","volume-title":"2020 ACM\/IEEE 11th International Conference on Cyber-Physical Systems (ICCPS)","author":"Cai Feiyang","year":"2020","unstructured":"Feiyang Cai and Xenofon Koutsoukos. 2020. Real-time out-of-distribution detection in learning-enabled cyber-physical systems. In 2020 ACM\/IEEE 11th International Conference on Cyber-Physical Systems (ICCPS). IEEE, 174\u2013183."},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429085"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.23919\/ACC.2019.8815169"},{"key":"e_1_3_3_14_2","first-page":"231","volume-title":"CMSB","author":"Clarke E. M.","year":"2008","unstructured":"E. M. Clarke, J. R. Faeder, C. J. Langmead, L. A. Harris, S. K. Jha, and A. Legay. 2008. Statistical model checking in biolab: Applications to the automated analysis of t-cell receptor signaling pathway. In CMSB. Springer, 231\u2013250."},{"key":"e_1_3_3_15_2","first-page":"220","volume-title":"ICCPS","author":"Deshmukh Jyotirmoy","year":"2018","unstructured":"Jyotirmoy Deshmukh, Xiaoqing Jin, Rupak Majumdar, and Vinayak Prabhu. 2018. Parameter optimization in control software using statistical fault localization techniques. In ICCPS. IEEE, 220\u2013231."},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/1885174.1885183"},{"key":"e_1_3_3_17_2","first-page":"432","volume-title":"CAV","author":"Dreossi Tommaso","year":"2019","unstructured":"Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Hadi Ravanbakhsh, Marcell Vazquez-Chanlatte, and Sanjit A. Seshia. 2019. VerifAI: A toolkit for the formal design and analysis of artificial intelligence-based systems. In CAV. 432\u2013442."},{"issue":"16","key":"e_1_3_3_18_2","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1016\/j.ifacol.2018.08.026","article-title":"Learning and verification of feedback control systems using feedforward neural networks","volume":"51","author":"Dutta Souradeep","year":"2018","unstructured":"Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, and Ashish Tiwari. 2018. Learning and verification of feedback control systems using feedforward neural networks. IFAC-PapersOnLine 51, 16 (2018), 151\u2013156.","journal-title":"IFAC-PapersOnLine"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.06.021"},{"key":"e_1_3_3_20_2","first-page":"441","volume-title":"CAV","author":"Fan Chuchu","year":"2017","unstructured":"Chuchu Fan, Bolun Qi, Sayan Mitra, and Mahesh Viswanathan. 2017. Dryvr: Data-driven verification and compositional reasoning for automotive systems. In CAV. 441\u2013461."},{"key":"e_1_3_3_21_2","volume-title":"The Elements of Statistical Learning","author":"Friedman Jerome","year":"2001","unstructured":"Jerome Friedman, Trevor Hastie, and Robert Tibshirani. 2001. The Elements of Statistical Learning. Vol. 1. Springer series in statistics, New York."},{"key":"e_1_3_3_22_2","article-title":"Probably approximately correct MDP learning and control with temporal logic constraints","author":"Fu Jie","year":"2014","unstructured":"Jie Fu and Ufuk Topcu. 2014. Probably approximately correct MDP learning and control with temporal logic constraints. arXiv preprint arXiv:1404.7073 (2014).","journal-title":"arXiv preprint arXiv:1404.7073"},{"key":"e_1_3_3_23_2","first-page":"249","volume-title":"10th ACM\/IEEE International Conference on Cyber-Physical Systems","author":"Gu Xiaozhe","year":"2019","unstructured":"Xiaozhe Gu and Arvind Easwaran. 2019. Towards safe machine learning for CPS: Infer uncertainty from training data. In 10th ACM\/IEEE International Conference on Cyber-Physical Systems. 249\u2013258."},{"key":"e_1_3_3_24_2","first-page":"208","volume-title":"ARCH@ ADHS","author":"Heidlauf Peter","year":"2018","unstructured":"Peter Heidlauf, Alexander Collins, Michael Bolender, and Stanley Bak. 2018. Verification challenges in F-16 ground collision avoidance and other automated maneuvers. In ARCH@ ADHS. 208\u2013217."},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/2661631"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"e_1_3_3_27_2","volume-title":"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 HSCC."},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-018-0319-x"},{"key":"e_1_3_3_29_2","first-page":"97","volume-title":"CAV","author":"Katz Guy","year":"2017","unstructured":"Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. 2017. Reluplex: An efficient SMT solver for verifying deep neural networks. In CAV, Rupak Majumdar and Viktor Kun\u010dak (Eds.). 97\u2013117."},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16612-9_11"},{"key":"e_1_3_3_31_2","doi-asserted-by":"crossref","unstructured":"Axel Legay and Mahesh Viswanathan. 2015. Statistical model checking: challenges and perspectives. International Journal on Software Tools for Technology Transfer 17 (2015) 369\u2013376.","DOI":"10.1007\/s10009-015-0384-z"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1080\/01621459.2017.1307116"},{"issue":"1","key":"e_1_3_3_33_2","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1111\/rssb.12021","article-title":"Distribution-free prediction bands for non-parametric regression","volume":"76","author":"Lei Jing","year":"2014","unstructured":"Jing Lei and Larry Wasserman. 2014. Distribution-free prediction bands for non-parametric regression. Journal of the Royal Statistical Society: Series B (Statistical Methodology) 76, 1 (2014), 71\u201396.","journal-title":"Journal of the Royal Statistical Society: Series B (Statistical Methodology)"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","unstructured":"Lars Lindemann Lejun Jiang Nikolai Matni and George J. Pappas. 2022. Risk of stochastic systems for temporal logic specifications. (2022). 10.48550\/ARXIV.2205.14523","DOI":"10.48550\/ARXIV.2205.14523"},{"key":"e_1_3_3_35_2","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/978-3-030-28619-4_10","volume-title":"Robotics Research","author":"Majumdar Anirudha","year":"2020","unstructured":"Anirudha Majumdar and Marco Pavone. 2020. How should a robot assess risk? Towards an axiomatic theory of risk in robotics. In Robotics Research, Nancy M. Amato, Greg Hager, Shawna Thomas, and Miguel Torres-Torriti (Eds.). Springer International Publishing, Cham, 75\u201384."},{"key":"e_1_3_3_36_2","doi-asserted-by":"crossref","unstructured":"Oded Maler and Dejan Nickovic. 2004. Monitoring temporal prop\/hastieerties of continuous signals. International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. Springer 152\u2013166.","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1177\/1932296813514502"},{"key":"e_1_3_3_38_2","unstructured":"Mathworks 2020. Train DQN agent for Lane Keep Assist. https:\/\/www.mathworks.com\/help\/reinforcement-learning\/ug\/train-dqn-agent-for-lane-keeping-assist.html (n.d.)."},{"key":"e_1_3_3_39_2","article-title":"Part-X: A family of stochastic algorithms for search-based test generation with probabilistic guarantees","author":"Pedrielli Giulia","year":"2021","unstructured":"Giulia Pedrielli, Tanmay Khandait, Surdeep Chotaliya, Quinn Thibeault, Hao Huang, Mauricio Castillo-Effen, and Georgios Fainekos. 2021. Part-X: A family of stochastic algorithms for search-based test generation with probabilistic guarantees. arXiv preprint arXiv:2110.10729 (2021).","journal-title":"arXiv preprint arXiv:2110.10729"},{"key":"e_1_3_3_40_2","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1109\/ICCPS54341.2022.00017","volume-title":"2022 ACM\/IEEE 13th International Conference on Cyber-Physical Systems (ICCPS)","author":"Qin Xin","year":"2022","unstructured":"Xin Qin, Yuan Xia, Aditya Zutshi, Chuchu Fan, and Jyotirmoy V. Deshmukh. 2022. Statistical verification of cyber-physical systems using surrogate models and conformal inference. In 2022 ACM\/IEEE 13th International Conference on Cyber-Physical Systems (ICCPS). IEEE, 116\u2013126."},{"key":"e_1_3_3_41_2","first-page":"63","volume-title":"Summer School on Machine Learning","author":"Rasmussen Carl Edward","year":"2003","unstructured":"Carl Edward Rasmussen. 2003. Gaussian processes in machine learning. In Summer School on Machine Learning. Springer, 63\u201371."},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0378-4266(02)00271-6"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.21314\/JOR.2000.038"},{"key":"e_1_3_3_44_2","first-page":"11","article-title":"Temporal logic as filtering","author":"Rodionova Alena","year":"2016","unstructured":"Alena Rodionova, Ezio Bartocci, Dejan Nickovic, and Radu Grosu. 2016. Temporal logic as filtering. In 19th International Conference on Hybrid Systems: Computation and Control (HSCC \u201916). (2016), 11\u201320. arxiv:1510.08079","journal-title":"19th International Conference on Hybrid Systems: Computation and Control (HSCC \u201916)."},{"key":"e_1_3_3_45_2","first-page":"3538","volume-title":"NeurIPS","author":"Romano Yaniv","year":"2019","unstructured":"Yaniv Romano, Evan Patterson, and Emmanuel Candes. 2019. Conformalized quantile regression. In NeurIPS. 3538\u20133548."},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/3049797.3049804"},{"key":"e_1_3_3_47_2","first-page":"9","article-title":"Partitioning for safety and security: Requirements, mechanisms, and assurance","author":"Rushby John","year":"2002","unstructured":"John Rushby. 2002. Partitioning for safety and security: Requirements, mechanisms, and assurance. AFRL-IF-RS-TR\u2019-2002-85 (2002), 9.","journal-title":"AFRL-IF-RS-TR\u2019-2002-85"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_16"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.1002\/9781119174882"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3302504.3311802"},{"key":"e_1_3_3_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_39"},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1109\/CIFER.2000.844598"},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","DOI":"10.5555\/1062391"},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3358232"},{"key":"e_1_3_3_55_2","unstructured":"Jinyu Xie. 2018. Simglucose v0.2.1. https:\/\/github.com\/jxx123\/simglucose. (2018)."},{"key":"e_1_3_3_56_2","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1145\/3302504.3311814","volume-title":"HSCC","author":"Yaghoubi Shakiba","year":"2019","unstructured":"Shakiba Yaghoubi and Georgios Fainekos. 2019. Gray-box adversarial testing for control systems with machine learning components. In HSCC. 179\u2013184."},{"key":"e_1_3_3_57_2","volume-title":"23nd ACM International Conference on Hybrid Systems: Computation and Control","author":"Zarei Mojtaba","year":"2020","unstructured":"Mojtaba Zarei, Yu Wang, and Miroslav Pajic. 2020. Statistical verification of learning-based cyber-physical systems. In 23nd ACM International Conference on Hybrid Systems: Computation and Control."},{"key":"e_1_3_3_58_2","first-page":"243","volume-title":"HSCC","author":"Zuliani Paolo","year":"2010","unstructured":"Paolo Zuliani, Andr\u00e9 Platzer, and Edmund M. Clarke. 2010. Bayesian statistical model checking with application to simulink\/stateflow verification. In HSCC. 243\u2013252."}],"container-title":["ACM Transactions on Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3635160","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3635160","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3635160","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:49:06Z","timestamp":1750286946000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3635160"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,30]]},"references-count":57,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,4,30]]}},"alternative-id":["10.1145\/3635160"],"URL":"https:\/\/doi.org\/10.1145\/3635160","relation":{},"ISSN":["2378-962X","2378-9638"],"issn-type":[{"type":"print","value":"2378-962X"},{"type":"electronic","value":"2378-9638"}],"subject":[],"published":{"date-parts":[[2024,4,30]]},"assertion":[{"value":"2022-11-09","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-11-14","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-05-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}