We present abstraction techniques that transform a given non-linear dynamical system into a linear system or an algebraic system described by polynomials of bounded degree, such that, invariant properties of the resulting abstraction can be used to infer invariants for the original system. The abstraction techniques rely on a change-of-basis transformation that associates each state variable of the abstract system with a function involving the state variables of the original system. We present conditions under which a given change of basis transformation for a non-linear system can define an abstraction. Furthermore, the techniques developed here apply to continuous systems defined by Ordinary Differential Equations (ODEs), discrete systems defined by transition systems and hybrid systems that combine continuous as well as discrete subsystems. The techniques presented here allow us to discover, given a non-linear system, if a change of bases transformation involving degree-bounded polynomials yielding an algebraic abstraction exists. If so, our technique yields the resulting abstract system, as well. This approach is further extended to search for a change of bases transformation that abstracts a given non-linear system into a system of linear differential inclusions. Our techniques enable the use of analysis techniques for linear systems to infer invariants for non-linear systems. We present preliminary evidence of the practical feasibility of our ideas using a prototype implementation.
Finally, our approach is closely related to that can be used to linearize a given differential equation with polynomial right-hand sides @cite_24 . The standard Carlemann embedding technique creates an infinite dimensional linear system, wherein, each dimension corresponds to a monomial or a basis polynomial. In practice, it is possible to create a linear approximation with known error bounds by truncating the monomial terms beyond a degree cutoff. Our approach for differential equation abstractions can be seen as a search for a finite submatrix'' inside the infinite matrix created by the Carleman linearization. The rows and columns of this submatrix correspond to monomials such that the derivative of each monomial in the submatrix is a linear combination of monomials that belong the submatrix. Note, however, that while Carleman embedding is defined using some basis for polynomials (usually power-products), our approach can derive transformations that may involve polynomials as opposed to just power-products.
@cite_24
1520892678
The Carleman linearization has become a new powerful tool in the study of nonlinear dynamical systems. Nevertheless, there is the general lack of familiarity with the Carleman embedding technique among those working in the field of nonlinear models. This book provides a systematic presentation of the Carleman linearization, its generalizations and applications. It also includes a review of existing alternative methods for linearization of nonlinear dynamical systems. There are probably no books covering such a wide spectrum of linearization algorithms. This book also gives a comprehensive introduction to the Kronecker product of matrices, whereas most books deal with it only superficially. The Kronecker product of matrices plays an important role in mathematics and in applications found in theoretical physics.