{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,29]],"date-time":"2026-05-29T05:02:33Z","timestamp":1780030953828,"version":"3.53.1"},"reference-count":69,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2026,5,12]],"date-time":"2026-05-12T00:00:00Z","timestamp":1778544000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"Office of Naval Research (ONR) MURI","award":["N00014-20-1-2787"],"award-info":[{"award-number":["N00014-20-1-2787"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Cyber-Phys. Syst."],"published-print":{"date-parts":[[2026,7,31]]},"abstract":"<jats:p>Validating the behavior of autonomous Cyber-Physical Systems (CPS) and AI agents, which rely on automated controllers, is an objective of great importance. In recent years, Neural-Network (NN) controllers have been demonstrating great promise and experiencing tremendous popularity. Unfortunately, such learned controllers are often not certified and can cause the system to suffer from unpredictable or unsafe behavior. To mitigate this issue, a great effort has been dedicated to automated verification of systems. Specifically, works in the category of \u201cblack-box testing\u201d rely on repeated system simulations to find a falsifying counterexample\u2014a system run that violates a specification. As running high-fidelity simulations is computationally demanding, the goal of falsification approaches is to minimize the simulation effort needed to return a falsifying example. This often proves to be a great challenge, especially when the tested controller is well trained. This work contributes a novel falsification approach for autonomous systems under formal specification operating in uncertain environments. We are especially interested in CPS operating in rich, semantically defined, open environments, which yield high-dimensional, simulation-dependent sensor observations as inputs to the controller. Our approach introduces a novel reformulation of the falsification problem as the problem of planning a trajectory for a \u201cmeta-system,\u201d which wraps and encapsulates the examined system; we call this approach: meta-planning. This approach results in testing fewer inputs, compared to serial input sampling, while making minimal assumptions on the system, and posing no limitation on the specification, environment, or controller, which is treated as a black-box. It also avoids redundant calculations and requires less effort for each test, by invoking only incremental updates to the autonomous-system\u2019s trajectory at each iteration, using partial simulations. This formulation can be solved with standard sampling-based motion-planning techniques (like RRT), can gradually integrate domain knowledge to improve the search, based on its availability, and can even work with no domain knowledge at all. We support these ideas with an experimental study on falsification of an obstacle-avoiding autonomous car with a NN controller, where meta-planning demonstrates superior performance over alternative approaches.<\/jats:p>","DOI":"10.1145\/3801740","type":"journal-article","created":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T16:39:18Z","timestamp":1773419958000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Falsification of Autonomous Systems in Rich Environments"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1391-8956","authenticated-orcid":false,"given":"Khen","family":"Elimelech","sequence":"first","affiliation":[{"name":"King\u2019s College London, London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7549-4365","authenticated-orcid":false,"given":"Morteza","family":"Lahijanian","sequence":"additional","affiliation":[{"name":"University of Colorado Boulder, Boulder, Colorado, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0699-8038","authenticated-orcid":false,"given":"Lydia E.","family":"Kavraki","sequence":"additional","affiliation":[{"name":"Rice University, Houston, Texas, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0661-5773","authenticated-orcid":false,"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[{"name":"Rice University, Houston, Texas, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,5,12]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3503914"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10462-021-09997-9"},{"key":"e_1_3_2_4_2","first-page":"1","article-title":"A survey of imitation learning: Algorithms, recent developments, and challenges","author":"Zare M.","year":"2024","unstructured":"M. Zare, P. M. Kebria, A. Khosravi, and S. Nahavandi. 2024. A survey of imitation learning: Algorithms, recent developments, and challenges. IEEE Transactions on Cybernetics (2024), 1\u201314.","journal-title":"IEEE Transactions on Cybernetics"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-13050-3_4"},{"key":"e_1_3_2_6_2","volume-title":"Structure and Interpretation of Signals and Systems","author":"Lee E. A.","year":"2011","unstructured":"E. A. Lee and P. Varaiya. 2011. Structure and Interpretation of Signals and Systems (2nd Ed.). LeeVaraiya.org."},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","unstructured":"R. Ehlers. 2017. Formal verification of piece-wise linear feed-forward neural networks. In Automated Technology for Verification and Analysis. Deepak D\u2019Souza and K. Narayan Kumar (Eds.) Springer International Publishing Cham 269\u2013286. DOI: 10.1007\/978-3-319-68167-2_19","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.5555\/3327345.3327533"},{"key":"e_1_3_2_11_2","first-page":"5276","volume-title":"Proceedings of the 35th International Conference on Machine Learning","author":"Weng L.","year":"2018","unstructured":"L. Weng, H. Zhang, H. Chen, Z. Song, C. J. Hsieh, L. Daniel, D. Boning, and I. Dhillon. 2018. Towards fast computation of certified robustness for ReLU networks. In Proceedings of the 35th International Conference on Machine Learning. PMLR, 5276\u20135285."},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2017.8263977"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2005.851439"},{"key":"e_1_3_2_14_2","first-page":"184","volume-title":"Proceedings of the 16th International Conference on Principles of Knowledge Representation and Reasoning (KR \u201918)","author":"Akintunde M. E.","year":"2018","unstructured":"M. E. Akintunde, A. Lomuscio, L. Maganti, and E. Pirovano. 2018. Reachability analysis for neural agent-environment systems. In Proceedings of the 16th International Conference on Principles of Knowledge Representation and Reasoning (KR \u201918), 184\u2013193."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/3302504.3311806"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3419742"},{"key":"e_1_3_2_17_2","unstructured":"W. Xiang and T. T. Johnson. 2018. Reachability analysis and safety verification for neural network control systems. In Proceedings of the Thirty-Seventh AAAI Conference on Artificial Intelligence and Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence and Thirteenth Symposium on Educational Advances in Artificial Intelligence 15287\u201315295. Retrieved from https:\/\/dl.acm.org\/doi\/10.1609\/aaai.v37i12.26783"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1581"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1613\/jair.1.12716"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.06.021"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_21"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.5555\/AAI30168538"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3126521"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2018.8460635"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/CASE49439.2021.9551474"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_23"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","unstructured":"Z. Ramezani K. \u0160ehi\u0107 L. Nardi and K. \u00c5kesson. 2025. Falsification of cyber-physical systems using Bayesian optimization. ACM Transactions on Embedded Computing Systems 24 3 Article 41 (2025) 1\u201323. DOI: 10.1145\/3711922","DOI":"10.1145\/3711922"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2021.3110740"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/2465787.2465797"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSTW.2018.00052"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/2185632.2185653"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.2514\/1.D0020"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1109\/MCS.2003.1213603"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICEC.1996.542381"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE5003.2020.00012"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2022.3194640"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-09509-5"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1146\/annurev-control-061623-094742"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2014.2302442"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1177\/0278364908097582"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1609\/icaps.v33i1.27172"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-008-0058-5"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0233-2"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/10991541_9"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1109\/ITSC.2019.8917375"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/3459605"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1613\/jair.1129"},{"key":"e_1_3_2_51_2","first-page":"854","volume-title":"Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI \u201913)","author":"De Giacomo G.","year":"2013","unstructured":"G. De Giacomo and M. Y. Vardi. 2013. Linear temporal logic and linear dynamic logic on finite traces. In Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI \u201913). AAAI Press, Beijing, China, 854\u2013860."},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2018.2858463"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1109\/ITSC45102.2020.9294549"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2020.2969178"},{"key":"e_1_3_2_55_2","first-page":"133","volume-title":"Proceedings of the 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH \u201921)","author":"Ernst G.","year":"2021","unstructured":"G. Ernst, P. Arcaini, I. Bennani, A. Chandratre, A. Donz\u00e9, G. Fainekos, G. Frehse, K. Gaaloul, J. Inoue, T. Khandait, et al. 2021. ARCH-COMP 2021 category report: Falsification with validation of results. In Proceedings of the 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH \u201921), 133\u2013112"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19835-9_21"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_17"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/2562059.2562140"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1145\/3076125.3076128"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_25"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10994-021-06120-5"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1177\/0278364915614386"},{"key":"e_1_3_2_63_2","first-page":"1","volume-title":"Encyclopedia of Robotics","author":"Cort\u00e9s J.","year":"2020","unstructured":"J. Cort\u00e9s and T. Sim\u00e9on. 2020. Sampling-based tree planners (RRT, EST, and variations). In Encyclopedia of Robotics. M.H. Ang, O. Khatib, and B. Siciliano (Eds.). Springer, Berlin, 1\u20139."},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1177\/02783640122067453"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.1177\/027836402320556421"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2011.2160466"},{"key":"e_1_3_2_67_2","volume-title":"Proceedings of the Workshop on Software Challenges in Formal Methods for Robotics (FMR), in Conjunction with ICRA 2024","author":"Elimelech K.","year":"2024","unstructured":"K. Elimelech, M. Lahijanian, M. Y. Vardi, and L. E. Kavraki. 2024. LiteRacer: A lightweight autonomous vehicle simulator for benchmarking and development of formal verification techniques. In Proceedings of the Workshop on Software Challenges in Formal Methods for Robotics (FMR), in Conjunction with ICRA 2024."},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","unstructured":"G. Brockman V. Cheung L. Pettersson J. Schneider J. Schulman J. Tang and W. Zaremba. 2016. OpenAI Gym. arXiv:1606.01540. Retrieved from 10.48550\/arXiv.1606.01540","DOI":"10.48550\/arXiv.1606.01540"},{"issue":"268","key":"e_1_3_2_69_2","first-page":"1","article-title":"Stable-baselines3: Reliable reinforcement learning implementations","volume":"22","author":"Raffin A.","year":"2021","unstructured":"A. Raffin, A. Hill, A. Gleave, A. Kanervisto, M. Ernestus, and N. Dormann. 2021. Stable-baselines3: Reliable reinforcement learning implementations. Journal of Machine Learning Research 22, 268 (2021), 1\u20138.","journal-title":"Journal of Machine Learning Research"},{"key":"e_1_3_2_70_2","unstructured":"F. Nogueira. 2014. Bayesian Optimization: Open Source Constrained Global Optimization Tool for Python. Retrieved from https:\/\/github.com\/bayesian-optimization\/BayesianOptimization"}],"container-title":["ACM Transactions on Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3801740","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,29]],"date-time":"2026-05-29T04:17:02Z","timestamp":1780028222000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3801740"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,5,12]]},"references-count":69,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2026,7,31]]}},"alternative-id":["10.1145\/3801740"],"URL":"https:\/\/doi.org\/10.1145\/3801740","relation":{},"ISSN":["2378-962X","2378-9638"],"issn-type":[{"value":"2378-962X","type":"print"},{"value":"2378-9638","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,5,12]]},"assertion":[{"value":"2025-01-04","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-02-08","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-05-12","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}