Constraint-based Approach for Analysis of Hybrid Systems
Abstract
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.