Constructing invariants for hybrid systems

We present a new method for generating algebraic invariants of hybrid systems. The method reduces the invariant generation problem to a constraint solving problem using techniques from the theory of ideals over polynomial rings. Starting with a template invariant—a polynomial equality over the system variables with unknown coefficients—constraints are generated on the coefficients guaranteeing that the solutions are inductive invariants. To control the complexity of the constraint solving, several stronger conditions that imply inductiveness are proposed, thus allowing a trade-off between the complexity of the invariant generation process and the strength of the resulting invariants. This research was supported in part by NSF grants CCR-01-21403, CCR-02-20134 and CCR-02-09237, by ARO grant DAAD19-01-1-0723, by ARPA/AF contracts F33615-00-C-1693 and F33615-99-C-3014, and by NAVY/ONR contract N00014-03-1-0939.