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 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 constraint is transformed into constraint using Farkas lemma. The constraint is solved using a bit-vector decision procedure. We present preliminary experimental results that demonstrate the feasibility of our approach of solving the constraints generated from models of real-world hybrid systems.

• Type: Conference
• Year: 2008
• Where: CAV
• Authors: Sumit Gulwani, Ashish Tiwari
• Keywords: CAV 2008, Hardware, Hybrid Systems, Invariant Set, Verification Condition