Hybridization Based CEGAR for Hybrid Automata with Affine Dynamics

Nima Roohi, Pavithra Prabhakar and Mahesh Viswanathan

We consider the problem of safety verification for hybrid sys- tems, whose continuous dynamics in each mode is affine, X ̇ = AX + b, and invariants and guards are specified using rectangular constraints. We present a counter-example guided abstraction refinement framework (CEGAR), which abstract these hybrid automata into simpler ones with rectangular inclusion dynamics, x ̇ ∈ I, where x is a variable and I is an interval in R. In contrast to existing CEGAR frameworks which consider discrete abstractions, our method provides highly efficient abstraction construction, though model-checking the abstract system is more expen- sive. Our CEGAR algorithm has been implemented in a prototype tool called HARE (Hybrid Abstraction-Refinement Engine), that makes calls to SpaceEx to validate abstract counterexamples. We analyze the perfor- mance of our tool against standard benchmark examples, and show that its performance is promising when compared to state-of-the-art safety verification tools, SpaceEx, PHAVer, SpaceEx AGAR, and HSolver.

22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2016
Download: BIB PS PDF