{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T05:04:13Z","timestamp":1769749453853,"version":"3.49.0"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2017,12,7]],"date-time":"2017-12-07T00:00:00Z","timestamp":1512604800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2018,3,31]]},"abstract":"<jats:p>\n            We consider the\n            <jats:italic>subtractive model repair problem<\/jats:italic>\n            : given a finite Kripke structure\n            <jats:italic>M<\/jats:italic>\n            and a CTL formula \u03b7, determine if\n            <jats:italic>M<\/jats:italic>\n            contains a substructure\n            <jats:italic>M<\/jats:italic>\n            <jats:sup>\u2032<\/jats:sup>\n            that satisfies \u03b7. Thus,\n            <jats:italic>M<\/jats:italic>\n            can be \u201crepaired\u201d to satisfy\n            <jats:italic>eta<\/jats:italic>\n            by deleting some transitions and states. We map an instance \u2329\n            <jats:italic>M<\/jats:italic>\n            ,\u03b7 \u232a of model repair to a Boolean formula\n            <jats:italic>repair<\/jats:italic>\n            (\n            <jats:italic>M<\/jats:italic>\n            ,\u03b7) such that \u2329\n            <jats:italic>M<\/jats:italic>\n            ,\u03b7 \u232a has a solution iff\n            <jats:italic>repair<\/jats:italic>\n            (\n            <jats:italic>M<\/jats:italic>\n            ,\u03b7) is satisfiable. Furthermore, a satisfying assignment determines which states and transitions must be removed from\n            <jats:italic>M<\/jats:italic>\n            to yield a model\n            <jats:italic>M<\/jats:italic>\n            <jats:sup>\u2032<\/jats:sup>\n            of \u03b7 Thus, we can use any SAT solver to repair Kripke structures. Using a complete SAT solver yields a complete algorithm: it always finds a repair if one exists. We also show that CTL model repair is NP-complete. We extend the basic repair method in three directions: (1) the use of abstraction mappings, that is, repair a structure abstracted from\n            <jats:italic>M<\/jats:italic>\n            and then concretize the resulting repair to obtain a repair of\n            <jats:italic>M<\/jats:italic>\n            , (2) repair concurrent Kripke structures and concurrent programs: we use the pairwise method of Attie and Emerson to represent and repair the behavior of a concurrent program, as a set of \u201cconcurrent Kripke structures\u201d, with only a quadratic increase in the size of the repair formula, and (3) repair hierarchical Kripke structures: we use a CTL formula to summarize the behavior of each \u201cbox,\u201d and CTL deduction to relate the box formula with the overall specification.\n          <\/jats:p>","DOI":"10.1145\/3147426","type":"journal-article","created":{"date-parts":[[2017,12,11]],"date-time":"2017-12-11T13:26:47Z","timestamp":1512998807000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Model and Program Repair via SAT Solving"],"prefix":"10.1145","volume":"17","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1989-0974","authenticated-orcid":false,"given":"Paul C.","family":"Attie","sequence":"first","affiliation":[{"name":"American University of Beirut, Beirut, Lebanon"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kinan Dak Al","family":"Bab","sequence":"additional","affiliation":[{"name":"American University of Beirut, Beirut, Lebanon"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mouhammad","family":"Sakr","sequence":"additional","affiliation":[{"name":"American University of Beirut, Beirut, Lebanon"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,12,7]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/585265.585270"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503503"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.11.032"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0252-9"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/248052.248070"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/383043.383044"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/646734.701461"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/271510.271519"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201999)","author":"Biere A.","unstructured":"A. Biere , A. Cimatti , E. M. Clarke , and Y. Zhu . 1999. Symbolic model checking without BDDs . In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201999) , LNCS No. 1579. Springer-Verlag, Amsterdam, The Netherlands, 193--207. A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. 1999. Symbolic model checking without BDDs. In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201999), LNCS No. 1579. Springer-Verlag, Amsterdam, The Netherlands, 193--207."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90098-9"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(99)00039-9"},{"key":"e_1_2_1_12_1","first-page":"401","article-title":"A method for CTL model update, representing kripke structures as table systems","volume":"52","author":"Carrillo M.","year":"2009","unstructured":"M. Carrillo and D. A. Rosenblueth . 2009 . A method for CTL model update, representing kripke structures as table systems . Int. J. Pure Appl. Math. 52 (2009), 401 -- 431 . M. Carrillo and D. A. Rosenblueth. 2009. A method for CTL model update, representing kripke structures as table systems. Int. J. Pure Appl. Math. 52 (2009), 401--431.","journal-title":"Int. J. Pure Appl. Math."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_32"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592761.1592781"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"e_1_2_1_16_1","volume-title":"Verification: Theory and Practice","author":"Clarke E. M.","year":"2003","unstructured":"E. M. Clarke and H. Veith . 2003 . Counterexamples revisited: Principles , algorithms, applications. In Verification: Theory and Practice . Springer , 208--224. E. M. Clarke and H. Veith. 2003. Counterexamples revisited: Principles, algorithms, applications. In Verification: Theory and Practice. Springer, 208--224."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/217474.217565"},{"key":"e_1_2_1_19_1","volume-title":"A Discipline of Programming","author":"Dijkstra E. W.","unstructured":"E. W. Dijkstra . 1976. A Discipline of Programming . Prentice-Hall Inc ., Englewood Cliffs, NJ. E. W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall Inc., Englewood Cliffs, NJ."},{"key":"e_1_2_1_20_1","volume-title":"Temporal and modal logic. Handbook of Theoretical Computer Science B","author":"Emerson E. A.","year":"1990","unstructured":"E. A. Emerson . 1990. Temporal and modal logic. Handbook of Theoretical Computer Science B ( 1990 ), 997--1072. E. A. Emerson. 1990. Temporal and modal logic. Handbook of Theoretical Computer Science B (1990), 997--1072."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90017-5"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00239-4"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the Conference on Computer Aided Verification (CAV\u201997)","volume":"1254","author":"Graf S.","unstructured":"S. Graf and H. Saidi . 1997. Construction of abstract state graphs with PVS . In Proceedings of the Conference on Computer Aided Verification (CAV\u201997) . LNCS, Vol. 1254 . Springer, London, UK, 72--83. S. Graf and H. Saidi. 1997. Construction of abstract state graphs with PVS. In Proceedings of the Conference on Computer Aided Verification (CAV\u201997). LNCS, Vol. 1254. Springer, London, UK, 72--83."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177725"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the Conference on Computer Aided Verification (CAV\u201993)","author":"Hojati R.","unstructured":"R. Hojati , R. K. Brayton , and R. P. Kurshan . 1993. BDD-based debugging of designs using language containment and fair CTL . In Proceedings of the Conference on Computer Aided Verification (CAV\u201993) . Springer-Verlag, London, UK, 41--58. Springer LNCS No. 697. R. Hojati, R. K. Brayton, and R. P. Kurshan. 1993. BDD-based debugging of designs using language containment and fair CTL. In Proceedings of the Conference on Computer Aided Verification (CAV\u201993). Springer-Verlag, London, UK, 41--58. Springer LNCS No. 697."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_23"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/138873.138877"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190075"},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the Conference on Computer Aided Verification (CAV\u201903)","author":"Shoham S.","unstructured":"S. Shoham and O. Grumberg . 2003. A game-based framework for CTL counterexamples and 3-valued abstraction-refinement . In Proceedings of the Conference on Computer Aided Verification (CAV\u201903) . ACM, New York, NY, 275--287. S. Shoham and O. Grumberg. 2003. A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. In Proceedings of the Conference on Computer Aided Verification (CAV\u201903). ACM, New York, NY, 275--287."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/11560548_6"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90110-4"},{"key":"e_1_2_1_32_1","first-page":"1","article-title":"CTL model update for system modifications","volume":"31","author":"Zhang Y.","year":"2008","unstructured":"Y. Zhang and Y. Ding . 2008 . CTL model update for system modifications . J. Artif. Int. Res. 31 , 1 (Jan. 2008), 113--155. Y. Zhang and Y. Ding. 2008. CTL model update for system modifications. J. Artif. Int. Res. 31, 1 (Jan. 2008), 113--155.","journal-title":"J. Artif. Int. Res."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3147426","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3147426","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:16Z","timestamp":1750212676000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3147426"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,7]]},"references-count":32,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,3,31]]}},"alternative-id":["10.1145\/3147426"],"URL":"https:\/\/doi.org\/10.1145\/3147426","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,7]]},"assertion":[{"value":"2016-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-12-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}