{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:06:06Z","timestamp":1750309566913,"version":"3.41.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2025,4,26]],"date-time":"2025-04-26T00:00:00Z","timestamp":1745625600000},"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. Comput. Logic"],"published-print":{"date-parts":[[2025,4,30]]},"abstract":"\n Given a program\n P<\/jats:italic>\n , one can construct a Kripke structure\n \n \\(\\mathcal{M}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n . Model checking verifies that\n P<\/jats:italic>\n satisfies a behavioral property given by a temporal logic formula\n \n \\(\\varphi\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n by checking that\n \n \\(\\mathcal{M}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n models\n \n \\(\\varphi\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n . However,\n \n \\(\\mathcal{M}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n can be exponentially large in\n P<\/jats:italic>\n . The action of a symmetry group\n G<\/jats:italic>\n on\n \n \\(\\mathcal{M}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n and\n \n \\(\\varphi\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n can produce a smaller structure\n \n \\(\\overline{\\mathcal{M}}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n . When\n \n \\(\\mathcal{M}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n does not satisfy\n \n \\(\\varphi\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n , one can look for a substructure that satisfies\n \n \\(\\varphi\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n . We call this\n substructure repair<\/jats:italic>\n .\n <\/jats:p>\n \n We show that repairs of\n \n \\(\\overline{\\mathcal{M}}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n lift to repairs of\n \n \\(\\mathcal{M}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n , i.e., we can repair a concurrent program by repairing the smaller structure\n \n \\(\\overline{\\mathcal{M}}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n and symmetrizing the resulting program. The substructures of\n \n \\(\\overline{\\mathcal{M}}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n map to substructures of\n \n \\(\\mathcal{M}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n preserved by\n G<\/jats:italic>\n . We present relative completeness results, which give conditions under which the existence of a repair of\n \n \\(\\mathcal{M}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n implies the existence of a repair of\n \n \\(\\overline{\\mathcal{M}}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n .\n <\/jats:p>\n \n In cases where there is no repair of a Kripke structure\n \n \\(\\mathcal{M}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n w.r.t. a formula, we show that there are instances where it is possible to \u201cunwind\u201d\n \n \\(\\mathcal{M}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n to generate a structure\n \n \\(\\mathcal{M^{\\prime}}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n that is strongly bisimilar to\n \n \\(\\mathcal{M}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n and for which a repair exists. This leads to a natural semantic notion,\n repairability<\/jats:italic>\n , which is not preserved by strong bisimulation. We illustrate the combined use of symmetry reduction and unwinding to effect a repair.\n <\/jats:p>\n Finally, we provide closed-form results for the reductions in number of states in the Kripke structure that can be achieved by symmetry reduction.<\/jats:p>","DOI":"10.1145\/3719008","type":"journal-article","created":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T15:59:21Z","timestamp":1740153561000},"page":"1-44","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Model and Program Repair via Group Actions and Structure Unwinding"],"prefix":"10.1145","volume":"26","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1989-0974","authenticated-orcid":false,"given":"Paul C.","family":"Attie","sequence":"first","affiliation":[{"name":"School of Computer and Cyber Sciences, Augusta University, Augusta, Georgia, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0732-6666","authenticated-orcid":false,"given":"William L.","family":"Cocke","sequence":"additional","affiliation":[{"name":"School of Computer and Cyber Sciences, Augusta University, Augusta, Georgia, USA and Language Technologies Institute, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,4,26]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54013-4_15"},{"key":"e_1_3_3_3_2","doi-asserted-by":"crossref","first-page":"520","DOI":"10.1007\/978-3-031-30829-1_25","volume-title":"Foundations of Software Science and Computation Structures","author":"Attie Paul C.","year":"2023","unstructured":"Paul C. Attie and William L. Cocke. 2023. Model and program repair via group actions. In Foundations of Software Science and Computation Structures. Orna Kupferman and Pawel Sobocinski (Eds.), Springer Nature, Cham, 520\u2013540."},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3147426"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/271510.271519"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/383043.383044"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.5555\/2886151"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/2951860.2951873"},{"key":"e_1_3_3_9_2","doi-asserted-by":"crossref","DOI":"10.1142\/4918","volume-title":"A Walk Through Combinatorics: An Introduction to Enumeration and Graph Theory","author":"B\u00f3na Mikl\u00f3s","year":"2002","unstructured":"Mikl\u00f3s B\u00f3na. 2002. A Walk Through Combinatorics: An Introduction to Enumeration and Graph Theory. World Scientific."},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90098-9"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(99)00039-9"},{"key":"e_1_3_3_12_2","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/978-3-642-28891-3_32","volume-title":"NASA Formal Methods","author":"Chatzieleftheriou George","year":"2012","unstructured":"George Chatzieleftheriou, Borzoo Bonakdarpour, Scott A. Smolka, and Panagiotis Katsaros. 2012. Abstract model repair. In NASA Formal Methods. Alwyn E. Goodloe and Suzette Person (Eds.), Lecture Notes in Computer Science, Vol. 7226. Springer, Berlin, 341\u2013355."},{"key":"e_1_3_3_13_2","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BFb0028741","volume-title":"Proceedings of the Computer Aided Verification (CAV)","author":"Clarke Edmund M.","year":"1998","unstructured":"Edmund M. Clarke, E. Allen Emerson, Somesh Jha, and A. Prasad Sistla. 1998. Symmetry reductions in model checking. In Proceedings of the Computer Aided Verification (CAV). Lecture Notes in Computer Science, Vol. 1427, Springer, 147\u2013158."},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/265943.265960"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00625969"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(80)90021-6"},{"key":"e_1_3_3_18_2","first-page":"481","volume-title":"Proceedings of the International Symposium on Formal Methods","author":"Donaldson Alastair F.","year":"2005","unstructured":"Alastair F. Donaldson and Alice Miller. 2005. Automatic symmetry detection for model checking using computational group theory. In Proceedings of the International Symposium on Formal Methods. Springer, 481\u2013496."},{"key":"e_1_3_3_19_2","first-page":"995","volume-title":"Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B)","author":"Emerson E. Allen","year":"1990","unstructured":"E. Allen Emerson. 1990. Temporal and Modal Logic. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B). Elsevier and MIT Press, Cambridge, MA, 995\u20131072."},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90017-5"},{"key":"e_1_3_3_21_2","first-page":"121","volume-title":"Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS)","author":"Emerson E. Allen","year":"2000","unstructured":"E. Allen Emerson, John Havlicek, and Richard J. Trefler. 2000. Virtual symmetry reduction. In Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, 121\u2013131."},{"key":"e_1_3_3_22_2","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/978-3-540-30124-0_26","volume-title":"Proceedings of the International Workshop on Computer Science Logic","author":"Emerson E. Allen","year":"2004","unstructured":"E. Allen Emerson and Vineet Kahlon. 2004. Parameterized model checking of ring-based message passing systems. In Proceedings of the International Workshop on Computer Science Logic. Lecture Notes in Computer Science, Vol. 3210, Springer, 325\u2013339."},{"key":"e_1_3_3_23_2","first-page":"85","volume-title":"Proceedings of the on Principles of Programming Languages (POPL)","author":"Emerson E. Allen","unstructured":"E. Allen Emerson and Kedar S. Namjoshi. 1995. Reasoning about rings. In Proceedings of the on Principles of Programming Languages (POPL). ACM, 85\u201394."},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054103001881"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00625970"},{"issue":"4","key":"e_1_3_3_26_2","doi-asserted-by":"crossref","first-page":"617","DOI":"10.1145\/262004.262008","article-title":"Utilizing symmetry when model-checking under fairness assumptions: An automata-theoretic approach","volume":"19","author":"Allen Emerson E.","year":"1997","unstructured":"E. Allen Emerson and A. Prasad Sistla. 1997. Utilizing symmetry when model-checking under fairness assumptions: An automata-theoretic approach. ACM Trans. Program. Lang. Syst. 19, 4 (1997), 617\u2013638.","journal-title":"ACM Trans. Program. Lang. Syst"},{"key":"e_1_3_3_27_2","first-page":"427","volume-title":"Proceedings of the Mathematical Foundations of Computer Science (MFCS)","author":"Emerson E. Allen","year":"1998","unstructured":"E. Allen Emerson and Richard J. Trefler. 1998. Model checking real-time properties of symmetric systems. In Proceedings of the Mathematical Foundations of Computer Science (MFCS). Lecture Notes in Computer Science, Vol. 1450, Springer, 427\u2013436."},{"key":"e_1_3_3_28_2","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/3-540-48153-2_12","volume-title":"Proceedings of the Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME)","author":"Emerson E. Allen","year":"1999","unstructured":"E. Allen Emerson and Richard J. Trefler. 1999. From asymmetry to full symmetry: New techniques for symmetry reduction in model checking. In Proceedings of the Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME). Lecture Notes in Computer Science, Vol. 1703, Springer, 142\u2013156."},{"key":"e_1_3_3_29_2","first-page":"382","volume-title":"Proceedings of the Tools and Algorithms for the Construction and Analysis (TACAS)","author":"Emerson E. Allen","year":"2005","unstructured":"E. Allen Emerson and Thomas Wahl. 2005. Dynamic symmetry reduction. In Proceedings of the Tools and Algorithms for the Construction and Analysis (TACAS). Lecture Notes in Computer Science, Vol. 3440, Springer, 382\u2013396."},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/248052.248113"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/146637.146681"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3318162"},{"key":"e_1_3_3_33_2","volume-title":"A Course of Pure Mathematics","author":"Hardy G. H.","year":"1992","unstructured":"G. H. Hardy. 1992. A Course of Pure Mathematics. Cambridge Mathematical Library, Cambridge."},{"key":"e_1_3_3_34_2","volume-title":"Finite Group Theory","author":"Martin Isaacs I","year":"2008","unstructured":"I Martin Isaacs. 2008. Finite Group Theory, Vol. 92. American Mathematical Society, Providence, RI."},{"key":"e_1_3_3_35_2","doi-asserted-by":"crossref","DOI":"10.1090\/gsm\/100","volume-title":"Algebra: A Graduate Course","author":"Martin Isaacs I","year":"2009","unstructured":"I Martin Isaacs. 2009. Algebra: A Graduate Course, Vol. 100. American Mathematical Society , Providence, RI."},{"key":"e_1_3_3_36_2","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1007\/11513988_23","volume-title":"Proceedings of the Computer Aided Verification (CAV)","author":"Jobstmann B.","year":"2005","unstructured":"B. Jobstmann, A. Griesmayer, and R. Bloem. 2005. Program repair as a game. In Proceedings of the Computer Aided Verification (CAV). Springer-Verlag, Berlin, 226\u2013238."},{"key":"e_1_3_3_37_2","volume-title":"Distributed Algorithms","author":"Nancy Lynch","year":"1996","unstructured":"Nancy Lynch. 1996. Distributed Algorithms. Morgan Kaufmann, San Francisco, CA."},{"key":"e_1_3_3_38_2","doi-asserted-by":"crossref","first-page":"496","DOI":"10.1007\/978-3-642-35873-9_29","volume-title":"Proceedings of the International Workshop on Verification, Model Checking, and Abstract Interpretation","author":"Namjoshi Kedar S.","year":"2013","unstructured":"Kedar S. Namjoshi and Richard J. Trefler. 2013. Uncovering symmetries in irregular process networks. In Proceedings of the International Workshop on Verification, Model Checking, and Abstract Interpretation. Springer, 496\u2013514."},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/358527.358537"},{"key":"e_1_3_3_40_2","volume-title":"Finite Groups: An Introduction","author":"Serre Jean-Pierre","year":"2016","unstructured":"Jean-Pierre Serre. 2016. Finite Groups: An Introduction. International Press, Somerville, MA."},{"key":"e_1_3_3_41_2","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/11560548_6","volume-title":"Proceedings of the Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME \u201905)","author":"Staber S.","year":"2005","unstructured":"S. Staber, B. Jobstmann, and R. Bloem. 2005. Finding and fixing faults. In Proceedings of the Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME \u201905). LNCS, Vol. 3725, Springer-Verlag, Berlin, 35\u201349."},{"key":"e_1_3_3_42_2","doi-asserted-by":"crossref","first-page":"498","DOI":"10.1007\/978-3-031-30829-1_24","volume-title":"Proceedings of the Foundations of Software Science and Computation Structures (FoSSaCS)","author":"van Glabbeek Rob","year":"2023","unstructured":"Rob van Glabbeek. 2023. Just testing. In Proceedings of the Foundations of Software Science and Computation Structures (FoSSaCS), 498\u2013519."},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-015-0223-6"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3719008","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3719008","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:19:08Z","timestamp":1750295948000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3719008"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,26]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,4,30]]}},"alternative-id":["10.1145\/3719008"],"URL":"https:\/\/doi.org\/10.1145\/3719008","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2025,4,26]]},"assertion":[{"value":"2024-10-28","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-17","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-26","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}