{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T15:33:17Z","timestamp":1759332797348,"version":"build-2065373602"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T00:00:00Z","timestamp":1748044800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T00:00:00Z","timestamp":1748044800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100004434","name":"Universit\u00e0 degli Studi di Firenze","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100004434","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2025,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>In the analysis of nonlinear ordinary differential equations (<jats:sc>ode<\/jats:sc>s), linear and Taylor approximations are fundamental tools. Such approximations are generally accurate only in a local sense, that is near a given expansion point in space or time. We study conditions and methods to compute linear approximations of nonlinear <jats:sc>ode<\/jats:sc>s that can be used to compute accurate reachability information also non locally. Relying on Carleman linearization and Krylov projection, our method yields a small, hence tractable linear system that is shown to produce accurate approximate solutions, under suitable stability conditions. In the general, possibly non stable case, we provide an algorithm that, given an initial set and a finite time horizon, builds a tight overapproximation of the reachable states at specified times. Experiments conducted with a proof-of-concept implementation have given encouraging results. We also establish a formal relation between our approach and Koopman approximation, a well-known framework for the analysis of nonlinear systems.<\/jats:p>","DOI":"10.1007\/s10703-025-00477-2","type":"journal-article","created":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T00:51:35Z","timestamp":1748047895000},"page":"419-454","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Linearization, model reduction and reachability in nonlinear odes"],"prefix":"10.1007","volume":"66","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1972-7491","authenticated-orcid":false,"given":"Michele","family":"Boreale","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luisa","family":"Collodi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,24]]},"reference":[{"doi-asserted-by":"publisher","unstructured":"Althoff M (2013) Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets. Proceedings of the 16th international conference on Hybrid systems: computation and control (HSCC\u201913), pp. 173-182, ACM. https:\/\/doi.org\/10.1145\/2461328.2461358","key":"477_CR1","DOI":"10.1145\/2461328.2461358"},{"unstructured":"Althoff M (2015) An introduction to CORA 2015. In Proc. of the Workshop on Applied Verification for Continuous and Hybrid Systems, pages 120-151","key":"477_CR2"},{"issue":"1","key":"477_CR3","doi-asserted-by":"publisher","first-page":"2021","DOI":"10.1146\/annurev-control-071420-081941","volume":"4","author":"M Althoff","year":"2021","unstructured":"Althoff M, Frehse G, Girard A (2021) Set propagation techniques for reachability analysis. Annual Rev Control Robot Auton Syst Annual Rev 4(1):2021. https:\/\/doi.org\/10.1146\/annurev-control-071420-081941. arXiv:hal-0304.8155","journal-title":"Annual Rev Control Robot Auton Syst Annual Rev"},{"doi-asserted-by":"crossref","unstructured":"Amini A, Sun Q, Motee N (2021) Error bounds for carleman linearization of general nonlinear systems. In 2021 Proceedings of the Conference on Control and its Applications, SIAM","key":"477_CR4","DOI":"10.1137\/1.9781611976847.1"},{"key":"477_CR5","first-page":"490","volume":"2022","author":"S Bak","year":"2022","unstructured":"Bak S, Bogomolov S, Hencey B, Kochdumper N, Lew E, Potomkin K (2022) Reachability of Koopman linearized systems using random fourier feature observables and polynomial zonotope refinement. Proc of CAV 2022:490\u2013510","journal-title":"Proc of CAV"},{"key":"477_CR6","volume-title":"Generalized inverses: theory and applications","author":"A Ben-Israel","year":"1974","unstructured":"Ben-Israel A, Greville T (1974) Generalized inverses: theory and applications. Wiley, New York, USA"},{"issue":"4","key":"477_CR7","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1090\/qam\/144472","volume":"20","author":"R Bellman","year":"1963","unstructured":"Bellman R, Richardson JM (1963) On some questions arising in the approximate solution of nonlinear differential equations. Q Appl Math 20(4):333\u2013339","journal-title":"Q Appl Math"},{"doi-asserted-by":"crossref","unstructured":"Boreale M (2018) Algorithms for exact and approximate linear abstractions of polynomial continuous systems. Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC\u201918, ACM","key":"477_CR8","DOI":"10.1145\/3178126.3178137"},{"doi-asserted-by":"crossref","unstructured":"Boreale M (2019) Algebra, coalgebra, and minimization in polynomial differential equations. Log Methods Comput Sci. 15(1)","key":"477_CR9","DOI":"10.23638\/LMCS-15(1:14)2019"},{"key":"477_CR10","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102441","volume":"193","author":"M Boreale","year":"2020","unstructured":"Boreale M (2020) Complete algorithms for algebraic strongest postconditions and weakest preconditions in polynomial odes. Sci Comput Program 193:102441","journal-title":"Sci Comput Program"},{"issue":"Part","key":"477_CR11","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2021.104860","volume":"285","author":"M Boreale","year":"2022","unstructured":"Boreale M (2022) Automatic pre- and postconditions for partial differential equations. Inf Comput 285(Part):104860","journal-title":"Inf Comput"},{"doi-asserted-by":"crossref","unstructured":"Boreale M, Collodi L (2022) Linearization, model reduction and reachability in nonlinear odes. Reachability Problems 2022 (RP22). LNCS 13608: 49-66, Springer","key":"477_CR12","DOI":"10.1007\/978-3-031-19135-0_4"},{"unstructured":"Chen X (2015) Reachability analysis of non-linear hybrid systems using Taylor models. Ph.D. thesis, RWTH Aachen University","key":"477_CR13"},{"doi-asserted-by":"crossref","unstructured":"Chen X, Abraham E, Sankaranarayanan S (2012) Taylor Model Flowpipe Construction for Non-linear Hybrid Systems. In Real-Time Systems Symposium (RTSS), pp. 183-192, IEEE","key":"477_CR14","DOI":"10.1109\/RTSS.2012.70"},{"doi-asserted-by":"crossref","unstructured":"Chen X, Abraham E, Sankaranarayanan S (2013) Flow$$*$$: an analyzer for non-linear hybrid systems. In Computer Aided Verification (CAV), LNCS 8044, pp. 258-263, Springer","key":"477_CR15","DOI":"10.1007\/978-3-642-39799-8_18"},{"unstructured":"Chen X, Abraham E, Sankaranarayanan S. Flow$$*$$ benchmarks. https:\/\/flowstar.org\/benchmarks\/","key":"477_CR16"},{"key":"477_CR17","volume-title":"Ordinary Differential Equations with Applications, 2\/e. Texts in Applied Mathematics","author":"C Chicone","year":"2006","unstructured":"Chicone C (2006) Ordinary Differential Equations with Applications, 2\/e. Texts in Applied Mathematics. Springer-Verlag, Berlin"},{"issue":"1","key":"477_CR18","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1109\/TAC.2002.806655","volume":"48","author":"A Chutinan","year":"2003","unstructured":"Chutinan A, Krogh BH (2003) Computational techniques for hybrid system verification. IEEE Trans Autom Control 48(1):64\u201375","journal-title":"IEEE Trans Autom Control"},{"unstructured":"Forets M, Pouly A (2017) Explicit error bounds for Carleman linearization. arXiv:1711.02552","key":"477_CR19"},{"key":"477_CR20","first-page":"85","volume":"13035","author":"M Forets","year":"2021","unstructured":"Forets M, Schilling C (2021) Reachability of weakly nonlinear systems using Carleman linearization. Proc. of RP 2021, LNCS 13035:85\u201399","journal-title":"Proc. of RP 2021, LNCS"},{"unstructured":"Goldsztejn A, Neumaier A (2009) On the exponentiation of interval matrices. arXiv:hal-0041.1330v1","key":"477_CR21"},{"key":"477_CR22","first-page":"2014","volume":"3571\u20133578","author":"E Goubault","year":"2014","unstructured":"Goubault E, Jourdan J-H, Putot S, Sankaranarayanan S (2014) Finding non-polynomial positive invariants and lyapunov functions for polynomial systems through Darboux polynomials. ACC 3571\u20133578:2014","journal-title":"ACC"},{"doi-asserted-by":"publisher","unstructured":"Jungers R M, Tabuada P (2019) Non-local linearization of nonlinear differential equations via polyflows. 2019 American Control Conference (ACC), pp. 1-6, https:\/\/doi.org\/10.23919\/ACC.2019.8814337","key":"477_CR23","DOI":"10.23919\/ACC.2019.8814337"},{"key":"477_CR24","volume-title":"Nonlinear systems, 3\/e","author":"H Khalil","year":"2002","unstructured":"Khalil H (2002) Nonlinear systems, 3\/e. Prentice-Hall, New Jersey"},{"key":"477_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8-17","volume-title":"Computer aided verification CAV 2013","author":"H Kong","year":"2013","unstructured":"Kong H, He F, Song X, Hung W, Gu M (2013) Exponential-condition-based barrier certificate generation for safety verification of hybrid systems. In: Sharygina N, Veith H (eds) Computer aided verification CAV 2013. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-642-39799-8-17"},{"key":"477_CR26","doi-asserted-by":"publisher","DOI":"10.1142\/1347","volume-title":"Nonlinear dynamical systems and Carleman linearization","author":"K Kowalski","year":"1991","unstructured":"Kowalski K, Steeb W-H (1991) Nonlinear dynamical systems and Carleman linearization. World Scientific, Singapore"},{"doi-asserted-by":"publisher","unstructured":"Makino K, Berz M (2009) Rigorous integration of flows and ODEs using Taylor models. In Proc. of Symbolic-Numeric Computation, pages 79\u201384, ACM, https:\/\/doi.org\/10.1145\/1577190.1577206","key":"477_CR27","DOI":"10.1145\/1577190.1577206"},{"issue":"11","key":"477_CR28","doi-asserted-by":"publisher","first-page":"3356","DOI":"10.1109\/TAC.2016.2518918","volume":"61","author":"A Mauroy","year":"2016","unstructured":"Mauroy A, Mezic I (2016) Global stability analysis using the eigenfunctions of the Koopman operator. IEEE Trans Automat Control 61(11):3356\u20133369. https:\/\/doi.org\/10.1109\/TAC.2016.2518918","journal-title":"IEEE Trans Automat Control"},{"volume-title":"The Koopman operator in systems and control: concepts, methodologies, and applications","year":"2020","unstructured":"Mauroy A, Mezic I, Susuki Y (eds) (2020) The Koopman operator in systems and control: concepts, methodologies, and applications. Springer, Berlin","key":"477_CR29"},{"key":"477_CR30","doi-asserted-by":"publisher","first-page":"947","DOI":"10.1109\/TAC.2005.851439","volume":"50","author":"IM Mitchell","year":"2005","unstructured":"Mitchell IM, Bayen AM, Tomlin CJ (2005) A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games. IEEE Trans Autom Control 50:947\u2013957","journal-title":"IEEE Trans Autom Control"},{"key":"477_CR31","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10703-016-0241-z","volume":"49","author":"S Mitsch","year":"2016","unstructured":"Mitsch S, Platzer A (2016) ModelPlex: verified runtime validation of verified cyber-physical system models. Form Methods Syst Des 49:33\u201374. https:\/\/doi.org\/10.1007\/s10703-016-0241-z","journal-title":"Form Methods Syst Des"},{"issue":"1","key":"477_CR32","first-page":"21","volume":"105","author":"NS Nedialkov","year":"1999","unstructured":"Nedialkov NS, Jackson KR, Corliss GF (1999) Validated solutions of initial value problems for ordinary differential equations. Appl Math Comput 105(1):21\u201368","journal-title":"Appl Math Comput"},{"doi-asserted-by":"crossref","unstructured":"Pippenger N (1976) On the evaluation of powers and related problems (preliminary version). In:Proceedings of the 17th Annual Symposium on Foundations of Computer Science (FOCS 1976), pages 258-263. Institute of Electrical and Electronics Engineers (IEEE) Computer Society, Washington, DC, USA","key":"477_CR33","DOI":"10.1109\/SFCS.1976.21"},{"doi-asserted-by":"crossref","unstructured":"Prajna S, Papachristodoulou A, Seiler P, Parrilo P (2005) SOSTOOLS and its control applications. Positive polynomials in control. Springer, pp 580\u2013580","key":"477_CR34","DOI":"10.1007\/10997703_14"},{"doi-asserted-by":"publisher","unstructured":"Prajna S (2003) Barrier certificates for nonlinear model validation. 42nd IEEE International Conference on Decision and Control (IEEE Cat. No.03CH37475), Vol.3, pp. 2884-2889. https:\/\/doi.org\/10.1109\/CDC.2003.1273063","key":"477_CR35","DOI":"10.1109\/CDC.2003.1273063"},{"key":"477_CR36","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898718003","volume-title":"Iterative methods for sparse linear systems","author":"Y Saad","year":"2003","unstructured":"Saad Y (2003) Iterative methods for sparse linear systems. SIAM, Philadelphia"},{"key":"477_CR37","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s10703-019-00337-w","volume":"54","author":"C S\u00e0nchez","year":"2019","unstructured":"S\u00e0nchez C, Schneider G, Ahrendt W et al (2019) A survey of challenges for runtime verification from advanced application domains (beyond software). Form Methods Syst Des 54:279\u2013335. https:\/\/doi.org\/10.1007\/s10703-019-00337-w","journal-title":"Form Methods Syst Des"},{"key":"477_CR38","first-page":"143","volume":"2011","author":"S Sankaranarayanan","year":"2011","unstructured":"Sankaranarayanan S (2011) Automatic abstraction of non-linear systems using change of bases transformations. 2011:143\u2013152","journal-title":"Automatic abstraction of non-linear systems using change of bases transformations."},{"unstructured":"Sankaranarayanan S (2012) Change-of-bases abstractions for non-linear systems. CoRR arXiv:1204.4347","key":"477_CR39"},{"doi-asserted-by":"crossref","unstructured":"Sch\u00fcrmann B, Kochdumper N, Althoff M (2018) Reachset model predictive control for disturbed nonlinear systems. Proceedings of the 57th IEEE Conference on Decision and Control, 3463\u20133470","key":"477_CR40","DOI":"10.1109\/CDC.2018.8619781"},{"key":"477_CR41","first-page":"1051","volume":"22","author":"B van der Pol","year":"1934","unstructured":"van der Pol B (1934) The nonlinear theory of electric oscillations. Proceed Inst Radio Eng 22:1051\u20131086","journal-title":"Proceed Inst Radio Eng"},{"key":"477_CR42","first-page":"600","volume":"2004","author":"A Tiwari","year":"2004","unstructured":"Tiwari A, Khanna G (2004) Nonlinear systems: approximating reach sets. HSCC 2004:600\u2013614","journal-title":"HSCC"},{"unstructured":"Wetzlinger M (2022) Personal communication","key":"477_CR43"},{"doi-asserted-by":"publisher","unstructured":"Xue B, Fr\u00e4nzle M, Zhan N (2018) Under-approximating reach sets for polynomial continuous systems. Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC\u201918, pp. 51\u201360, ACM. https:\/\/doi.org\/10.1145\/3178126.3178133","key":"477_CR44","DOI":"10.1145\/3178126.3178133"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00477-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-025-00477-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00477-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,30]],"date-time":"2025-09-30T15:26:43Z","timestamp":1759246003000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-025-00477-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,24]]},"references-count":44,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["477"],"URL":"https:\/\/doi.org\/10.1007\/s10703-025-00477-2","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2025,5,24]]},"assertion":[{"value":"25 April 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 March 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 May 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 July 2025","order":4,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Update","order":5,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The original online version of this article was revised: In this article the affiliation details were incorrectly given as \u20181. Dipartimento di Statistica, Informatica, Applicazioni \u201cG. Parenti\u201d, V.le Morgagni 65, 50134 Firenze, IT, Italy\u2019; 2. Universit\u00e0 di Firenze, Italy\u2019 but should have been \u2018Dipartimento di Statistica, Informatica, Applicazioni \u201cG. Parenti\u201d, Universit\u00e0 di Firenze, V.le Morgagni 65, 50134 Firenze FI, Italy\u2019.","order":6,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}}]}}