{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:35:38Z","timestamp":1753889738458,"version":"3.41.2"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2015,9,17]],"date-time":"2015-09-17T00:00:00Z","timestamp":1442448000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Given a Kripke structure M and CTL formula $\\varphi$, where M does not\nsatisfy $\\varphi$, the problem of Model Repair is to obtain a new model M' such\nthat M' satisfies $\\varphi$. Moreover, the changes made to M to derive M'\nshould be minimum with respect to all such M'. As in model checking, state\nexplosion can make it virtually impossible to carry out model repair on models\nwith infinite or even large state spaces. In this paper, we present a framework\nfor model repair that uses abstraction refinement to tackle state explosion.\nOur framework aims to repair Kripke Structure models based on a Kripke Modal\nTransition System abstraction and a 3-valued semantics for CTL. We introduce an\nabstract-model-repair algorithm for which we prove soundness and\nsemi-completeness, and we study its complexity class. Moreover, a prototype\nimplementation is presented to illustrate the practical utility of\nabstract-model-repair on an Automatic Door Opener system model and a model of\nthe Andrew File System 1 protocol.<\/jats:p>","DOI":"10.2168\/lmcs-11(3:11)2015","type":"journal-article","created":{"date-parts":[[2016,11,21]],"date-time":"2016-11-21T13:46:02Z","timestamp":1479735962000},"source":"Crossref","is-referenced-by-count":4,"title":["Abstract Model Repair"],"prefix":"10.46298","volume":"Volume 11, Issue 3","author":[{"given":"George","family":"Chatzieleftheriou","sequence":"first","affiliation":[]},{"given":"Borzoo","family":"Bonakdarpour","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4309-5295","authenticated-orcid":false,"given":"Panagiotis","family":"Katsaros","sequence":"additional","affiliation":[]},{"given":"Scott A.","family":"Smolka","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2015,9,17]]},"reference":[{"key":"1041:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1587\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1587\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:07:20Z","timestamp":1681243640000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1587"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9,17]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-11(3:11)2015","relation":{"is-same-as":[{"id-type":"arxiv","id":"1506.06165","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1506.06165","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2015,9,17]]},"article-number":"1587"}}