Abstract Model Repair

DOI10.2168/LMCS-11(3:11)2015MaRDI QIDQ3196342zbMATH OpenOpenAlexFDO

Authors G. Chatzieleftheriou, Borzoo Bonakdarpour, Scott A. Smolka, Panagiotis Katsaros

Publication date 29 October 2015

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1506.06165

zbMATH Keywords

abstraction refinementmodel checkingmodel repair

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: Given a Kripke structure M and CTL formula $varphi$, where M does not satisfy $varphi$, the problem of Model Repair is to obtain a new model M' such that M' satisfies $varphi$. Moreover, the changes made to M to derive M' should be minimum 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 framework aims to repair Kripke Structure models based on a Kripke Modal Transition System abstraction and a 3-valued semantics for CTL. We introduce an abstract-model-repair algorithm for which we prove soundness and semi-completeness, and we study its complexity class. Moreover, a prototype implementation is presented to illustrate the practical utility of abstract-model-repair on an Automatic Door Opener system model and a model of the Andrew File System 1 protocol.

Recommendations

• Modeling of repairable systems
• scientific article; zbMATH DE number 1531972
• Abstract model repair for probabilistic systems
• Change-Preserving Model Repair
• A general minimal repair model

Cited in

(16)

• Abstract model repair for probabilistic systems
• A refinement repair algorithm based on refinement game for KMTS models
• Automatic addition of conflicting properties
• An automated system repair framework with signal temporal logic
• Two AGM-style characterizations of model repair
• The complexity of automated addition of fault-tolerance without explicit legitimate states
• On module-based abstraction and repair of behavioral programs
• Model repair for probabilistic systems
• Synthesis of large dynamic concurrent programs from dynamic specifications
• Rule-based graph repair
• The Complexity of Linear-Time Temporal Logic Model Repair
• Toward the revision of CTL models through Kripke modal transition systems
• Change-Preserving Model Repair
• Model and program repair via group actions
• Fast Automated Abstract Machine Repair Using Simultaneous Modifications and Refactoring
• Clock bound repair for timed systems

This page was built for publication: Abstract Model Repair

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3196342)