{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T15:41:52Z","timestamp":1784302912377,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":52,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,5,14]],"date-time":"2024-05-14T00:00:00Z","timestamp":1715644800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100006374","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2237229"],"award-info":[{"award-number":["2237229"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100006374","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-22-1-2156"],"award-info":[{"award-number":["N00014-22-1-2156"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100006374","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-19-1-0288, FA9550-21-1-0121, FA9550-23-1-0066"],"award-info":[{"award-number":["FA9550-19-1-0288, FA9550-21-1-0121, FA9550-23-1-0066"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,5,14]]},"DOI":"10.1145\/3641513.3650141","type":"proceedings-article","created":{"date-parts":[[2024,5,2]],"date-time":"2024-05-02T18:05:48Z","timestamp":1714673148000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Falsification using Reachability of Surrogate Koopman Models"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4947-9553","authenticated-orcid":false,"given":"Stanley","family":"Bak","sequence":"first","affiliation":[{"name":"Stony Brook University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0686-0365","authenticated-orcid":false,"given":"Sergiy","family":"Bogomolov","sequence":"additional","affiliation":[{"name":"Newcastle University, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-9685-0558","authenticated-orcid":false,"given":"Abdelrahman","family":"Hekal","sequence":"additional","affiliation":[{"name":"Newcastle University, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6017-7623","authenticated-orcid":false,"given":"Niklas","family":"Kochdumper","sequence":"additional","affiliation":[{"name":"Stony Brook University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6509-6846","authenticated-orcid":false,"given":"Ethan","family":"Lew","sequence":"additional","affiliation":[{"name":"Galois, Inc, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-7435-332X","authenticated-orcid":false,"given":"Andrew","family":"Mata","sequence":"additional","affiliation":[{"name":"Stony Brook University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7361-1898","authenticated-orcid":false,"given":"Amir","family":"Rahmati","sequence":"additional","affiliation":[{"name":"Stony Brook University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,5,14]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proc. of the Annual Allerton Conference on Communication, Control, and Computing. 1594\u20131601","author":"Abbas H.","unstructured":"H. Abbas and G. Fainekos. 2012. Convergence Proofs for Simulated Annealing Falsification of Safety Properties. In Proc. of the Annual Allerton Conference on Communication, Control, and Computing. 1594\u20131601."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2014.6859453"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSTW.2018.00052"},{"key":"e_1_3_2_1_4_1","volume-title":"Proc. of the International Workshop on Applied Verification for Continuous and Hybrid Systems. 120\u2013151","author":"Althoff M.","year":"2015","unstructured":"M. Althoff. 2015. An Introduction to CORA 2015. In Proc. of the International Workshop on Applied Verification for Continuous and Hybrid Systems. 120\u2013151."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1146\/annurev-control-071420-081941"},{"key":"e_1_3_2_1_6_1","volume-title":"Proc. of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 254\u2013257","author":"Annapureddy Y.","unstructured":"Y. Annapureddy, C. Liu, G. Fainekos, and S. Sankaranarayanan. 2011. S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems. In Proc. of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 254\u2013257."},{"key":"e_1_3_2_1_7_1","volume-title":"Proc. of the Annual Conference on IEEE Industrial Electronics Society. 91\u201396","author":"Annapureddy R.","unstructured":"Y.\u00a0S.\u00a0R. Annapureddy and G. Fainekos. 2010. Ant Colonies for Temporal Logic Falsification of Hybrid Systems. In Proc. of the Annual Conference on IEEE Industrial Electronics Society. 91\u201396."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_20"},{"key":"e_1_3_2_1_9_1","volume-title":"Proc. of the International Conference on Computer Aided Verification. 490\u2013510","author":"Bak S.","unstructured":"S. Bak and et al.2022. Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement. In Proc. of the International Conference on Computer Aided Verification. 490\u2013510."},{"key":"e_1_3_2_1_10_1","volume-title":"Proc. of the International Conference on Hybrid Systems: Computation and Control. Article No. 1.","author":"Bogomolov S.","unstructured":"S. Bogomolov and et al.2019. Falsification of Hybrid Systems Using Symbolic Reachability and Trajectory Splicing. In Proc. of the International Conference on Hybrid Systems: Computation and Control. Article No. 1."},{"key":"e_1_3_2_1_11_1","volume-title":"NASA Formal Methods Symposium. Springer, 109\u2013130","year":"2022","unstructured":"Xin Chen and Sriram Sankaranarayanan. 2022. Reachability Analysis for Cyber-Physical Systems: Are We There Yet?. In NASA Formal Methods Symposium. Springer, 109\u2013130."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1137\/17M115414X"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3126521"},{"key":"e_1_3_2_1_14_1","volume-title":"Proc. of International Symposium on Automated Technology for Verification and Analysis. 500\u2013517","author":"Deshmukh J.","unstructured":"J. Deshmukh, X. Jin, J. Kapinski, and O. Maler. 2015. Stochastic Local Search for Falsification of Hybrid Systems. In Proc. of International Symposium on Automated Technology for Verification and Analysis. 500\u2013517."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_17"},{"key":"e_1_3_2_1_16_1","volume-title":"Proc. of the International Workshop on Applied Verification for Continuous and Hybrid Systems","author":"Donz\u00e9 A.","year":"2015","unstructured":"A. Donz\u00e9, V. Raman, G. Frehse, and M. Althoff. 2015. BluSTL: Controller Synthesis from Signal Temporal Logic Specifications. Proc. of the International Workshop on Applied Verification for Continuous and Hybrid Systems (2015), 160\u2013168."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2020.2966480"},{"key":"e_1_3_2_1_18_1","volume-title":"Proc. of the International Workshop on Applied Verification for Continuous and Hybrid Systems. 204\u2013221","author":"Ernst G.","unstructured":"G. Ernst and et al.2022. ARCH-COMP 2022 Category Report: Falsification with Unbounded Resources. In Proc. of the International Workshop on Applied Verification for Continuous and Hybrid Systems. 204\u2013221."},{"key":"e_1_3_2_1_19_1","volume-title":"Proc. of the International Conference on Quantitative Evaluation of Systems. 165\u2013181","author":"Ernst G.","unstructured":"G. Ernst, S. Sedwards, Z. Zhang, and I. Hasuo. 2019. Fast Falsification of Hybrid Systems Using Probabilistically Adaptive Input. In Proc. of the International Conference on Quantitative Evaluation of Systems. 165\u2013181."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.06.021"},{"key":"e_1_3_2_1_21_1","volume-title":"Proc. of the International Conference on Decision and Control. 1890\u20131895","author":"Han Y.","unstructured":"Y. Han and et al.2020. Deep Learning of Koopman Representation for Control. In Proc. of the International Conference on Decision and Control. 1890\u20131895."},{"key":"e_1_3_2_1_22_1","volume-title":"Proc. of the International Workshop on Applied Verification for Continuous and Hybrid Systems. 25\u201330","author":"Hoxha B.","unstructured":"B. Hoxha, H. Abbas, and G. Fainekos. 2015. Benchmarks for Temporal Logic Requirements for Automotive Systems. In Proc. of the International Workshop on Applied Verification for Continuous and Hybrid Systems. 25\u201330."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2020.3024348"},{"key":"e_1_3_2_1_24_1","volume-title":"Proc. of the International Conference on Hybrid Systems: Computation and Control. Article No. 1.","author":"Kochdumper N.","unstructured":"N. Kochdumper, B. Sch\u00fcrmann, and M. Althoff. 2020. Utilizing Dependencies to Obtain Subsets of Reachable Sets. In Proc. of the International Conference on Hybrid Systems: Computation and Control. Article No. 1."},{"key":"e_1_3_2_1_25_1","volume-title":"Proc. of the International Symposium on Information Theory and Its Applications. 1\u20135.","author":"Komatsu K.","unstructured":"K. Komatsu and H. Takata. 2008. Nonlinear Feedback Control of Stabilization Problem via Formal Linearization Using Taylor Expansion. In Proc. of the International Symposium on Information Theory and Its Applications. 1\u20135."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.17.5.315"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2018.03.046"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"J\u00a0Nathan Kutz Steven\u00a0L Brunton Bingni\u00a0W Brunton and Joshua\u00a0L Proctor. 2016. Dynamic mode decomposition: data-driven modeling of complex systems. SIAM.","DOI":"10.1137\/1.9781611974508"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISORC.2008.25"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1080\/00207178708933847"},{"key":"e_1_3_2_1_31_1","volume-title":"Proc. of the International Symposium on Automated Technology for Verification and Analysis. 237\u2013250","author":"Lew E.","unstructured":"E. Lew and et al.2023. AutoKoopman: A Toolbox for Automated System Identification via Koopman Operator Linearization. In Proc. of the International Symposium on Automated Technology for Verification and Analysis. 237\u2013250."},{"key":"e_1_3_2_1_32_1","first-page":"379","article-title":"Taylor Models and Other Validated Functional Inclusion Methods","volume":"4","author":"Makino K.","year":"2003","unstructured":"K. Makino and M. Berz. 2003. Taylor Models and Other Validated Functional Inclusion Methods. International Journal of Pure and Applied Mathematics 4, 4 (2003), 379\u2013456.","journal-title":"International Journal of Pure and Applied Mathematics"},{"key":"e_1_3_2_1_33_1","volume-title":"Proc. of the International Conference on Formal Modelling and Analysis of Timed Systems. 152\u2013166","author":"Maler O.","unstructured":"O. Maler and D. Nickovic. 2004. Monitoring Temporal Properties of Continuous Signals. In Proc. of the International Conference on Formal Modelling and Analysis of Timed Systems. 152\u2013166."},{"key":"e_1_3_2_1_34_1","volume-title":"Efficient Optimization-Based Falsification of Cyber-Physical Systems with Multiple Conjunctive Requirements. In Prof. of the International Conference on Automation Science and Engineering. 732\u2013737","author":"Mathesen L.","unstructured":"L. Mathesen, G. Pedrielli, and G. Fainekos. 2021. Efficient Optimization-Based Falsification of Cyber-Physical Systems with Multiple Conjunctive Requirements. In Prof. of the International Conference on Automation Science and Engineering. 732\u2013737."},{"key":"e_1_3_2_1_35_1","volume-title":"Proc. of the International Conference on Automation Science and Engineering. 991\u2013997","author":"Mathesen L.","unstructured":"L. Mathesen, S. Yaghoubi, G. Pedrielli, and G. Fainekos. 2019. Falsification of Cyber-Physical Systems with Robustness Uncertainty Quantification Through Stochastic Optimization with Adaptive Restart. In Proc. of the International Conference on Automation Science and Engineering. 991\u2013997."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380370"},{"key":"e_1_3_2_1_37_1","volume-title":"Proc. of the International Conference on Hybrid Systems: Computation and Control. 211\u2013220","author":"Nghiem T.","unstructured":"T. Nghiem and et al.2010. Monte-Carlo Techniques for Falsification of Temporal Properties of Non-Linear Hybrid Systems. In Proc. of the International Conference on Hybrid Systems: Computation and Control. 211\u2013220."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1002\/rnc.6536"},{"key":"e_1_3_2_1_39_1","volume-title":"Logical foundations of cyber-physical systems. Vol.\u00a0662","unstructured":"Andr\u00e9 Platzer. 2018. Logical foundations of cyber-physical systems. Vol.\u00a0662. Springer."},{"key":"e_1_3_2_1_40_1","volume-title":"Proc. of the Design Automation Conference. 731\u2013736","author":"Rajkumar R.","unstructured":"R. Rajkumar, I. Lee, L. Sha, and J. Stankovic. 2010. Cyber-Physical Systems: The Next Computing Revolution. In Proc. of the Design Automation Conference. 731\u2013736."},{"key":"e_1_3_2_1_41_1","volume-title":"Proc. of the International Conference on Decision and Control. 81\u201387","author":"Raman V.","unstructured":"V. Raman and et al.2014. Model Predictive Control with Signal Temporal Logic Specifications. In Proc. of the International Conference on Decision and Control. 81\u201387."},{"key":"e_1_3_2_1_42_1","volume-title":"Proc. of the International Workshop on Formal Techniques for Safety-Critical Systems. 3\u201318","author":"Rashid A.","unstructured":"A. Rashid, U. Siddique, and S. Tahar. 2020. Formal Verification of Cyber-Physical Systems Using Theorem Proving. In Proc. of the International Workshop on Formal Techniques for Safety-Critical Systems. 3\u201318."},{"key":"e_1_3_2_1_43_1","volume-title":"Proc. of the International Conference on Methods and Models in Automation and Robotics. 455\u2013460","author":"Rauh A.","unstructured":"A. Rauh and et al.2009. Carleman Linearization for Control and for State and Disturbance Estimation of Nonlinear Dynamical Processes. In Proc. of the International Conference on Methods and Models in Automation and Robotics. 455\u2013460."},{"key":"e_1_3_2_1_44_1","volume-title":"Proc. of the International Conference on Hybrid Systems: Computation and Control. 125\u2013134","author":"Sankaranarayanan S.","unstructured":"S. Sankaranarayanan and G. Fainekos. 2012. Falsification of Temporal Properties of Hybrid Systems Using the Cross-Entropy Method. In Proc. of the International Conference on Hybrid Systems: Computation and Control. 125\u2013134."},{"key":"e_1_3_2_1_45_1","unstructured":"T. S\u00f6derstr\u00f6m and P Stoica. 1989. System Identification."},{"key":"e_1_3_2_1_46_1","volume-title":"Proc. of the International Conference on Formal Methods for Industrial Critical Systems. 223\u2013231","author":"Thibeault Q.","unstructured":"Q. Thibeault and et al.2021. PSY-TaLiRo: A Python Toolbox for Search-Based Test Generation for Cyber-Physical Systems. In Proc. of the International Conference on Formal Methods for Industrial Critical Systems. 223\u2013231."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3365365.3382193"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00332-015-9258-5"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2020.2969178"},{"key":"e_1_3_2_1_50_1","volume-title":"Proc. of the American Control Conference. 4832\u20134839","author":"Yeung E.","unstructured":"E. Yeung and et al.2019. Learning Deep Neural Network Representations for Koopman Operators of Nonlinear Dynamical Systems. In Proc. of the American Control Conference. 4832\u20134839."},{"key":"e_1_3_2_1_51_1","volume-title":"Proc. of the International Conference on Computer Aided Verification. 595\u2013618","author":"Zhang Z.","unstructured":"Z. Zhang and et al.2021. Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness. In Proc. of the International Conference on Computer Aided Verification. 595\u2013618."},{"key":"e_1_3_2_1_52_1","volume-title":"Proc. of the International Conference on Embedded Software. Article No. 5.","author":"Zutshi A.","unstructured":"A. Zutshi, J.\u00a0V. Deshmukh, S. Sankaranarayanan, and J. Kapinski. 2014. Multiple Shooting, CEGAR-Based Falsification for Hybrid Systems. In Proc. of the International Conference on Embedded Software. Article No. 5."}],"event":{"name":"HSCC '24: Computation and Control","location":"Hong Kong SAR China","acronym":"HSCC '24","sponsor":["SIGCHI ACM Special Interest Group on Computer-Human Interaction"]},"container-title":["Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3641513.3650141","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3641513.3650141","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T00:12:48Z","timestamp":1755907968000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3641513.3650141"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,14]]},"references-count":52,"alternative-id":["10.1145\/3641513.3650141","10.1145\/3641513"],"URL":"https:\/\/doi.org\/10.1145\/3641513.3650141","relation":{},"subject":[],"published":{"date-parts":[[2024,5,14]]},"assertion":[{"value":"2024-05-14","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}