TY  - CONF
AU  - Mari, Federico
AU  - Tronci, Enrico
ED  - Bemporad, A.
ED  - Bicchi, A.
ED  - Buttazzo, G.C.
PY  - 2007
DA  - 2007//
TI  - CEGAR Based Bounded Model Checking of Discrete Time Hybrid Systems
BT  - Hybrid Systems: Computation and Control (HSCC 2007)
T3  - Lecture Notes in Computer Science
SP  - 399
EP  - 412
VL  - 4416
PB  - Springer
KW  - Model Checking
KW  - Abstraction
KW  - CEGAR
KW  - SAT
KW  - Hybrid Systems
KW  - 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.
L1  - http://mclab.di.uniroma1.it/publications/papers/papers/Mari2007.pdf
UR  - https://doi.org/10.1007/978-3-540-71493-4_32
DO  - 10.1007/978-3-540-71493-4_32
N1  - exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=92), last updated on Thu, 22 Nov 2012 14:59:18 +0100
ID  - Mari+Tronci2007
ER  -