{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T15:41:51Z","timestamp":1784302911446,"version":"3.55.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2021,7,18]],"date-time":"2021-07-18T00:00:00Z","timestamp":1626566400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["15KT0012"],"award-info":[{"award-number":["15KT0012"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002241","name":"Japan Science and Technology Agency","doi-asserted-by":"publisher","award":["JPMJER1603"],"award-info":[{"award-number":["JPMJER1603"]}],"id":[{"id":"10.13039\/501100002241","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Model. Comput. Simul."],"published-print":{"date-parts":[[2021,7,31]]},"abstract":"<jats:p>We present and analyse an algorithm that quickly finds falsifying inputs for hybrid systems. Our method is based on a probabilistically directed tree search, whose distribution adapts to consider an increasingly fine-grained discretization of the input space. In experiments with standard benchmarks, our algorithm shows comparable or better performance to existing techniques, yet it does not build an explicit model of a system. Instead, at each decision point within a single trial, it makes an uninformed probabilistic choice between simple strategies to extend the input signal by means of exploration or exploitation. Key to our approach is the way input signal space is decomposed into levels, such that coarse segments are more probable than fine segments. We perform experiments to demonstrate how and why our approach works, finding that a fully randomized exploration strategy performs as well as our original algorithm that exploits robustness. We propose this strategy as a new baseline for falsification and conclude that more discriminative benchmarks are required.<\/jats:p>","DOI":"10.1145\/3459605","type":"journal-article","created":{"date-parts":[[2021,7,18]],"date-time":"2021-07-18T16:04:06Z","timestamp":1626624246000},"page":"1-22","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":24,"title":["Falsification of Hybrid Systems Using Adaptive Probabilistic Search"],"prefix":"10.1145","volume":"31","author":[{"given":"Gidon","family":"Ernst","sequence":"first","affiliation":[{"name":"Ludwig-Maximilians-University, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sean","family":"Sedwards","sequence":"additional","affiliation":[{"name":"University of Waterloo, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhenya","family":"Zhang","sequence":"additional","affiliation":[{"name":"National Institute of Informatics"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ichiro","family":"Hasuo","sequence":"additional","affiliation":[{"name":"National Institute of Informatics"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,7,18]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_24"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46982-9_27"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_21"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19835-9_21"},{"key":"e_1_2_1_5_1","article-title":"Underminer: A framework for automatically identifying nonconverging behaviors in black-box system models","volume":"17","author":"Balkan Ayca","year":"2017","unstructured":"Ayca Balkan , Paulo Tabuada , Jyotirmoy V. Deshmukh , Xiaoqing Jin , and James Kapinski . 2017 . Underminer: A framework for automatically identifying nonconverging behaviors in black-box system models . ACM Trans. Embed. Comput. Syst. 17 , 1, Article 20 (2017), 28 pages. Ayca Balkan, Paulo Tabuada, Jyotirmoy V. Deshmukh, Xiaoqing Jin, and James Kapinski. 2017. Underminer: A framework for automatically identifying nonconverging behaviors in black-box system models. ACM Trans. Embed. Comput. Syst. 17, 1, Article 20 (2017), 28 pages.","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"e_1_2_1_6_1","volume-title":"Lectures on Runtime Verification","author":"Bartocci Ezio","unstructured":"Ezio Bartocci , Jyotirmoy Deshmukh , Alexandre Donz\u00e9 , Georgios Fainekos , Oded Maler , Dejan Ni\u010dkovi\u0107 , and Sriram Sankaranarayanan . 2018. Specification-based monitoring of cyber-physical systems: A survey on theory, tools and applications . In Lectures on Runtime Verification . Springer , 135\u2013175. Ezio Bartocci, Jyotirmoy Deshmukh, Alexandre Donz\u00e9, Georgios Fainekos, Oded Maler, Dejan Ni\u010dkovi\u0107, and Sriram Sankaranarayanan. 2018. Specification-based monitoring of cyber-physical systems: A survey on theory, tools and applications. In Lectures on Runtime Verification. Springer, 135\u2013175."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461348"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24953-7_35"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH\u201917)","volume":"48","author":"Dokhanchi Adel","unstructured":"Adel Dokhanchi , Shakiba Yaghoubi , Bardh Hoxha , and Georgios E. Fainekos . 2017. ARCH-COMP17 category report: Preliminary results on the falsification benchmarks . In Proceedings of the International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH\u201917) (EPiC Series in Computing), Goran Frehse and Matthias Althoff (Eds.) , Vol. 48 . EasyChair, 170\u2013174. Adel Dokhanchi, Shakiba Yaghoubi, Bardh Hoxha, and Georgios E. Fainekos. 2017. ARCH-COMP17 category report: Preliminary results on the falsification benchmarks. In Proceedings of the International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH\u201917) (EPiC Series in Computing), Goran Frehse and Matthias Althoff (Eds.), Vol. 48. EasyChair, 170\u2013174."},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH\u201919)","volume":"54","author":"Dokhanchi Adel","year":"2019","unstructured":"Adel Dokhanchi , Shakiba Yaghoubi , Bardh Hoxha , Georgios E. Fainekos , Gidon Ernst , Zhenya Zhang , Paolo Arcaini , Ichiro Hasuo , and Sean Sedwards . 2019 . ARCH-COMP18 Category report: Results on the falsification benchmarks . In Proceedings of the International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH\u201919) (EPiC Series in Computing), Goran Frehse (Ed.) , Vol. 54 . EasyChair, 104\u2013109. Adel Dokhanchi, Shakiba Yaghoubi, Bardh Hoxha, Georgios E. Fainekos, Gidon Ernst, Zhenya Zhang, Paolo Arcaini, Ichiro Hasuo, and Sean Sedwards. 2019. ARCH-COMP18 Category report: Results on the falsification benchmarks. In Proceedings of the International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH\u201919) (EPiC Series in Computing), Goran Frehse (Ed.), Vol. 54. EasyChair, 104\u2013109."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_17"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_19"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15297-9_9"},{"key":"e_1_2_1_14_1","volume-title":"Deshmukh","author":"Dreossi Tommaso","year":"2015","unstructured":"Tommaso Dreossi , Thao Dang , Alexandre Donz\u00e9 , James Kapinski , Xiaoqing Jin , and Jyotirmoy V . Deshmukh . 2015 . Efficient guiding strategies for testing of temporal properties of hybrid systems. In NASA Formal Methods (LNCS), Klaus Havelund, Gerard Holzmann, and Rajeev Joshi (Eds.), Vol. 9058 . Springer , 127\u2013142. Tommaso Dreossi, Thao Dang, Alexandre Donz\u00e9, James Kapinski, Xiaoqing Jin, and Jyotirmoy V. Deshmukh. 2015. Efficient guiding strategies for testing of temporal properties of hybrid systems. In NASA Formal Methods (LNCS), Klaus Havelund, Gerard Holzmann, and Rajeev Joshi (Eds.), Vol. 9058. Springer, 127\u2013142."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/COASE.2017.8256285"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.29007\/trr1"},{"key":"e_1_2_1_17_1","volume-title":"Quantitative Evaluation of Systems (LNCS)","author":"Ernst Gidon","unstructured":"Gidon Ernst , Sean Sedwards , Zhenya Zhang , and Ichiro Hasuo . 2019. Fast falsification of hybrid systems using probabilistically adaptive input . In Quantitative Evaluation of Systems (LNCS) , Vol. 11785 . Springer , 165\u2013181. Gidon Ernst, Sean Sedwards, Zhenya Zhang, and Ichiro Hasuo. 2019. Fast falsification of hybrid systems using probabilistically adaptive input. In Quantitative Evaluation of Systems (LNCS), Vol. 11785. Springer, 165\u2013181."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.06.021"},{"key":"e_1_2_1_19_1","volume-title":"Hansen","author":"Fr\u00e4nzle Martin","year":"2005","unstructured":"Martin Fr\u00e4nzle and Michael R . Hansen . 2005 . A robust interpretation of duration calculus. In International Colloquium on Theoretical Aspects of Computing. Springer , 257\u2013271. Martin Fr\u00e4nzle and Michael R. Hansen. 2005. A robust interpretation of duration calculus. In International Colloquium on Theoretical Aspects of Computing. Springer, 257\u2013271."},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH@ ADHS\u201918)","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 Proceedings of the International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH@ ADHS\u201918) . 208\u2013217. Peter Heidlauf, Alexander Collins, Michael Bolender, and Stanley Bak. 2018. Verification challenges in F-16 ground collision avoidance and other automated maneuvers. In Proceedings of the International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH@ ADHS\u201918). 208\u2013217."},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH\u201914)","volume":"34","author":"Hoxha Bardh","unstructured":"Bardh Hoxha , Houssam Abbas , and Georgios E. Fainekos . 2014. Benchmarks for temporal logic requirements for automotive systems . In Proceedings of the International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH\u201914) (EPiC Series in Computing), Goran Frehse and Matthias Althoff (Eds.) , Vol. 34 . EasyChair, 25\u201330. Bardh Hoxha, Houssam Abbas, and Georgios E. Fainekos. 2014. Benchmarks for temporal logic requirements for automotive systems. In Proceedings of the International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH\u201914) (EPiC Series in Computing), Goran Frehse and Matthias Althoff (Eds.), Vol. 34. EasyChair, 25\u201330."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46430-1_16"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1162\/evco.2007.15.1.1"},{"key":"e_1_2_1_24_1","volume-title":"Computer Aided Verification. LNCS","author":"Jegourel Cyrille","unstructured":"Cyrille Jegourel , Axel Legay , and Sean Sedwards . 2013. Importance splitting for statistical model checking rare properties . In Computer Aided Verification. LNCS , Vol. 8044 . Springer , 576\u2013591. Cyrille Jegourel, Axel Legay, and Sean Sedwards. 2013. Importance splitting for statistical model checking rare properties. In Computer Aided Verification. LNCS, Vol. 8044. Springer, 576\u2013591."},{"key":"e_1_2_1_25_1","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications (ISoLA), Tiziana Margaria and Bernhard Steffen (Eds.). LNCS","author":"Jegourel Cyrille","unstructured":"Cyrille Jegourel , Axel Legay , and Sean Sedwards . 2014. An effective heuristic for adaptive importance splitting in statistical model checking . In Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications (ISoLA), Tiziana Margaria and Bernhard Steffen (Eds.). LNCS , Vol. 8803 . Springer , 143\u2013159. Cyrille Jegourel, Axel Legay, and Sean Sedwards. 2014. An effective heuristic for adaptive importance splitting in statistical model checking. In Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications (ISoLA), Tiziana Margaria and Bernhard Steffen (Eds.). LNCS, Vol. 8803. Springer, 143\u2013159."},{"key":"e_1_2_1_26_1","volume-title":"Butts","author":"Jin Xiaoqing","year":"2014","unstructured":"Xiaoqing Jin , Jyotirmoy V. Deshmukh , James Kapinski , Koichi Ueda , and Kenneth R . Butts . 2014 . Powertrain control verification benchmark. In Hybrid Systems: Computation and Control (HSCC), Martin Fr\u00e4nzle and John Lygeros (Eds.). ACM , 253\u2013262. Xiaoqing Jin, Jyotirmoy V. Deshmukh, James Kapinski, Koichi Ueda, and Kenneth R. Butts. 2014. Powertrain control verification benchmark. In Hybrid Systems: Computation and Control (HSCC), Martin Fr\u00e4nzle and John Lygeros (Eds.). ACM, 253\u2013262."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2015.2421907"},{"key":"e_1_2_1_28_1","first-page":"6","article-title":"Simulation-based approaches for verification of embedded control systems: An overview of traditional and advanced modeling, testing, and verification techniques","volume":"36","author":"Kapinski James","year":"2016","unstructured":"James Kapinski , Jyotirmoy V. Deshmukh , Xiaoqing Jin , Hisahiro Ito , and Ken Butts . 2016 . Simulation-based approaches for verification of embedded control systems: An overview of traditional and advanced modeling, testing, and verification techniques . IEEE Control Syst. Mag. 36 , 6 (Dec 2016), 45\u201364. James Kapinski, Jyotirmoy V. Deshmukh, Xiaoqing Jin, Hisahiro Ito, and Ken Butts. 2016. Simulation-based approaches for verification of embedded control systems: An overview of traditional and advanced modeling, testing, and verification techniques. IEEE Control Syst. Mag. 36, 6 (Dec 2016), 45\u201364.","journal-title":"IEEE Control Syst. Mag."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1177\/02783640122067453"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the IEEE\/AIAA 34th Digital Avionics Systems Conference (DASC\u201915)","author":"Lee Ritchie","unstructured":"Ritchie Lee , Mykel J. Kochenderfer , Ole J. Mengshoel , Guillaume P. Brat , and Michael P. Owen . 2015. Adaptive stress testing of airborne collision avoidance systems . In Proceedings of the IEEE\/AIAA 34th Digital Avionics Systems Conference (DASC\u201915) . 6C2:1\u20136C2:13. Ritchie Lee, Mykel J. Kochenderfer, Ole J. Mengshoel, Guillaume P. Brat, and Michael P. Owen. 2015. Adaptive stress testing of airborne collision avoidance systems. In Proceedings of the IEEE\/AIAA 34th Digital Avionics Systems Conference (DASC\u201915). 6C2:1\u20136C2:13."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380370"},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH\u201916)","author":"Schuler Simone","year":"2016","unstructured":"Simone Schuler , Fabiano Daher Adegas , and Adolfo Anta . 2016 . Hybrid modelling of a wind turbine (benchmark proposal) . Proceedings of the International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH\u201916) . Simone Schuler, Fabiano Daher Adegas, and Adolfo Anta. 2016. Hybrid modelling of a wind turbine (benchmark proposal). Proceedings of the International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH\u201916)."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66845-1_1"},{"key":"e_1_2_1_34_1","volume-title":"Barto","author":"Sutton Richard S.","year":"2018","unstructured":"Richard S. Sutton and Andrew G . Barto . 2018 . Reinforcement Learning : An Introduction (2nd ed.). MIT Press . Richard S. Sutton and Andrew G. Barto. 2018. Reinforcement Learning: An Introduction (2nd ed.). MIT Press."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3365365.3382193"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/4235.585893"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302504.3311814"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH\u201919)","volume":"61","author":"Yaghoubi Shakiba","year":"2019","unstructured":"Shakiba Yaghoubi , Bardh Hoxha , Georgios E. Fainekos , Gidon Ernst , Zhenya Zhang , Paolo Arcaini , Ichiro Hasuo , and Sean Sedwards . 2019 . ARCH-COMP19 category report: Falsification . In Proceedings of the International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH\u201919) (EPiC Series in Computing), Goran Frehse (Ed.) , Vol. 61 . EasyChair, 129\u2013140. Shakiba Yaghoubi, Bardh Hoxha, Georgios E. Fainekos, Gidon Ernst, Zhenya Zhang, Paolo Arcaini, Ichiro Hasuo, and Sean Sedwards. 2019. ARCH-COMP19 category report: Falsification. In Proceedings of the International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH\u201919) (EPiC Series in Computing), Goran Frehse (Ed.), Vol. 61. EasyChair, 129\u2013140."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2020.2969178"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/MT-CPS.2018.00008"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2018.2858463"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2656045.2656061"}],"container-title":["ACM Transactions on Modeling and Computer Simulation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3459605","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3459605","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3459605","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T17:49:11Z","timestamp":1750268951000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3459605"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,7,18]]},"references-count":42,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,7,31]]}},"alternative-id":["10.1145\/3459605"],"URL":"https:\/\/doi.org\/10.1145\/3459605","relation":{},"ISSN":["1049-3301","1558-1195"],"issn-type":[{"value":"1049-3301","type":"print"},{"value":"1558-1195","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,7,18]]},"assertion":[{"value":"2020-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-07-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}