Constraint-Based Approach for Analysis of Hybrid Systems

This paper presents a constraint-based technique for discovering a rich class of inductive invariants (boolean combinations of polynomial inequalities of bounded degree) for verification of hybrid systems. The key idea is to introduce a template for the unknown invariants and then translate the verification condition into an $\exists \forall$ constraint, where the template unknowns are existentially quantified and state variables are universally quantified. The verification condition for continuous dynamics encodes that the system does not exit the invariant set from any point on the boundary of the invariant set. The $\exists\forall$ constraint is transformed into $\exists$ constraint using Farkas lemma. The $\exists$ constraint is solved using a bit-vector decision procedure. We present preliminary experimental results that demonstrate the feasibility of our approach of solving the $\exists \forall$ constraints generated from models of real-world hybrid systems.