Record |
Author |
Mari, Federico; Tronci, Enrico |
Title |
CEGAR Based Bounded Model Checking of Discrete Time Hybrid Systems |
Type |
Conference Article |
Year |
2007 |
Publication |
Hybrid Systems: Computation and Control (HSCC 2007) |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
399-412 |
Keywords |
Model Checking, Abstraction, CEGAR, SAT, Hybrid Systems, DTHS |
Abstract |
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. |
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
Springer |
Place of Publication |
|
Editor |
Bemporad, A.; Bicchi, A.; Buttazzo, G.C. |
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
Series Volume |
4416 |
Series Issue |
|
Edition |
|
ISSN ![sorted by ISSN field, descending order (down)](img/sort_desc.gif) |
|
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
yes |
Call Number |
Sapienza @ mari @ MarTro07 |
Serial |
92 |
Permanent link to this record |