{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T21:06:31Z","timestamp":1769720791012,"version":"3.49.0"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031787492","type":"print"},{"value":"9783031787508","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-78750-8_12","type":"book-chapter","created":{"date-parts":[[2025,2,11]],"date-time":"2025-02-11T12:15:56Z","timestamp":1739276156000},"page":"234-255","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Fast Koopman Surrogate Falsification Using Linear Relaxations and\u00a0Weights"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4947-9553","authenticated-orcid":false,"given":"Stanley","family":"Bak","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-9685-0558","authenticated-orcid":false,"given":"Abdelrahman","family":"Hekal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6017-7623","authenticated-orcid":false,"given":"Niklas","family":"Kochdumper","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6509-6846","authenticated-orcid":false,"given":"Ethan","family":"Lew","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-7435-332X","authenticated-orcid":false,"given":"Andrew","family":"Mata","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7361-1898","authenticated-orcid":false,"given":"Amir","family":"Rahmati","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,2,12]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Abbas, H., Fainekos, G.: Convergence proofs for simulated annealing falsification of safety properties. In: Proceedings of the Annual Allerton Conference on Communication, Control, and Computing, pp. 1594\u20131601 (2012)","DOI":"10.1109\/Allerton.2012.6483411"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Annapureddy, Y.S.R., Fainekos, G.: Ant colonies for temporal logic falsification of hybrid systems. In: Proceedings of the Annual Conference of the IEEE Industrial Electronics Society, pp. 91\u201396 (2010)","DOI":"10.1109\/IECON.2010.5675195"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: A tool for temporal logic falsification for hybrid systems. In: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 254\u2013257 (2011)","DOI":"10.1007\/978-3-642-19835-9_21"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Bak, S., et\u00a0al.: Reachability of black-box nonlinear systems after Koopman operator linearization. In: Proceedings of the International Conference on Analysis and Design of Hybrid Systems, pp. 253\u2013258 (2021)","DOI":"10.1016\/j.ifacol.2021.08.507"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Bak, S., et\u00a0al.: Reachability of Koopman linearized systems using random Fourier feature observables and polynomial zonotope refinement. In: Proceedings of the International Conference on Computer Aided Verification, pp. 490\u2013510 (2022)","DOI":"10.1007\/978-3-031-13185-1_24"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Bak, S., et\u00a0al.: Falsification using reachability of surrogate Koopman models. In: Proceedings of the International Conference on Hybrid Systems: Computation and Control (2024). Article No. 27","DOI":"10.1145\/3641513.3650141"},{"key":"12_CR7","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1016\/j.arcontrol.2021.09.002","volume":"52","author":"P Bevanda","year":"2021","unstructured":"Bevanda, P., Sosnowski, S., Hirche, S.: Koopman operator dynamical models: Learning, analysis and control. Annu. Rev. Control. 52, 197\u2013212 (2021)","journal-title":"Annu. Rev. Control."},{"issue":"4","key":"12_CR8","doi-asserted-by":"publisher","first-page":"904","DOI":"10.1287\/trsc.2022.1128","volume":"56","author":"Z Cheng","year":"2022","unstructured":"Cheng, Z., Tr\u00e9panier, M., Sun, L.: Real-time forecasting of metro origin-destination matrices with high-order weighted dynamic mode decomposition. Transp. Sci. 56(4), 904\u2013918 (2022)","journal-title":"Transp. Sci."},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Deshmukh, J., et\u00a0al.: Testing cyber-physical systems through Bayesian optimization. ACM Trans. Embedded Comput. Syst. 16(5s) (2017). Article No. 170","DOI":"10.1145\/3126521"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Donz\u00e9, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Proceedings of the International Conference on Computer Aided Verification, pp. 167\u2013170 (2010)","DOI":"10.1007\/978-3-642-14295-6_17"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Ernst, G., et\u00a0al.: ARCH-COMP 2022 category report: Falsification with Ubounded resources. In: Proceedings of the International Workshop on Applied Verification of Continuous and Hybrid Systems, pp. 204\u2013221 (2022)","DOI":"10.29007\/fhnk"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Ernst, G., Sedwards, S., Zhang, Z., Hasuo, I.: Fast falsification of hybrid systems using probabilistically adaptive input. In: Proceedings of the International Conference on Quantitative Evaluation of Systems, pp. 165\u2013181 (2019)","DOI":"10.1007\/978-3-030-30281-8_10"},{"issue":"42","key":"12_CR13","doi-asserted-by":"publisher","first-page":"4262","DOI":"10.1016\/j.tcs.2009.06.021","volume":"410","author":"G Fainekos","year":"2009","unstructured":"Fainekos, G., Pappas, G.: Robustness of temporal logic specifications for continuous-time signals. Theoret. Comput. Sci. 410(42), 4262\u20134291 (2009)","journal-title":"Theoret. Comput. Sci."},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Ferr\u00e8re, T., et\u00a0al.: Interface-aware signal temporal logic. In: Proceedings of the International Conference on Hybrid Systems: Computation and Control, pp. 57\u201366 (2019)","DOI":"10.1145\/3302504.3311800"},{"key":"12_CR15","unstructured":"Garey, M.R., Johnson, D.S.: A guide to the theory of NP-completeness. Comput. Intractabil. 37\u201379 (1990)"},{"issue":"1","key":"12_CR16","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1109\/LCSYS.2020.3001875","volume":"5","author":"Y Gilpin","year":"2020","unstructured":"Gilpin, Y., Kurtz, V., Lin, H.: A smooth robustness measure of signal temporal logic for symbolic control. IEEE Control Syst. Lett. 5(1), 241\u2013246 (2020)","journal-title":"IEEE Control Syst. Lett."},{"issue":"5","key":"12_CR17","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1073\/pnas.17.5.315","volume":"17","author":"BO Koopman","year":"1931","unstructured":"Koopman, B.O.: Hamiltonian systems and transformation in Hilbert space. Proc. Natl. Acad. Sci. U.S.A. 17(5), 315\u2013318 (1931)","journal-title":"Proc. Natl. Acad. Sci. U.S.A."},{"key":"12_CR18","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/j.automatica.2018.03.046","volume":"93","author":"M Korda","year":"2018","unstructured":"Korda, M., Mezi\u0107, I.: Linear predictors for nonlinear dynamical systems: Koopman operator meets model predictive control. Automatica 93, 149\u2013160 (2018)","journal-title":"Automatica"},{"issue":"4","key":"12_CR19","doi-asserted-by":"publisher","first-page":"1429","DOI":"10.1109\/LCSYS.2020.3038640","volume":"5","author":"V Kurtz","year":"2020","unstructured":"Kurtz, V., Lin, H.: Trajectory optimization for high-dimensional nonlinear systems under STL specifications. IEEE Control Syst. Lett. 5(4), 1429\u20131434 (2020)","journal-title":"IEEE Control Syst. Lett."},{"key":"12_CR20","doi-asserted-by":"publisher","first-page":"1718","DOI":"10.1109\/LCSYS.2021.3132839","volume":"6","author":"V Kurtz","year":"2021","unstructured":"Kurtz, V., Lin, H.: A more scalable mixed-integer encoding for metric temporal logic. IEEE Control Syst. Lett. 6, 1718\u20131723 (2021)","journal-title":"IEEE Control Syst. Lett."},{"key":"12_CR21","doi-asserted-by":"publisher","first-page":"2635","DOI":"10.1109\/LCSYS.2022.3172857","volume":"6","author":"V Kurtz","year":"2022","unstructured":"Kurtz, V., Lin, H.: Mixed-integer programming for signal temporal logic with fewer binary variables. IEEE Control Syst. Lett. 6, 2635\u20132640 (2022)","journal-title":"IEEE Control Syst. Lett."},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Kutz, J.N., Brunton, S.L., Brunton, B.W., Proctor, J.L.: Dynamic Mode Decomposition: Data-Driven Modeling of Complex Systems. SIAM (2016)","DOI":"10.1137\/1.9781611974508"},{"issue":"6","key":"12_CR23","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1177\/02783649221082115","volume":"42","author":"K Leung","year":"2023","unstructured":"Leung, K., Ar\u00e9chiga, N., Pavone, M.: Backpropagation through signal temporal logic specifications: Infusing logical structure into gradient-based methods. Int. J. Robot. Res. 42(6), 356\u2013370 (2023)","journal-title":"Int. J. Robot. Res."},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Lew, E., et\u00a0al.: AutoKoopman: A toolbox for automated system identification via Koopman operator linearization. In: Proceedings of the International Symposium on Automated Technology for Verification and Analysis, pp. 237\u2013250 (2023)","DOI":"10.1007\/978-3-031-45332-8_12"},{"issue":"1","key":"12_CR25","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1109\/LCSYS.2018.2853182","volume":"3","author":"L Lindemann","year":"2018","unstructured":"Lindemann, L., Dimarogonas, D.V.: Control barrier functions for signal temporal logic tasks. IEEE Control Syst. Lett. 3(1), 96\u2013101 (2018)","journal-title":"IEEE Control Syst. Lett."},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Proceedings of the International Conference on Formal Modelling and Analysis of Timed Systems, pp. 152\u2013166 (2004)","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"Mathesen, L., Pedrielli, G., Fainekos, G.: Efficient optimization-based falsification of cyber-physical systems with multiple conjunctive requirements. In: Proceedings of the International Conference on Automation Science and Engineering, pp. 732\u2013737 (2021)","DOI":"10.1109\/CASE49439.2021.9551474"},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"Menghi, C., Nejati, S., Briand, L., Parache, Y.I.: Approximation-refinement testing of compute-intensive cyber-physical models: An approach based on system identification. In: Proceedings of the International Conference on Software Engineering, pp. 372\u2013384 (2020)","DOI":"10.1145\/3377811.3380370"},{"key":"12_CR29","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1146\/annurev-fluid-011212-140652","volume":"45","author":"I Mezi\u0107","year":"2013","unstructured":"Mezi\u0107, I.: Analysis of fluid flows via spectral properties of the Koopman operator. Annu. Rev. Fluid Mech. 45, 357\u2013378 (2013)","journal-title":"Annu. Rev. Fluid Mech."},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"Nghiem, T., et\u00a0al.: Monte-Carlo techniques for falsification of temporal properties of non-linear hybrid systems. In: Proceedings of the International Conference on Hybrid Systems: Computation and Control, pp. 211\u2013220 (2010)","DOI":"10.1145\/1755952.1755983"},{"key":"12_CR31","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1146\/annurev-control-071020-010108","volume":"4","author":"SE Otto","year":"2021","unstructured":"Otto, S.E., Rowley, C.W.: Koopman operators for estimation and control of dynamical systems. Ann. Rev. Control Robot. Auton. Syst. 4, 59\u201387 (2021)","journal-title":"Ann. Rev. Control Robot. Auton. Syst."},{"key":"12_CR32","doi-asserted-by":"crossref","unstructured":"Pant, Y.V., Abbas, H., Mangharam, R.: Smooth operator: Control using the smooth robustness of temporal logic. In: Proceedings of the International Conference on Control Technology and Applications. pp. 1235\u20131240 (2017)","DOI":"10.1109\/CCTA.2017.8062628"},{"issue":"1","key":"12_CR33","doi-asserted-by":"publisher","first-page":"909","DOI":"10.1137\/16M1062296","volume":"17","author":"JL Proctor","year":"2018","unstructured":"Proctor, J.L., Brunton, S.L., Kutz, J.N.: Generalizing Koopman theory to allow for inputs and control. SIAM J. Appl. Dyn. Syst. 17(1), 909\u2013930 (2018)","journal-title":"SIAM J. Appl. Dyn. Syst."},{"key":"12_CR34","doi-asserted-by":"crossref","unstructured":"Raman, V., et\u00a0al.: Model predictive control with signal temporal logic specifications. In: Proceedings of the International Conference on Decision and Control, pp. 81\u201387 (2014)","DOI":"10.1109\/CDC.2014.7039363"},{"key":"12_CR35","doi-asserted-by":"crossref","unstructured":"Raman, V., et\u00a0al.: Reactive synthesis from signal temporal logic specifications. In: Proceedings of the International Conference on Hybrid Systems: Computation and Control, pp. 239\u2013248 (2015)","DOI":"10.1145\/2728606.2728628"},{"key":"12_CR36","doi-asserted-by":"crossref","unstructured":"Saha, S., Julius, A.A.: An MILP approach for real-time optimal controller synthesis with metric temporal logic specifications. In: Proceedings of the American Control Conference, pp. 1105\u20131110 (2016)","DOI":"10.1109\/ACC.2016.7525063"},{"key":"12_CR37","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Fainekos, G.: Falsification of temporal properties of hybrid systems using the cross-entropy method. In: Proceedings of the International Conference on Hybrid Systems: Computation and Control, pp. 125\u2013134 (2012)","DOI":"10.1145\/2185632.2185653"},{"key":"12_CR38","doi-asserted-by":"crossref","unstructured":"Takayama, Y., Hashimoto, K., Ohtsuka, T.: Signal temporal logic meets convex-concave programming: A structure-exploiting SQP algorithm for STL specifications. In: Proceedings of the International Conference on Decision and Control, pp. 6855\u20136862 (2023)","DOI":"10.1109\/CDC49753.2023.10383605"},{"key":"12_CR39","doi-asserted-by":"crossref","unstructured":"Waga, M.: Falsification of cyber-physical systems with robustness-guided black-box checking. In: Proceedings of the International Conference on Hybrid Systems: Computation and Control (2020). Article No. 11","DOI":"10.1145\/3365365.3382193"},{"issue":"12","key":"12_CR40","doi-asserted-by":"publisher","first-page":"2823","DOI":"10.1109\/TSE.2020.2969178","volume":"47","author":"Y Yamagata","year":"2020","unstructured":"Yamagata, Y., et al.: Falsification of cyber-physical systems using deep reinforcement learning. IEEE Trans. Software Eng. 47(12), 2823\u20132840 (2020)","journal-title":"IEEE Trans. Software Eng."},{"issue":"3","key":"12_CR41","doi-asserted-by":"publisher","first-page":"1586","DOI":"10.1137\/18M1192329","volume":"18","author":"H Zhang","year":"2019","unstructured":"Zhang, H., Rowley, C.W., Deem, E.A., Cattafesta, L.N.: Online dynamic mode decomposition for time-varying systems. SIAM J. Appl. Dyn. Syst. 18(3), 1586\u20131609 (2019)","journal-title":"SIAM J. Appl. Dyn. Syst."},{"key":"12_CR42","doi-asserted-by":"crossref","unstructured":"Zhang, Z., et\u00a0al.: Effective hybrid system falsification using Monte Carlo tree search guided by QB-robustness. In: Proceedings of the International Conference on Computer Aided Verification, pp. 595\u2013618 (2021)","DOI":"10.1007\/978-3-030-81685-8_29"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-78750-8_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T10:08:32Z","timestamp":1769681312000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-78750-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031787492","9783031787508"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-78750-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"12 February 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kyoto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}