{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T18:19:04Z","timestamp":1784830744314,"version":"3.55.0"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>Two-player graph games have found numerous applications, most notably in the synthesis of reactive systems from temporal specifications, but also in verification. The relevance of infinite-state systems in these areas has lead to significant attention towards developing techniques for solving infinite-state games.<\/jats:p>\n          <jats:p>We propose novel symbolic semi-algorithms for solving infinite-state games with temporal winning conditions. The novelty of our approach lies in the introduction of an acceleration technique that enhances fixpoint-based game-solving methods and helps to avoid divergence. Classical fixpoint-based algorithms, when applied to infinite-state games, are bound to diverge in many cases, since they iteratively compute the set of states from which one player has a winning strategy. Our proposed approach can lead to convergence in cases where existing algorithms require an infinite number of iterations. This is achieved by acceleration: computing an infinite set of states from which a simpler sub-strategy can be iterated an unbounded number of times in order to win the game. Ours is the first method for solving infinite-state games to employ acceleration. Thanks to this, it is able to outperform state-of-the-art techniques on a range of benchmarks, as evidenced by our evaluation of a prototype implementation.<\/jats:p>","DOI":"10.1145\/3632899","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"1696-1726","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Solving Infinite-State Games via Acceleration"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5433-8133","authenticated-orcid":false,"given":"Philippe","family":"Heim","sequence":"first","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-2494-8690","authenticated-orcid":false,"given":"Rayna","family":"Dimitrova","sequence":"additional","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exm062"},{"key":"e_1_3_1_3_1","doi-asserted-by":"crossref","unstructured":"Rajeev Alur Rastislav Bodik Garvit Juniwal Milo M. K. Martin Mukund Raghothaman Sanjit A. Seshia Rishabh Singh Armando Solar-Lezama Emina Torlak and Abhishek Udupa. 2013. Syntax-Guided Synthesis. In Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD). 1\u201317.","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.10"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_12"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11562948_35"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_17"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535860"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_27"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2011.08.007"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33475-7_5"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523429"},{"key":"e_1_3_1_14_1","unstructured":"Alonzo Church. 1962. Logic arithmetic and automata. In International congress of mathematicians. 23\u201335."},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44685-0_36"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_17_1","doi-asserted-by":"crossref","unstructured":"Marco Faella and Gennaro Parlato. 2023. Reachability Games Modulo Theories with a Bounded Safety Player. In Thirty-Seventh AAAI Conference on Artificial Intelligence AAAI 2023.","DOI":"10.1609\/aaai.v37i5.25779"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158149"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-11245-5_5"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99253-8_17"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_35"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0228-z"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36206-1_14"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36387-4"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_33"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_16"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.10.009"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","unstructured":"Philippe Heim and Rayna Dimitrova. 2023a. Artifact of \u201cSolving Infinite-State Games via Acceleration\u201d. https:\/\/doi.org\/10.5281\/zenodo.8424953 10.5281\/zenodo.8424953","DOI":"10.5281\/zenodo.8424953"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","unstructured":"Philippe Heim and Rayna Dimitrova. 2023b. Solving Infinite-State Games via Acceleration (Full Version). https:\/\/doi.org\/10.48550\/ARXIV.2305.16118 10.48550\/ARXIV.2305.16118 arXiv:2305.16118 [cs.LO]","DOI":"10.48550\/ARXIV.2305.16118"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45061-0_69"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_10"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2009.2030225"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0176-y"},{"key":"e_1_3_1_34_1","volume-title":"Software Verification: Infinite-State Model Checking and Static Program Analysis, 19.02. - 24.02.2006 (Dagstuhl Seminar Proceedings, Vol. 06081)","author":"Leroux J\u00e9r\u00f4me","year":"2006","unstructured":"J\u00e9r\u00f4me Leroux and Gr\u00e9goire Sutre. 2006. Flat counter automata almost everywhere!. In Software Verification: Infinite-State Model Checking and Static Program Analysis, 19.02. - 24.02.2006 (Dagstuhl Seminar Proceedings, Vol. 06081), Parosh Aziz Abdulla, Ahmed Bouajjani, and Markus M\u00fcller-Olm (Eds.). Internationales Begegnungs-und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany. http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2006\/729"},{"key":"e_1_3_1_35_1","unstructured":"Benedikt Maderbacher and Roderick Bloem. 2021. Reactive Synthesis Modulo Theories Using Abstraction Refinement. CoRR abs\/2108.00090 (2021). arXiv:2108.00090 https:\/\/arxiv.org\/abs\/2108.00090"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-64437-6_14"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_31"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_12"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72013-1_8"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3468264.3473126"},{"key":"e_1_3_1_41_1","unstructured":"Stanly Samuel Deepak D\u2019Souza and Raghavan Komondoor. 2023. Towards Efficient Controller Synthesis Techniques for Logical LTL Games. arXiv:2306.02427v2 [cs.LO]"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-0224-5"},{"key":"e_1_3_1_43_1","unstructured":"Hiroshi Unno Yuki Satake Tachio Terauchi and Eric Koskinen. 2020. Program Verification via Predicate Constraint Satisfiability Modulo Theories. CoRR abs\/2007.03656 (2020). arXiv:2007.03656 https:\/\/arxiv.org\/abs\/2007.03656"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571265"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987617"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2894"},{"key":"e_1_3_1_47_1","unstructured":"Woeginger. 2009. Combinatorics problem C5. 33\u201335 pages."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632899","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632899","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:04:18Z","timestamp":1751659458000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632899"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":46,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632899"],"URL":"https:\/\/doi.org\/10.1145\/3632899","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}