View Related Documents

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.
The research of the first author was partially supported by Spanish FPU grant ref. AP2002-3693 and the projects Maverish (MCYT TIC2001-2476-C03-01) and LogicTools (TIN2004-03382) funded by the Spanish Ministry of Education and Science. The second author was supported in part by the National Science Foundation under grants CCR-0311348 and CCR-ITR-0326540 and NASA Langley Research Center contract NAS1-00108 to Rannoch Corporation.

Fulltext Preview

Image of the first page of the fulltext document