Refining abstractions of hybrid systems using counterexample fragments

Ansgar Fehnker; Edmund Clarke; Sumit Kumar Jha; Bruce Krogh

doi:10.1007/978-3-540-31954-2_16

Refining abstractions of hybrid systems using counterexample fragments

Ansgar Fehnker, Edmund Clarke, Sumit Kumar Jha, Bruce Krogh

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

28 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 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
Place of Publication	Berlin
Publisher	Springer, Springer Nature
Pages	242-257
Number of pages	16
ISBN (Print)	9783540251088, 3540251081
DOIs	https://doi.org/10.1007/978-3-540-31954-2_16
Publication status	Published - 2005
Externally published	Yes
Event	8th Workshop on Hybrid Systems: Computation and Control, HSCC 2005 - Zurich, Switzerland Duration: 9 Mar 2005 → 11 Mar 2005

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	3414
ISSN (Print)	0302-9743

Conference

Conference	8th Workshop on Hybrid Systems: Computation and Control, HSCC 2005
Country/Territory	Switzerland
City	Zurich
Period	9/03/05 → 11/03/05

Access to Document

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

Cite this

Fehnker, A., Clarke, E., Jha, S. K., & Krogh, B. (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, Springer Nature. https://doi.org/10.1007/978-3-540-31954-2_16

Fehnker, Ansgar ; Clarke, Edmund ; Jha, Sumit Kumar et al. / 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. Berlin : Springer, Springer Nature, 2005. pp. 242-257 (Lecture Notes in Computer Science).

@inproceedings{af625b9c63474fec9f27a3075c94cf51,

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 Edmund Clarke and Jha, {Sumit Kumar} and Bruce Krogh",

year = "2005",

doi = "10.1007/978-3-540-31954-2_16",

language = "English",

isbn = "9783540251088",

series = "Lecture Notes in Computer Science",

publisher = "Springer, Springer Nature",

pages = "242--257",

editor = "Manfred Morari and Lothar Thiele",

booktitle = "Hybrid Systems: Computation and Control",

address = "United States",

note = "8th Workshop on Hybrid Systems: Computation and Control, HSCC 2005 ; Conference date: 09-03-2005 Through 11-03-2005",

}

Fehnker, A, Clarke, E, Jha, SK & Krogh, B 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, Springer Nature, Berlin, pp. 242-257, 8th Workshop on Hybrid Systems: Computation and Control, HSCC 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; Jha, Sumit Kumar et al.
Hybrid Systems: Computation and Control: 8th International Workshop, HSCC 2005 Zurich, Switzerland, March 9-11, 2005, Proceedings. ed. / Manfred Morari; Lothar Thiele. Berlin: Springer, Springer Nature, 2005. p. 242-257 (Lecture Notes in Computer Science; Vol. 3414).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

TY - GEN

T1 - Refining abstractions of hybrid systems using counterexample fragments

AU - Fehnker, Ansgar

AU - Clarke, Edmund

AU - Jha, Sumit Kumar

AU - Krogh, Bruce

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 proceeding contribution

SN - 9783540251088

SN - 3540251081

T3 - Lecture Notes in Computer Science

SP - 242

EP - 257

BT - Hybrid Systems: Computation and Control

A2 - Morari, Manfred

A2 - Thiele, Lothar

PB - Springer, Springer Nature

CY - Berlin

T2 - 8th Workshop on Hybrid Systems: Computation and Control, HSCC 2005

Y2 - 9 March 2005 through 11 March 2005

ER -

Fehnker A, Clarke E, Jha SK, Krogh B. 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. Berlin: Springer, Springer Nature. 2005. p. 242-257. (Lecture Notes in Computer Science). doi: 10.1007/978-3-540-31954-2_16

Refining abstractions of hybrid systems using counterexample fragments

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this