Generating polynomial invariants for hybrid systems

Abstract

We present a powerful computational method for automatically generating polynomial invariants of hybrid systems with linear continuous dynamics. When restricted to linear continuous dynamical systems, our method generates a set of polynomial equations (algebraic set) that is the best such over-approximation of the reach set. This shows that the set of algebraic invariants of a linear system is computable. The extension to hybrid systems is achieved using the abstract interpretation framework over the lattice defined by algebraic sets. Algebraic sets are represented using canonical Gröbner bases and the lattice operations are effectively computed via appropriate Gröbner basis manipulations. © Springer-Verlag Berlin Heidelberg 2005.