Refining Abstractions of Hybrid Systems Using Counterexample Fragments

Ansgar Fehnker, Edmund M. Clarke, Sumit Kumar Jha, Bruce H. Krogh

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

18 Citations (Scopus)

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 languageEnglish
Title of host publicationHybrid Systems: Computation and Control
Subtitle of host publication8th International Workshop, HSCC 2005, Zurich, Switzerland, March 9-11, 2005. Proceedings
EditorsManfred Morari, Lothar Thiele
PublisherSpringer
Pages242-257
Number of pages16
ISBN (Electronic)978-3-540-31954-2
ISBN (Print)978-3-540-25108-8
DOIs
Publication statusPublished - 2005
Externally publishedYes
Event8th International Workshop on Hybrid Systems: Computation and Control 2005 - ETH, Zurich, Switzerland
Duration: 9 Mar 200511 Mar 2005
Conference number: 8

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume3414

Conference

Conference8th International Workshop on Hybrid Systems: Computation and Control 2005
Abbreviated titleHSCC 2005
CountrySwitzerland
CityZurich
Period9/03/0511/03/05

Fingerprint

Hybrid systems
Refining
Directed graphs

Cite this

Fehnker, A., Clarke, E. M., Jha, S. K., & Krogh, B. H. (2005). Refining Abstractions of Hybrid Systems Using Counterexample Fragments. In M. Morari, & L. Thiele (Eds.), Hybrid Systems: Computation and Control: 8th International Workshop, HSCC 2005, Zurich, Switzerland, March 9-11, 2005. Proceedings (pp. 242-257). (Lecture Notes in Computer Science; Vol. 3414). Springer. https://doi.org/10.1007/978-3-540-31954-2_16
Fehnker, Ansgar ; Clarke, Edmund M. ; Jha, Sumit Kumar ; Krogh, Bruce H. / Refining Abstractions of Hybrid Systems Using Counterexample Fragments. Hybrid Systems: Computation and Control: 8th International Workshop, HSCC 2005, Zurich, Switzerland, March 9-11, 2005. Proceedings. editor / Manfred Morari ; Lothar Thiele. Springer, 2005. pp. 242-257 (Lecture Notes in Computer Science).
@inproceedings{beeaccedeb524d82bbf0f1424ff4c4f0,
title = "Refining Abstractions of Hybrid Systems Using Counterexample Fragments",
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.",
author = "Ansgar Fehnker and Clarke, {Edmund M.} and Jha, {Sumit Kumar} and Krogh, {Bruce H.}",
year = "2005",
doi = "10.1007/978-3-540-31954-2_16",
language = "English",
isbn = "978-3-540-25108-8",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "242--257",
editor = "Manfred Morari and Lothar Thiele",
booktitle = "Hybrid Systems: Computation and Control",

}

Fehnker, A, Clarke, EM, Jha, SK & Krogh, BH 2005, Refining Abstractions of Hybrid Systems Using Counterexample Fragments. in M Morari & L Thiele (eds), Hybrid Systems: Computation and Control: 8th International Workshop, HSCC 2005, Zurich, Switzerland, March 9-11, 2005. Proceedings. Lecture Notes in Computer Science, vol. 3414, Springer, pp. 242-257, 8th International Workshop on Hybrid Systems: Computation and Control 2005, Zurich, Switzerland, 9/03/05. https://doi.org/10.1007/978-3-540-31954-2_16

Refining Abstractions of Hybrid Systems Using Counterexample Fragments. / Fehnker, Ansgar; Clarke, Edmund M.; Jha, Sumit Kumar; Krogh, Bruce H.

Hybrid Systems: Computation and Control: 8th International Workshop, HSCC 2005, Zurich, Switzerland, March 9-11, 2005. Proceedings. ed. / Manfred Morari; Lothar Thiele. Springer, 2005. p. 242-257 (Lecture Notes in Computer Science; Vol. 3414).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Refining Abstractions of Hybrid Systems Using Counterexample Fragments

AU - Fehnker, Ansgar

AU - Clarke, Edmund M.

AU - Jha, Sumit Kumar

AU - Krogh, Bruce H.

PY - 2005

Y1 - 2005

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-540-31954-2_16

DO - 10.1007/978-3-540-31954-2_16

M3 - Conference contribution

SN - 978-3-540-25108-8

T3 - Lecture Notes in Computer Science

SP - 242

EP - 257

BT - Hybrid Systems: Computation and Control

A2 - Morari, Manfred

A2 - Thiele, Lothar

PB - Springer

ER -

Fehnker A, Clarke EM, Jha SK, Krogh BH. Refining Abstractions of Hybrid Systems Using Counterexample Fragments. In Morari M, Thiele L, editors, Hybrid Systems: Computation and Control: 8th International Workshop, HSCC 2005, Zurich, Switzerland, March 9-11, 2005. Proceedings. Springer. 2005. p. 242-257. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-540-31954-2_16