PT Unknown
AU Mari, F
   Tronci, E
TI CEGAR Based Bounded Model Checking of Discrete Time Hybrid Systems
SE Hybrid Systems: Computation and Control (HSCC 2007)
PY 2007
BP 399
EP 412
VL 4416
DI 10.1007/978-3-540-71493-4_32
DE Model Checking; Abstraction; CEGAR; SAT; Hybrid Systems; DTHS
AB Many hybrid systems can be conveniently modeled as Piecewise Affine Discrete Time Hybrid Systems PA-DTHS. As well known Bounded Model Checking (BMC) for such systems comes down to solve a Mixed Integer Linear Programming (MILP) feasibility problem. We present a SAT based BMC algorithm for automatic verification of PA-DTHSs. Using Counterexample Guided Abstraction Refinement (CEGAR) our algorithm gradually transforms a PA-DTHS verification problem into larger and larger SAT problems. Our experimental results show that our approach can handle PA-DTHSs that are more then 50 times larger than those that can be handled using a MILP solver.
ER