{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,20]],"date-time":"2026-02-20T07:23:49Z","timestamp":1771572229079,"version":"3.50.1"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031131844","type":"print"},{"value":"9783031131851","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,7]],"date-time":"2022-08-07T00:00:00Z","timestamp":1659830400000},"content-version":"vor","delay-in-days":218,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Koopman operator linearization approximates nonlinear systems of differential equations with higher-dimensional linear systems. For formal verification using reachability analysis, this is an attractive conversion, as highly scalable methods exist to compute reachable sets for linear systems. However, two main challenges are present with this approach, both of which are addressed in this work. First, the approximation must be sufficiently accurate for the result to be meaningful, which is controlled by the choice of<jats:italic>observable functions<\/jats:italic>during Koopman operator linearization. By using random Fourier features as observable functions, the process becomes more systematic than earlier work, while providing a higher-accuracy approximation. Second, although the higher-dimensional system is linear, simple convex initial sets in the original space can become complex non-convex initial sets in the linear system. We overcome this using a combination of Taylor model arithmetic and polynomial zonotope refinement. Compared with prior work, the result is more efficient, more systematic and more accurate.<\/jats:p>","DOI":"10.1007\/978-3-031-13185-1_24","type":"book-chapter","created":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T19:29:09Z","timestamp":1659814149000},"page":"490-510","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Reachability of\u00a0Koopman Linearized Systems Using Random Fourier Feature Observables and\u00a0Polynomial Zonotope Refinement"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4947-9553","authenticated-orcid":false,"given":"Stanley","family":"Bak","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0686-0365","authenticated-orcid":false,"given":"Sergiy","family":"Bogomolov","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9240-7999","authenticated-orcid":false,"given":"Brandon","family":"Hencey","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6017-7623","authenticated-orcid":false,"given":"Niklas","family":"Kochdumper","sequence":"additional","affiliation":[]},{"given":"Ethan","family":"Lew","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4726-8931","authenticated-orcid":false,"given":"Kostiantyn","family":"Potomkin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,7]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Althoff, M.: Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets. In: Proceedings of the International Conference on Hybrid Systems: Computation and Control, pp. 173\u2013182 (2013)","DOI":"10.1145\/2461328.2461358"},{"issue":"2","key":"24_CR2","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1109\/TAC.2019.2906432","volume":"65","author":"M Althoff","year":"2019","unstructured":"Althoff, M.: Reachability analysis of large linear systems with uncertain inputs in the Krylov subspace. Trans. Autom. Control 65(2), 477\u2013492 (2019)","journal-title":"Trans. Autom. Control"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Amini, A., et al.: Error bounds for Carleman linearization of general nonlinear systems. In: Proceedings of the International Conference on Control and its Applications, pp. 1\u20138 (2021)","DOI":"10.1137\/1.9781611976847.1"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"Bak, S., et al.: Numerical verification of affine systems with up to a billion dimensions. In: Proceedings of the International Conference on Hybrid Systems: Computation and Control, pp. 23\u201332 (2019)","DOI":"10.1145\/3302504.3311792"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Bak, S., et al.: 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":"24_CR6","doi-asserted-by":"crossref","unstructured":"Bogomolov, S., et al.: Reach set approximation through decomposition with low-dimensional sets and high-dimensional matrices. In: Proceedings of the International Conference on Hybrid Systems: Computation and Control, pp. 41\u201350 (2018)","DOI":"10.1145\/3178126.3178128"},{"key":"24_CR7","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/BF02546499","volume":"59","author":"T Carleman","year":"1932","unstructured":"Carleman, T.: Application de la th\u00e9orie des \u00e9quations int\u00e9grales lin\u00e9aires aux syst\u00e8mes d\u2019\u00e9quations diff\u00e9rentielles non lin\u00e9aires. Acta Math. 59, 63\u201387 (1932)","journal-title":"Acta Math."},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"Chen, X., et al.: Taylor model flowpipe construction for non-linear hybrid systems. In: Proceedings of the Real-Time Systems Symposium, pp. 183\u2013192 (2012)","DOI":"10.1109\/RTSS.2012.70"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"X Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258\u2013263. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_18"},{"issue":"3","key":"24_CR10","doi-asserted-by":"publisher","first-page":"1482","DOI":"10.1137\/17M115414X","volume":"41","author":"AM DeGennaro","year":"2019","unstructured":"DeGennaro, A.M., Urban, N.M.: Scalable extended dynamic mode decomposition using random kernel approximation. SIAM J. Sci. Comput. 41(3), 1482\u20131499 (2019)","journal-title":"SIAM J. Sci. Comput."},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"Duggirala, P.S., Viswanathan, M.: Parsimonious, simulation based verification of linear systems. In: Proceedings of the International Conference on Computer Aided Verification, pp. 477\u2013494 (2016)","DOI":"10.1007\/978-3-319-41528-4_26"},{"key":"24_CR12","unstructured":"Forets, M., Pouly, A.: Explicit error bounds for Carleman linearization. arXiv preprint arXiv:1711.02552 (2017)"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-030-89716-1_6","volume-title":"Reachability Problems","author":"M Forets","year":"2021","unstructured":"Forets, M., Schilling, C.: Reachability of weakly nonlinear systems using Carleman linearization. In: Bell, P.C., Totzke, P., Potapov, I. (eds.) RP 2021. LNCS, vol. 13035, pp. 85\u201399. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-89716-1_6"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Proceedings of the International Conference on Computer Aided Verification, pp. 379\u2013395 (2011)","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"Girard, A.: Reachability of uncertain linear systems using zonotopes. In: Proceedings of the International Conference on Hybrid Systems: Computation and Control, pp. 291\u2013305 (2005)","DOI":"10.1007\/978-3-540-31954-2_19"},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"Han, Y., et al.: Deep learning of Koopman representation for control. In: Proceedings of the International Conference on Decision and Control, pp. 1890\u20131895 (2020)","DOI":"10.1109\/CDC42340.2020.9304238"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Jaulin, L., Kieffer, M., Didrit, O., Walter, E.: Interval analysis. In: Applied Interval Analysis, pp. 11\u201343. Springer (2001)","DOI":"10.1007\/978-1-4471-0249-6_2"},{"issue":"4","key":"24_CR18","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1016\/j.patcog.2004.09.006","volume":"38","author":"DW Kim","year":"2005","unstructured":"Kim, D.W., et al.: Evaluation of the performance of clustering algorithms in kernel-induced feature space. Pattern Recogn. 38(4), 607\u2013611 (2005)","journal-title":"Pattern Recogn."},{"key":"24_CR19","doi-asserted-by":"publisher","DOI":"10.1002\/3527603603","volume-title":"Systems Biology in Practice: Concepts, Implementation and Application","author":"E Klipp","year":"2005","unstructured":"Klipp, E., et al.: Systems Biology in Practice: Concepts, Implementation and Application. Wiley, Hoboken (2005)"},{"issue":"9","key":"24_CR20","doi-asserted-by":"publisher","first-page":"4043","DOI":"10.1109\/TAC.2020.3024348","volume":"66","author":"N Kochdumper","year":"2021","unstructured":"Kochdumper, N., Althoff, M.: Sparse polynomial zonotopes: a novel set representation for reachability analysis. Trans. Autom. Control 66(9), 4043\u20134058 (2021)","journal-title":"Trans. Autom. Control"},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"Kochdumper, N., et al.: Utilizing dependencies to obtain subsets of reachable sets. In: Proceedings of the International Conference on Hybrid Systems: Computation and Control (2020)","DOI":"10.1145\/3365365.3382192"},{"issue":"5","key":"24_CR22","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":"24_CR23","doi-asserted-by":"crossref","unstructured":"Kurzhanski, A.B., Varaiya, P.: Ellipsoidal techniques for reachability analysis. In: Proceedings of the International Conference on Hybrid Systems: Computation and Control, pp. 202\u2013214 (2000)","DOI":"10.1007\/3-540-46430-1_19"},{"key":"24_CR24","doi-asserted-by":"crossref","unstructured":"Liu, J.P., et al.: Efficient quantum algorithm for dissipative nonlinear differential equations. Proc. Natl. Acad. Sci. U.S.A. 118(35), e2026805118 (2021)","DOI":"10.1073\/pnas.2026805118"},{"issue":"4","key":"24_CR25","first-page":"379","volume":"4","author":"K Makino","year":"2003","unstructured":"Makino, K., Berz, M.: Taylor models and other validated functional inclusion methods. Int. J. Pure Appl. Math. 4(4), 379\u2013456 (2003)","journal-title":"Int. J. Pure Appl. Math."},{"key":"24_CR26","series-title":"Lecture Notes in Control and Information Sciences","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-35713-9","volume-title":"The Koopman Operator in Systems and Control","year":"2020","unstructured":"Mauroy, A., Mezi\u0107, I., Susuki, Y. (eds.): The Koopman Operator in Systems and Control. LNCIS, vol. 484. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-35713-9"},{"issue":"7","key":"24_CR27","doi-asserted-by":"publisher","first-page":"947","DOI":"10.1109\/TAC.2005.851439","volume":"50","author":"IM Mitchell","year":"2005","unstructured":"Mitchell, I.M., et al.: A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games. Trans. Autom. Control 50(7), 947\u2013957 (2005)","journal-title":"Trans. Autom. Control"},{"key":"24_CR28","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. Annu. Rev. Control Robot. Auton. Syst. 4, 59\u201387 (2021)","journal-title":"Annu. Rev. Control Robot. Auton. Syst."},{"key":"24_CR29","unstructured":"Rahimi, A., Recht, B.: Random features for large-scale kernel machines. In: Proceedings of the International Conference on Neural Information Processing Systems, pp. 1177\u20131184 (2007)"},{"issue":"4\u20135","key":"24_CR30","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1016\/0020-7462(80)90024-4","volume":"15","author":"R Rand","year":"1980","unstructured":"Rand, R., Holmes, P.: Bifurcation of periodic motions in two weakly coupled Van der Pol oscillators. Int. J. Non-Linear Mech. 15(4\u20135), 387\u2013399 (1980)","journal-title":"Int. J. Non-Linear Mech."},{"key":"24_CR31","doi-asserted-by":"crossref","unstructured":"Rauh, A., et al.: Carleman linearization for control and for state and disturbance estimation of nonlinear dynamical processes. In: Proceedings of the International Conference on Methods and Models in Automation and Robotics, pp. 455\u2013460 (2009)","DOI":"10.3182\/20090819-3-PL-3002.00079"},{"issue":"5","key":"24_CR32","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/0375-9601(76)90101-8","volume":"57","author":"OE R\u00f6ssler","year":"1976","unstructured":"R\u00f6ssler, O.E.: An equation for continuous chaos. Phys. Lett. A 57(5), 397\u2013398 (1976)","journal-title":"Phys. Lett. A"},{"key":"24_CR33","unstructured":"Rudin, W.: Fourier Analysis on Groups. Courier Dover Publications, Mineola (2017)"},{"key":"24_CR34","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S.: Automatic abstraction of non-linear systems using change of bases transformations. In: Proceedings of the International Conference on Hybrid Systems: Computation and Control, pp. 143\u2013152 (2011)","DOI":"10.1145\/1967701.1967723"},{"key":"24_CR35","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/j.nahs.2015.08.006","volume":"19","author":"S Sankaranarayanan","year":"2016","unstructured":"Sankaranarayanan, S.: Change-of-bases abstractions for non-linear hybrid systems. Nonlinear Anal. Hybrid Syst. 19, 107\u2013133 (2016)","journal-title":"Nonlinear Anal. Hybrid Syst."},{"key":"24_CR36","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/4175.001.0001","volume-title":"Learning with Kernels: Support Vector Machines, Regularization, Optimization, and Beyond","author":"B Sch\u00f6lkopf","year":"2018","unstructured":"Sch\u00f6lkopf, B., Smola, A.J.: Learning with Kernels: Support Vector Machines, Regularization, Optimization, and Beyond. MIT Press, Cambridge (2018)"},{"issue":"1","key":"24_CR37","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1590\/S0101-82052007000100002","volume":"26","author":"J Sotomayor","year":"2007","unstructured":"Sotomayor, J., et al.: Bifurcation analysis of the Watt governor system. Comput. Appl. Math. 26(1), 19\u201344 (2007)","journal-title":"Comput. Appl. Math."},{"issue":"2","key":"24_CR38","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1109\/TIP.2006.888330","volume":"16","author":"H Takeda","year":"2007","unstructured":"Takeda, H., et al.: Kernel regression for image processing and reconstruction. Trans. Image Process. 16(2), 349\u2013366 (2007)","journal-title":"Trans. Image Process."},{"issue":"10","key":"24_CR39","doi-asserted-by":"publisher","first-page":"3780","DOI":"10.1109\/TGRS.2010.2049496","volume":"48","author":"D Tuia","year":"2010","unstructured":"Tuia, D., et al.: Learning relevant image features with multiple-kernel classification. Trans. Geosci. Remote Sens. 48(10), 3780\u20133791 (2010)","journal-title":"Trans. Geosci. Remote Sens."},{"key":"24_CR40","doi-asserted-by":"crossref","unstructured":"Wetzlinger, M., et al.: Adaptive parameter tuning for reachability analysis of linear systems. In: Proceedings of the International Conference on Decision and Control, pp. 5145\u20135152 (2020)","DOI":"10.1109\/CDC42340.2020.9304431"},{"issue":"6","key":"24_CR41","doi-asserted-by":"publisher","first-page":"1307","DOI":"10.1007\/s00332-015-9258-5","volume":"25","author":"MO Williams","year":"2015","unstructured":"Williams, M.O., et al.: A data-driven approximation of the Koopman operator: extending dynamic mode decomposition. J. Nonlinear Sci. 25(6), 1307\u20131346 (2015)","journal-title":"J. Nonlinear Sci."},{"issue":"2","key":"24_CR42","doi-asserted-by":"publisher","first-page":"247","DOI":"10.3934\/jcd.2015005","volume":"2","author":"MO Williams","year":"2015","unstructured":"Williams, M.O., et al.: A kernel-based method for data-driven Koopman spectral analysis. J. Comput. Dyn. 2(2), 247\u2013265 (2015)","journal-title":"J. Comput. Dyn."},{"key":"24_CR43","doi-asserted-by":"crossref","unstructured":"Yeung, E., et al.: Learning deep neural network representations for Koopman operators of nonlinear dynamical systems. In: Proceedings of the American Control Conference, pp. 4832\u20134839 (2019)","DOI":"10.23919\/ACC.2019.8815339"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13185-1_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,25]],"date-time":"2023-11-25T10:49:20Z","timestamp":1700909360000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13185-1_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131844","9783031131851"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13185-1_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"7 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"209","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.9","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9.7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}