  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.
