Abstract
Counterexample guided abstraction refinement, a powerful technique for verifying properties of discrete-state systems, has been extended recently to hybrid systems verification. Unlike in discrete systems, however, establishing the successor relation for hybrid systems can be a fairly expensive step since it requires evaluation and over-approximation of the continuous dynamics. It has been observed that it is often sufficient to consider fragments of counterexamples rather than complete counterexamples. In this paper we further develop the idea of fragments. We extend the notion of cut sets in directed graphs to cutting sets of fragments in abstractions. Cutting sets of fragments are then used to guide the abstraction refinement in order to prove safety properties for hybrid systems.
Original language | English |
---|---|
Title of host publication | Hybrid Systems: Computation and Control |
Subtitle of host publication | 8th International Workshop, HSCC 2005, Zurich, Switzerland, March 9-11, 2005. Proceedings |
Editors | Manfred Morari, Lothar Thiele |
Publisher | Springer |
Pages | 242-257 |
Number of pages | 16 |
ISBN (Electronic) | 978-3-540-31954-2 |
ISBN (Print) | 978-3-540-25108-8 |
DOIs | |
Publication status | Published - 2005 |
Externally published | Yes |
Event | 8th International Workshop on Hybrid Systems: Computation and Control 2005 - ETH, Zurich, Switzerland Duration: 9 Mar 2005 → 11 Mar 2005 Conference number: 8 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 3414 |
Conference
Conference | 8th International Workshop on Hybrid Systems: Computation and Control 2005 |
---|---|
Abbreviated title | HSCC 2005 |
Country/Territory | Switzerland |
City | Zurich |
Period | 9/03/05 → 11/03/05 |