Linearization, model reduction and reachability in nonlinear odes

In the analysis of nonlinear ordinary differential equations (odes), 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 odes 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.