Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems

Edmund M. Clarke, Ansgar Fehnker, Zhi Han, Bruce H. Krogh, Joël Ouaknine, Olaf Stursberg, Michael Theobald

Research output: Contribution to journalArticleAcademicpeer-review

121 Citations (Scopus)
9 Downloads (Pure)

Abstract

Hybrid dynamic systems include both continuous and discrete state variables. Properties of hybrid systems, which have an infinite state space, can often be verified using ordinary model checking together with a finite-state abstraction. Model checking can be inconclusive, however, in which case the abstraction must be refined. This paper presents a new procedure to perform this refinement operation for abstractions of hybrid systems. Following an approach originally developed for finite-state systems [11, 25], the refinement procedure constructs a new abstraction that eliminates a counterexample generated by the model checker. For hybrid systems, analysis of the counterexample requires the computation of sets of reachable states in the continuous state space. We show how such reachability computations with varying degrees of complexity can be used to refine hybrid system abstractions efficiently. Examples illustrate our counterexample-guided refinement procedure. Experimental results for a prototype implementation indicate significant advantages over existing methods.

Original languageEnglish
Pages (from-to)583-604
Number of pages22
JournalInternational journal of foundations of computer science
Volume14
Issue number4
DOIs
Publication statusPublished - 2003
Externally publishedYes

Fingerprint

Model checking
Hybrid systems
Dynamical systems
Systems analysis

Cite this

Clarke, Edmund M. ; Fehnker, Ansgar ; Han, Zhi ; Krogh, Bruce H. ; Ouaknine, Joël ; Stursberg, Olaf ; Theobald, Michael. / Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems. In: International journal of foundations of computer science. 2003 ; Vol. 14, No. 4. pp. 583-604.
@article{b92ee26368a947cc8aa7a09d041b57dd,
title = "Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems",
abstract = "Hybrid dynamic systems include both continuous and discrete state variables. Properties of hybrid systems, which have an infinite state space, can often be verified using ordinary model checking together with a finite-state abstraction. Model checking can be inconclusive, however, in which case the abstraction must be refined. This paper presents a new procedure to perform this refinement operation for abstractions of hybrid systems. Following an approach originally developed for finite-state systems [11, 25], the refinement procedure constructs a new abstraction that eliminates a counterexample generated by the model checker. For hybrid systems, analysis of the counterexample requires the computation of sets of reachable states in the continuous state space. We show how such reachability computations with varying degrees of complexity can be used to refine hybrid system abstractions efficiently. Examples illustrate our counterexample-guided refinement procedure. Experimental results for a prototype implementation indicate significant advantages over existing methods.",
author = "Clarke, {Edmund M.} and Ansgar Fehnker and Zhi Han and Krogh, {Bruce H.} and Jo{\"e}l Ouaknine and Olaf Stursberg and Michael Theobald",
year = "2003",
doi = "10.1142/S012905410300190X",
language = "English",
volume = "14",
pages = "583--604",
journal = "International journal of foundations of computer science",
issn = "0129-0541",
publisher = "World Scientific Publishing Co. Pte Ltd",
number = "4",

}

Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems. / Clarke, Edmund M.; Fehnker, Ansgar; Han, Zhi; Krogh, Bruce H.; Ouaknine, Joël; Stursberg, Olaf; Theobald, Michael.

In: International journal of foundations of computer science, Vol. 14, No. 4, 2003, p. 583-604.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems

AU - Clarke, Edmund M.

AU - Fehnker, Ansgar

AU - Han, Zhi

AU - Krogh, Bruce H.

AU - Ouaknine, Joël

AU - Stursberg, Olaf

AU - Theobald, Michael

PY - 2003

Y1 - 2003

N2 - Hybrid dynamic systems include both continuous and discrete state variables. Properties of hybrid systems, which have an infinite state space, can often be verified using ordinary model checking together with a finite-state abstraction. Model checking can be inconclusive, however, in which case the abstraction must be refined. This paper presents a new procedure to perform this refinement operation for abstractions of hybrid systems. Following an approach originally developed for finite-state systems [11, 25], the refinement procedure constructs a new abstraction that eliminates a counterexample generated by the model checker. For hybrid systems, analysis of the counterexample requires the computation of sets of reachable states in the continuous state space. We show how such reachability computations with varying degrees of complexity can be used to refine hybrid system abstractions efficiently. Examples illustrate our counterexample-guided refinement procedure. Experimental results for a prototype implementation indicate significant advantages over existing methods.

AB - Hybrid dynamic systems include both continuous and discrete state variables. Properties of hybrid systems, which have an infinite state space, can often be verified using ordinary model checking together with a finite-state abstraction. Model checking can be inconclusive, however, in which case the abstraction must be refined. This paper presents a new procedure to perform this refinement operation for abstractions of hybrid systems. Following an approach originally developed for finite-state systems [11, 25], the refinement procedure constructs a new abstraction that eliminates a counterexample generated by the model checker. For hybrid systems, analysis of the counterexample requires the computation of sets of reachable states in the continuous state space. We show how such reachability computations with varying degrees of complexity can be used to refine hybrid system abstractions efficiently. Examples illustrate our counterexample-guided refinement procedure. Experimental results for a prototype implementation indicate significant advantages over existing methods.

U2 - 10.1142/S012905410300190X

DO - 10.1142/S012905410300190X

M3 - Article

VL - 14

SP - 583

EP - 604

JO - International journal of foundations of computer science

JF - International journal of foundations of computer science

SN - 0129-0541

IS - 4

ER -