Abstract 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.

We study connections among polynomials, differential equations, and streams over a field 𝕂, in terms of algebra and coalgebra. We first introduce the class of (F,G) - products on streams, those where the stream derivative of a product can be expressed as a polynomial function of the streams and their derivatives. Our first result is that, for every (F,G) -product, there is a canonical way to construct a transition function on polynomials such that the resulting unique final coalgebra morphism from polynomials into streams is the (unique) commutative 𝕂-algebra homomorphism—and vice versa. This implies that one can algebraically reason on streams via their polynomial representation. We apply this result to obtain an algebraic-geometric decision algorithm for polynomial stream equivalence, for an underlying generic (F,G) -product. Finally, we extend this algorithm to solve a more general problem: finding all valid polynomial equalities that fit in a user specified polynomial template.