Abstract Model Repair

DOI10.2168/LMCS-11(3:11)2015zbMATH Open1448.68292arXiv1506.06165OpenAlexW2395626435MaRDI QIDQ3196342FDOQ3196342

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

Publication date: 29 October 2015

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

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.

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

zbMATH Keywords

model checkingabstraction refinementmodel repair

Mathematics Subject Classification ID

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

Cited In (7)

• Fast Automated Abstract Machine Repair Using Simultaneous Modifications and Refactoring
• Model and program repair via group actions
• The Complexity of Linear-Time Temporal Logic Model Repair
• Change-Preserving Model Repair
• Synthesis of large dynamic concurrent programs from dynamic specifications
• Two AGM-style characterizations of model repair
• Abstract model repair for probabilistic systems

   Recommendations

• Modeling of repairable systems 👍 👎
• Title not available (Why is that?) 👍 👎
• Abstract model repair for probabilistic systems 👍 👎
• Change-Preserving Model Repair 👍 👎
• A general minimal repair model 👍 👎

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)