{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T20:24:34Z","timestamp":1791231874985,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":53,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,7,12]],"date-time":"2023-07-12T00:00:00Z","timestamp":1689120000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"FNR","award":["C19\/IS\/13646587\/RASoRS"],"award-info":[{"award-number":["C19\/IS\/13646587\/RASoRS"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,7,15]]},"DOI":"10.1145\/3583131.3590454","type":"proceedings-article","created":{"date-parts":[[2024,2,18]],"date-time":"2024-02-18T06:57:04Z","timestamp":1708239424000},"page":"1499-1507","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Automated Repair of Unrealisable LTL Specifications Guided by Model Counting"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-9427-9345","authenticated-orcid":false,"given":"Mat\u00edas","family":"Brizzio","sequence":"first","affiliation":[{"name":"IMDEA Software Institute, Madrid, Spain"},{"name":"Universidad Polit\u00e9cnica de Madrid, Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8312-1358","authenticated-orcid":false,"given":"Maxime","family":"Cordy","sequence":"additional","affiliation":[{"name":"SnT, University of Luxembourg, Luxembourg, Luxembourg"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1852-2547","authenticated-orcid":false,"given":"Mike","family":"Papadakis","sequence":"additional","affiliation":[{"name":"SnT, University of Luxembourg, Luxembourg, Luxembourg"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3927-4773","authenticated-orcid":false,"given":"C\u00e9sar","family":"S\u00e1nchez","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0532-5296","authenticated-orcid":false,"given":"Nazareno","family":"Aguirre","sequence":"additional","affiliation":[{"name":"Universidad Nacional de R\u00edo Cuarto, R\u00edo Cuarto, Argentina"},{"name":"CONICET, R\u00edo Cuarto, Argentina"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1611-3969","authenticated-orcid":false,"given":"Renzo","family":"Degiovanni","sequence":"additional","affiliation":[{"name":"SnT, University of Luxembourg, Luxembourg, Luxembourg"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,7,12]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Aalta benchmark. https:\/\/www.lab301.cn\/aalta\/node3.html."},{"key":"e_1_3_2_1_2_1","unstructured":"Commons math: The apache commons mathematics library. https:\/\/commons.apache.org\/proper\/commons-math\/."},{"key":"e_1_3_2_1_3_1","unstructured":"The reactive synthesis competition. www.syntcomp.org."},{"key":"e_1_3_2_1_4_1","unstructured":"Synthesis competition repository. https:\/\/bitbucket.org\/swenjacobs\/syntcomp\/."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380927"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10431-7_9"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932505"},{"key":"e_1_3_2_1_8_1","first-page":"26","volume-title":"FMCAD 2013","author":"Alur Rajeev","year":"2013","unstructured":"Rajeev Alur, Salar Moarref, and Ufuk Topcu. Counter-strategy guided refinement of GR(1) temporal logic specifications. In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20--23, 2013, pages 26--33, 2013."},{"key":"e_1_3_2_1_9_1","volume-title":"IFAC Proceedings Volumes, 31(18):447 -- 452, 1998. 5th IFAC Conference on System Structure and Control 1998 (SSC'98)","author":"Asarin Eugene","unstructured":"Eugene Asarin, Oded Maler, Amir Pnueli, and Joseph Sifakis. Controller synthesis for timed automata. IFAC Proceedings Volumes, 31(18):447 -- 452, 1998. 5th IFAC Conference on System Structure and Control 1998 (SSC'98), Nantes, France."},{"key":"e_1_3_2_1_10_1","first-page":"255","volume-title":"CAV 2015, San Francisco, CA, USA, July 18--24, 2015, Proceedings, Part I","author":"Aydin Abdulbaki","year":"2015","unstructured":"Abdulbaki Aydin, Lucas Bang, and Tevfik Bultan. Automata-based model counting for string constraints. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18--24, 2015, Proceedings, Part I, pages 255--272, 2015."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2000799.2000800"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2011.08.007"},{"key":"e_1_3_2_1_13_1","first-page":"281","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Cavezza Davide G","year":"2017","unstructured":"Davide G Cavezza and Dalal Alrajeh. Interpolation-based GR(1) assumptions refinement. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 281--297. Springer, 2017."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_14"},{"key":"e_1_3_2_1_15_1","volume-title":"Abstract model repair. Log. Methods Comput. Sci., 11(3)","author":"Chatzieleftheriou George","year":"2015","unstructured":"George Chatzieleftheriou, Borzoo Bonakdarpour, Panagiotis Katsaros, and Scott A. Smolka. Abstract model repair. Log. Methods Comput. Sci., 11(3), 2015."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1787526.1787535"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568323"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180261"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238220"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970349"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2430536.2430543"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302672"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90017-5"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-04921-2_29"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/1600258.1600261"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/534133"},{"key":"e_1_3_2_1_28_1","volume-title":"Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, AAAI 97","author":"Bayardo Roberto J.","year":"1997","unstructured":"Roberto J. Bayardo Jr. and Robert Schrag. Using CSP look-back techniques to solve real-world SAT instances. In Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, AAAI 97, IAAI 97, July 27--31, 1997, Providence, Rhode Island., pages 203--208, 1997."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0221-y"},{"key":"e_1_3_2_1_30_1","volume-title":"Genetic Programming: On the Programming of Computers by Means of Natural Selection","author":"Koza John R.","year":"1992","unstructured":"John R. Koza. Genetic Programming: On the Programming of Computers by Means of Natural Selection. MIT Press, Cambridge, MA, USA, 1992."},{"key":"e_1_3_2_1_31_1","series-title":"Electronic Proceedings in Theoretical Computer Science","first-page":"50","volume-title":"Proceedings 3rd Workshop on formal reasoning about Causation, Responsibility, and Explanations in Science and Technology, Thessaloniki, Greece, 21st","author":"Kress-Gazit Hadas","year":"2018","unstructured":"Hadas Kress-Gazit and Hazem Torfah. The challenges in specifying and explaining synthesized implementations of reactive systems. In Bernd Finkbeiner and Samantha Kleinberg, editors, Proceedings 3rd Workshop on formal reasoning about Causation, Responsibility, and Explanations in Science and Technology, Thessaloniki, Greece, 21st April 2018, volume 286 of Electronic Proceedings in Theoretical Computer Science, pages 50--64. Open Publishing Association, 2019."},{"key":"e_1_3_2_1_32_1","first-page":"543","volume-title":"ATVA 2018, Los Angeles, CA, USA, October 7--10, 2018","author":"Kret\u00ednsk\u00fd Jan","year":"2018","unstructured":"Jan Kret\u00ednsk\u00fd, Tobias Meggendorfer, and Salomon Sickert. Owl: A library for \u03c9-words, automata, and LTL. In Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7--10, 2018, Proceedings, pages 543--550, 2018."},{"key":"e_1_3_2_1_33_1","first-page":"186","volume-title":"5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15--17, 2004","author":"Latvala Timo","year":"2004","unstructured":"Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi A. Junttila. Simple bounded LTL model checking. In Formal Methods in Computer-Aided Design, 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15--17, 2004, Proceedings, pages 186--200, 2004."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2011.104"},{"key":"e_1_3_2_1_35_1","volume-title":"Polsat: A portfolio LTL satisfiability solver. CoRR, abs\/1311.1602","author":"Li Jianwen","year":"2013","unstructured":"Jianwen Li, Geguang Pu, Lijun Zhang, Yinbo Yao, Moshe Y. Vardi, and Jifeng He. Polsat: A portfolio LTL satisfiability solver. CoRR, abs\/1311.1602, 2013."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26287-1_13"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2011.5970509"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/128869"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/211468"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/357233.357237"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00106"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2015.63"},{"key":"e_1_3_2_1_43_1","first-page":"578","volume-title":"CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14--17, 2018, Proceedings, Part I","author":"Meyer Philipp J.","year":"2018","unstructured":"Philipp J. Meyer, Salomon Sickert, and Michael Luttenberger. Strix: Explicit reactive synthesis strikes back! In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14--17, 2018, Proceedings, Part I, pages 578--586, 2018."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/229930"},{"key":"e_1_3_2_1_45_1","first-page":"364","volume-title":"VMCAI","author":"Piterman Nir","year":"2006","unstructured":"Nir Piterman, Amir Pnueli, and Yaniv Sa'ar. Synthesis of reactive(1) designs. In VMCAI, pages 364--380, 2006."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2012.2214558"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11623-0_7"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2019\/163"},{"key":"e_1_3_2_1_50_1","first-page":"424","volume-title":"9th International Conference","author":"Thurley Marc","year":"2006","unstructured":"Marc Thurley. sharpsat - counting models with advanced component caching and implicit BCP. In Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference, Seattle, WA, USA, August 12--15, 2006, Proceedings, pages 424--429, 2006."},{"key":"e_1_3_2_1_51_1","volume-title":"Requirements Engineering - From System Goals to UML Models to Software Specifications","author":"van Lamsweerde Axel","year":"2009","unstructured":"Axel van Lamsweerde. Requirements Engineering - From System Goals to UML Models to Software Specifications. Wiley, 2009."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.879820"},{"issue":"2","key":"e_1_3_2_1_53_1","first-page":"101","article-title":"A Critique and Improvement of the \"CL","volume":"25","author":"Vargha Andr\u00e1s","year":"2000","unstructured":"Andr\u00e1s Vargha and Harold D. Delaney. A Critique and Improvement of the \"CL\" Common Language Effect Size Statistics of McGraw and Wong. Journal of Educational and Behavioral Statistics, 25(2):101--132, 2000.","journal-title":"Journal of Educational and Behavioral Statistics"}],"event":{"name":"GECCO '23: Genetic and Evolutionary Computation Conference","location":"Lisbon Portugal","acronym":"GECCO '23","sponsor":["SIGEVO ACM Special Interest Group on Genetic and Evolutionary Computation"]},"container-title":["Proceedings of the Genetic and Evolutionary Computation Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3583131.3590454","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3583131.3590454","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:03Z","timestamp":1750178823000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3583131.3590454"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7,12]]},"references-count":53,"alternative-id":["10.1145\/3583131.3590454","10.1145\/3583131"],"URL":"https:\/\/doi.org\/10.1145\/3583131.3590454","relation":{},"subject":[],"published":{"date-parts":[[2023,7,12]]},"assertion":[{"value":"2023-07-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}