Abstract model repair

George Chatzieleftheriou; Borzoo Bonakdarpour; Scott A. Smolka; Panagiotis Katsaros

doi:10.1007/978-3-642-28891-3_32

Abstract model repair

George Chatzieleftheriou
, Borzoo Bonakdarpour
, Scott A. Smolka
, Panagiotis Katsaros

Computer Science

Aristotle University of Thessaloniki
University of Waterloo

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

28 Scopus citations

Abstract

Given a Kripke structure M and CTL formula φ, where M | ≠ φ, the problem of Model Repair is to obtain a new model M′ such that M′ |= φ. Moreover, the changes made to M to derive M′ should be minimal with respect to all such M′. As in model checking, state explosion can make it virtually impossible to carry out model repair on models with infinite or even large state spaces. In this paper, we present a framework for model repair that uses abstraction refinement to tackle state explosion. Our model-repair framework is based on Kripke Structures, a 3-valued semantics for CTL, and Kripke Modal Transition Systems (KMTSs), and features an abstract-model-repair algorithm for KMTSs. Application to an Automatic Door Opener system is used to illustrate the practical utility of abstract model repair.

Original language	English
Title of host publication	NASA Formal Methods - 4th International Symposium, NFM 2012, Proceedings
Pages	341-355
Number of pages	15
DOIs	https://doi.org/10.1007/978-3-642-28891-3_32
State	Published - 2012
Event	4th NASA Formal Methods Symposium, NFM 2012 - Norfolk, VA, United States Duration: Apr 3 2012 → Apr 5 2012

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	7226 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	4th NASA Formal Methods Symposium, NFM 2012
Country/Territory	United States
City	Norfolk, VA
Period	04/3/12 → 04/5/12

Keywords

Abstraction Refinement
Model Checking
Model Repair

Access to Document

10.1007/978-3-642-28891-3_32

Cite this

Chatzieleftheriou, G., Bonakdarpour, B., Smolka, S. A., & Katsaros, P. (2012). Abstract model repair. In NASA Formal Methods - 4th International Symposium, NFM 2012, Proceedings (pp. 341-355). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7226 LNCS). https://doi.org/10.1007/978-3-642-28891-3_32

@inproceedings{97603de93896483794bdca07d6084458,

title = "Abstract model repair",

abstract = "Given a Kripke structure M and CTL formula φ, where M | ≠ φ, the problem of Model Repair is to obtain a new model M′ such that M′ |= φ. Moreover, the changes made to M to derive M′ should be minimal with respect to all such M′. As in model checking, state explosion can make it virtually impossible to carry out model repair on models with infinite or even large state spaces. In this paper, we present a framework for model repair that uses abstraction refinement to tackle state explosion. Our model-repair framework is based on Kripke Structures, a 3-valued semantics for CTL, and Kripke Modal Transition Systems (KMTSs), and features an abstract-model-repair algorithm for KMTSs. Application to an Automatic Door Opener system is used to illustrate the practical utility of abstract model repair.",

keywords = "Abstraction Refinement, Model Checking, Model Repair",

author = "George Chatzieleftheriou and Borzoo Bonakdarpour and Smolka, \{Scott A.\} and Panagiotis Katsaros",

year = "2012",

doi = "10.1007/978-3-642-28891-3\_32",

language = "English",

isbn = "9783642288906",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "341--355",

booktitle = "NASA Formal Methods - 4th International Symposium, NFM 2012, Proceedings",

note = "4th NASA Formal Methods Symposium, NFM 2012 ; Conference date: 03-04-2012 Through 05-04-2012",

}

Chatzieleftheriou, G, Bonakdarpour, B, Smolka, SA & Katsaros, P 2012, Abstract model repair. in NASA Formal Methods - 4th International Symposium, NFM 2012, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7226 LNCS, pp. 341-355, 4th NASA Formal Methods Symposium, NFM 2012, Norfolk, VA, United States, 04/3/12. https://doi.org/10.1007/978-3-642-28891-3_32

Abstract model repair. / Chatzieleftheriou, George; Bonakdarpour, Borzoo; Smolka, Scott A. et al.
NASA Formal Methods - 4th International Symposium, NFM 2012, Proceedings. 2012. p. 341-355 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7226 LNCS).

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

TY - GEN

T1 - Abstract model repair

AU - Chatzieleftheriou, George

AU - Bonakdarpour, Borzoo

AU - Smolka, Scott A.

AU - Katsaros, Panagiotis

PY - 2012

Y1 - 2012

N2 - Given a Kripke structure M and CTL formula φ, where M | ≠ φ, the problem of Model Repair is to obtain a new model M′ such that M′ |= φ. Moreover, the changes made to M to derive M′ should be minimal with respect to all such M′. As in model checking, state explosion can make it virtually impossible to carry out model repair on models with infinite or even large state spaces. In this paper, we present a framework for model repair that uses abstraction refinement to tackle state explosion. Our model-repair framework is based on Kripke Structures, a 3-valued semantics for CTL, and Kripke Modal Transition Systems (KMTSs), and features an abstract-model-repair algorithm for KMTSs. Application to an Automatic Door Opener system is used to illustrate the practical utility of abstract model repair.

AB - Given a Kripke structure M and CTL formula φ, where M | ≠ φ, the problem of Model Repair is to obtain a new model M′ such that M′ |= φ. Moreover, the changes made to M to derive M′ should be minimal with respect to all such M′. As in model checking, state explosion can make it virtually impossible to carry out model repair on models with infinite or even large state spaces. In this paper, we present a framework for model repair that uses abstraction refinement to tackle state explosion. Our model-repair framework is based on Kripke Structures, a 3-valued semantics for CTL, and Kripke Modal Transition Systems (KMTSs), and features an abstract-model-repair algorithm for KMTSs. Application to an Automatic Door Opener system is used to illustrate the practical utility of abstract model repair.

KW - Abstraction Refinement

KW - Model Checking

KW - Model Repair

UR - https://www.scopus.com/pages/publications/84859456526

U2 - 10.1007/978-3-642-28891-3_32

DO - 10.1007/978-3-642-28891-3_32

M3 - Conference contribution

AN - SCOPUS:84859456526

SN - 9783642288906

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 341

EP - 355

BT - NASA Formal Methods - 4th International Symposium, NFM 2012, Proceedings

T2 - 4th NASA Formal Methods Symposium, NFM 2012

Y2 - 3 April 2012 through 5 April 2012

ER -

Abstract model repair

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this