{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T15:26:58Z","timestamp":1772119618163,"version":"3.50.1"},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2025,3,18]],"date-time":"2025-03-18T00:00:00Z","timestamp":1742256000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,3,18]],"date-time":"2025-03-18T00:00:00Z","timestamp":1742256000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-19-1-0288"],"award-info":[{"award-number":["FA9550-19-1-0288"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA2386-17-1-4065"],"award-info":[{"award-number":["FA2386-17-1-4065"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-19-1-0288"],"award-info":[{"award-number":["FA9550-19-1-0288"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA2386-17-1-4065"],"award-info":[{"award-number":["FA2386-17-1-4065"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","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\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","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\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-19-C-0092"],"award-info":[{"award-number":["FA8750-19-C-0092"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2025,8]]},"DOI":"10.1007\/s10703-024-00464-z","type":"journal-article","created":{"date-parts":[[2025,3,18]],"date-time":"2025-03-18T13:09:23Z","timestamp":1742303363000},"page":"307-333","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Reachability of Koopman linearized systems using explicit kernel approximation and polynomial zonotope refinement"],"prefix":"10.1007","volume":"66","author":[{"given":"Stanley","family":"Bak","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergiy","family":"Bogomolov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Brandon","family":"Hencey","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Niklas","family":"Kochdumper","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ethan","family":"Lew","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kostiantyn","family":"Potomkin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,3,18]]},"reference":[{"key":"464_CR1","doi-asserted-by":"crossref","unstructured":"Girard A (2005) Reachability of uncertain linear systems using zonotopes. In: Proceedings of the international conference on hybrid systems: computation and control, pp 291\u2013305","DOI":"10.1007\/978-3-540-31954-2_19"},{"key":"464_CR2","doi-asserted-by":"crossref","unstructured":"Bogomolov S et al. (2018) 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","DOI":"10.1145\/3178126.3178128"},{"key":"464_CR3","doi-asserted-by":"crossref","unstructured":"Bak S et al. (2019) 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","DOI":"10.1145\/3302504.3311792"},{"key":"464_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-35713-9","volume-title":"The Koopman operator in systems and control: concepts, methodologies, and applications","author":"A Mauroy","year":"2020","unstructured":"Mauroy A et al (2020) The Koopman operator in systems and control: concepts, methodologies, and applications. Springer, Berlin"},{"key":"464_CR5","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1146\/annurev-control-071020-010108","volume":"4","author":"SE Otto","year":"2021","unstructured":"Otto SE, Rowley CW (2021) Koopman operators for estimation and control of dynamical systems. Ann Rev Control Robot Auton Syst 4:59\u201387","journal-title":"Ann Rev Control Robot Auton Syst"},{"key":"464_CR6","doi-asserted-by":"crossref","unstructured":"Rauh A et al. (2009) 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","DOI":"10.3182\/20090819-3-PL-3002.00079"},{"key":"464_CR7","doi-asserted-by":"crossref","unstructured":"Bak S et al. (2021) 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","DOI":"10.1016\/j.ifacol.2021.08.507"},{"key":"464_CR8","doi-asserted-by":"crossref","unstructured":"Bak S et al. (2022) 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","DOI":"10.1007\/978-3-031-13185-1_24"},{"key":"464_CR9","unstructured":"Rahimi A, Recht B (2007) Random features for large-scale kernel machines. In: Proceedings of the international conference on neural information processing systems, pp 1177\u20131184"},{"key":"464_CR10","unstructured":"Dao T, De Sa CM, R\u00e9 C (2017) Gaussian quadrature for kernel features. In: Proceedings of the international conference on neural information processing systems, pp 6107\u20136117"},{"key":"464_CR11","unstructured":"Li K, Principe JC (2019) No-trick (treat) kernel adaptive filtering using deterministic features. arXiv preprint arXiv:1912.04530"},{"key":"464_CR12","volume-title":"Learning with Kernels: support vector machines, regularization, optimization, and beyond","author":"B Sch\u00f6lkopf","year":"2018","unstructured":"Sch\u00f6lkopf B, Smola AJ (2018) Learning with Kernels: support vector machines, regularization, optimization, and beyond. MIT Press, Cambridge"},{"issue":"2","key":"464_CR13","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 (2007) Kernel regression for image processing and reconstruction. Trans Image Process 16(2):349\u2013366","journal-title":"Trans Image Process"},{"key":"464_CR14","doi-asserted-by":"crossref","unstructured":"Koopman BO (1931) Hamiltonian systems and transformation in Hilbert space. In: Proceedings National Academy Science USA 17(5):315\u2013318","DOI":"10.1073\/pnas.17.5.315"},{"issue":"6","key":"464_CR15","doi-asserted-by":"publisher","first-page":"1307","DOI":"10.1007\/s00332-015-9258-5","volume":"25","author":"MO Williams","year":"2015","unstructured":"Williams MO et al (2015) A data-driven approximation of the Koopman operator: extending dynamic mode decomposition. J Nonlinear Sci 25(6):1307\u20131346","journal-title":"J Nonlinear Sci"},{"key":"464_CR16","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/BF02546499","volume":"59","author":"T Carleman","year":"1932","unstructured":"Carleman T (1932) 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","journal-title":"Acta Math"},{"key":"464_CR17","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan S (2011) 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","DOI":"10.1145\/1967701.1967723"},{"key":"464_CR18","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 (2016) Change-of-bases abstractions for non-linear hybrid systems. Nonlinear Anal Hybrid Syst 19:107\u2013133","journal-title":"Nonlinear Anal Hybrid Syst"},{"key":"464_CR19","doi-asserted-by":"crossref","unstructured":"Han Y et al. (2020) Deep learning of Koopman representation for control. In: Proceedings of the international conference on decision and control, pp 1890\u20131895","DOI":"10.1109\/CDC42340.2020.9304238"},{"key":"464_CR20","doi-asserted-by":"crossref","unstructured":"Yeung E et al. (2019) Learning deep neural network representations for Koopman operators of nonlinear dynamical systems. In: Proceedings of the American control conference, pp 4832\u20134839","DOI":"10.23919\/ACC.2019.8815339"},{"key":"464_CR21","doi-asserted-by":"crossref","unstructured":"Liu J-P et al. (2021) Efficient quantum algorithm for dissipative nonlinear differential equations. In: Proceeding of the national academy of sciences of the United States of America 118(35)","DOI":"10.1073\/pnas.2026805118"},{"key":"464_CR22","unstructured":"Forets M, Pouly A (2017) Explicit error bounds for Carleman linearization. arXiv preprint arXiv:1711.02552"},{"key":"464_CR23","doi-asserted-by":"crossref","unstructured":"Amini A et al. (2021) Error bounds for Carleman linearization of general nonlinear systems. In: Proceedings of the international conference on control and its applications, pp 1\u20138","DOI":"10.1137\/1.9781611976847.1"},{"key":"464_CR24","doi-asserted-by":"crossref","unstructured":"Duggirala PS, Viswanathan M (2016) Parsimonious, simulation based verification of linear systems. In: Proceedings of the international conference on Computer aided verification, pp 477\u2013494","DOI":"10.1007\/978-3-319-41528-4_26"},{"key":"464_CR25","doi-asserted-by":"crossref","unstructured":"Kurzhanski AB, Varaiya P (2000) Ellipsoidal techniques for reachability analysis. In: Proceedings of the international conference on hybrid systems: computation and control, pp 202\u2013214","DOI":"10.1007\/3-540-46430-1_19"},{"issue":"2","key":"464_CR26","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1109\/TAC.2019.2906432","volume":"65","author":"M Althoff","year":"2019","unstructured":"Althoff M (2019) Reachability analysis of large linear systems with uncertain inputs in the Krylov subspace. Trans Autom Control 65(2):477\u2013492","journal-title":"Trans Autom Control"},{"key":"464_CR27","doi-asserted-by":"crossref","unstructured":"Chen X et al. (2012) Taylor model flowpipe construction for non-linear hybrid systems. In: Proceedings of the real-time systems symposium, pp 183\u2013192","DOI":"10.1109\/RTSS.2012.70"},{"key":"464_CR28","doi-asserted-by":"crossref","unstructured":"Althoff M (2013) 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","DOI":"10.1145\/2461328.2461358"},{"issue":"7","key":"464_CR29","doi-asserted-by":"publisher","first-page":"947","DOI":"10.1109\/TAC.2005.851439","volume":"50","author":"IM Mitchell","year":"2005","unstructured":"Mitchell IM et al (2005) A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games. Trans Autom Control 50(7):947\u2013957","journal-title":"Trans Autom Control"},{"key":"464_CR30","doi-asserted-by":"crossref","unstructured":"Kochdumper N, Bak S (2022) Conformant synthesis for Koopman operator linearized control systems. In: Proceedings of the international conference on decision and control, pp 7327\u20137332","DOI":"10.1109\/CDC51059.2022.9992324"},{"key":"464_CR31","doi-asserted-by":"crossref","unstructured":"Forets M, Schilling C (2021) Reachability of weakly nonlinear systems using Carleman linearization. In: Proceedings of the international conference on reachability problems, pp 85\u201399","DOI":"10.1007\/978-3-030-89716-1_6"},{"key":"464_CR32","volume-title":"Applied interval analysis","author":"L Jaulin","year":"2006","unstructured":"Jaulin L et al (2006) Applied interval analysis. Springer, Berlin"},{"issue":"4","key":"464_CR33","first-page":"379","volume":"4","author":"K Makino","year":"2003","unstructured":"Makino K, Berz M (2003) Taylor models and other validated functional inclusion methods. Int J Pure Appl Math 4(4):379\u2013456","journal-title":"Int J Pure Appl Math"},{"issue":"9","key":"464_CR34","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 (2021) Sparse polynomial zonotopes: a novel set representation for reachability analysis. Trans Autom Control 66(9):4043\u20134058","journal-title":"Trans Autom Control"},{"issue":"4","key":"464_CR35","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1016\/j.patcog.2004.09.006","volume":"38","author":"D-W Kim","year":"2005","unstructured":"Kim D-W et al (2005) Evaluation of the performance of clustering algorithms in kernel-induced feature space. Pattern Recognit 38(4):607\u2013611","journal-title":"Pattern Recognit"},{"issue":"10","key":"464_CR36","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 (2010) Learning relevant image features with multiple-kernel classification. Trans Geosci Remote Sens 48(10):3780\u20133791","journal-title":"Trans Geosci Remote Sens"},{"issue":"2","key":"464_CR37","doi-asserted-by":"publisher","first-page":"247","DOI":"10.3934\/jcd.2015005","volume":"2","author":"MO Williams","year":"2015","unstructured":"Williams MO et al (2015) A kernel-based method for data-driven Koopman spectral analysis. J Comput Dyn 2(2):247\u2013265","journal-title":"J Comput Dyn"},{"issue":"3","key":"464_CR38","doi-asserted-by":"publisher","first-page":"1482","DOI":"10.1137\/17M115414X","volume":"41","author":"AM DeGennaro","year":"2019","unstructured":"DeGennaro AM, Urban NM (2019) Scalable extended dynamic mode decomposition using random kernel approximation. SIAM J Sci Comput 41(3):1482\u20131499","journal-title":"SIAM J Sci Comput"},{"key":"464_CR39","volume-title":"Fourier analysis on groups","author":"W Rudin","year":"2017","unstructured":"Rudin W (2017) Fourier analysis on groups. Courier Dover Publications, Mineola"},{"key":"464_CR40","volume-title":"Theory and applications of gaussian quadrature methods","author":"N Kovvali","year":"2022","unstructured":"Kovvali N (2022) Theory and applications of gaussian quadrature methods. Springer, Berlin"},{"key":"464_CR41","volume-title":"Sparse grids and applications","author":"J Garcke","year":"2012","unstructured":"Garcke J, Griebel M (2012) Sparse grids and applications. Springer, Berlin"},{"key":"464_CR42","doi-asserted-by":"crossref","unstructured":"Frehse G et al. (2011) SpaceEx: scalable verification of hybrid systems. In: Proceedings of the international conference on computer aided verification, pp 379\u2013395","DOI":"10.1007\/978-3-642-22110-1_30"},{"issue":"12","key":"464_CR43","doi-asserted-by":"publisher","first-page":"7771","DOI":"10.1109\/TAC.2023.3292008","volume":"68","author":"M Wetzlinger","year":"2023","unstructured":"Wetzlinger M et al (2023) Fully automated verification of linear systems using inner-and outer-approximations of reachable sets. Trans Autom Control 68(12):7771\u20137786","journal-title":"Trans Autom Control"},{"issue":"7","key":"464_CR44","doi-asserted-by":"publisher","first-page":"3518","DOI":"10.1109\/TAC.2016.2615599","volume":"62","author":"B Xue","year":"2016","unstructured":"Xue B et al (2016) Reach-avoid verification for nonlinear systems based on boundary analysis. Trans Autom Control 62(7):3518\u20133523","journal-title":"Trans Autom Control"},{"key":"464_CR45","doi-asserted-by":"crossref","unstructured":"Kochdumper N et al. (2020) Utilizing dependencies to obtain subsets of reachable sets. In: Proceedings of the international conference on hybrid systems: computation and control. Article\u00a0No.\u00a01","DOI":"10.1145\/3365365.3382192"},{"issue":"9","key":"464_CR46","doi-asserted-by":"publisher","first-page":"2341","DOI":"10.1109\/TAC.2015.2491740","volume":"61","author":"M Ma\u00efga","year":"2015","unstructured":"Ma\u00efga M et al (2015) A comprehensive method for reachability analysis of uncertain nonlinear hybrid systems. Trans Autom Control 61(9):2341\u20132356","journal-title":"Trans Autom Control"},{"issue":"5","key":"464_CR47","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 OE (1976) An equation for continuous chaos. Phys Lett A 57(5):397\u2013398","journal-title":"Phys Lett A"},{"issue":"1","key":"464_CR48","first-page":"19","volume":"26","author":"J Sotomayor","year":"2007","unstructured":"Sotomayor J et al (2007) Bifurcation analysis of the Watt governor system. Comput Appl Math 26(1):19\u201344","journal-title":"Comput Appl Math"},{"issue":"4\u20135","key":"464_CR49","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 (1980) Bifurcation of periodic motions in two weakly coupled Van der Pol oscillators. Int J Non-Linear Mech 15(4\u20135):387\u2013399","journal-title":"Int J Non-Linear Mech"},{"key":"464_CR50","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 (2005) Systems biology in practice: concepts, implementation and application. John Wiley & Sons, Hoboken"},{"key":"464_CR51","doi-asserted-by":"crossref","unstructured":"Chen X et al. (2013) Flow*: an analyzer for non-linear hybrid systems. In: Proceedings of the international conference on computer-aided verification, pp 258\u2013263","DOI":"10.1007\/978-3-642-39799-8_18"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00464-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-024-00464-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00464-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,6]],"date-time":"2025-09-06T07:48:41Z","timestamp":1757144921000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-024-00464-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,18]]},"references-count":51,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,8]]}},"alternative-id":["464"],"URL":"https:\/\/doi.org\/10.1007\/s10703-024-00464-z","relation":{"has-preprint":[{"id-type":"doi","id":"10.21203\/rs.3.rs-3069543\/v1","asserted-by":"object"}]},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,3,18]]},"assertion":[{"value":"15 June 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 October 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 March 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"Not Applicable. We did no human and\/or animal studies.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethical approval"}}]}}