%0 Conference Proceedings
%T CEGAR Based Bounded Model Checking of Discrete Time Hybrid Systems
%A Mari, Federico
%A Tronci, Enrico
%Y Bemporad, A.
%Y Bicchi, A.
%Y Buttazzo, G.C.
%S Hybrid Systems: Computation and Control (HSCC 2007)
%S Lecture Notes in Computer Science
%D 2007
%V 4416
%I Springer
%F Mari+Tronci2007
%O exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=92), last updated on Thu, 22 Nov 2012 14:59:18 +0100
%X 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.
%K Model Checking
%K Abstraction
%K CEGAR
%K SAT
%K Hybrid Systems
%K DTHS
%R 10.1007/978-3-540-71493-4_32
%U http://mclab.di.uniroma1.it/publications/papers/papers/Mari2007.pdf
%U https://doi.org/10.1007/978-3-540-71493-4_32
%P 399-412