research-article

Open access

Solving Infinite-State Games via Acceleration

Authors:

Rayna DimitrovaAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 8, Issue POPL

Article No.: 57, Pages 1696 - 1726

https://doi.org/10.1145/3632899

Published: 05 January 2024 Publication History

Abstract

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.

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.

References

[1]

Parosh Aziz Abdulla, Ahmed Bouajjani, and Julien d’Orso. 2008. Monotonic and Downward Closed Games. J. Log. Comput., 18, 1 (2008), 153–169. https://doi.org/10.1093/logcom/exm062

[2]

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–17.

[3]

Thomas Ball and Orna Kupferman. 2006. An Abstraction-Refinement Framework for Multi-Agent Systems. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings. IEEE Computer Society, 379–388. https://doi.org/10.1109/LICS.2006.10

[4]

Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022. cvc5: A Versatile and Industrial-Strength SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, Dana Fisman and Grigore Rosu (Eds.) (Lecture Notes in Computer Science, Vol. 13243). Springer, 415–442. https://doi.org/10.1007/978-3-030-99524-9_24

[5]

Sébastien Bardin, Alain Finkel, Jérôme Leroux, and Laure Petrucci. 2003. FAST: Fast Acceleration of Symbolic Transition Systems. In Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings, Warren A. Hunt Jr. and Fabio Somenzi (Eds.) (Lecture Notes in Computer Science, Vol. 2725). Springer, 118–121. https://doi.org/10.1007/978-3-540-45069-6_12

[6]

Sébastien Bardin, Alain Finkel, Jérôme Leroux, and Philippe Schnoebelen. 2005. Flat Acceleration in Symbolic Model Checking. In Automated Technology for Verification and Analysis, Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings, Doron A. Peled and Yih-Kuen Tsay (Eds.) (Lecture Notes in Computer Science, Vol. 3707). Springer, 474–488. https://doi.org/10.1007/11562948_35

[7]

Raven Beutner and Bernd Finkbeiner. 2022. Software Verification of Hyperproperties Beyond k-Safety. In Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I, Sharon Shoham and Yakir Vizel (Eds.) (Lecture Notes in Computer Science, Vol. 13371). Springer, 341–362. https://doi.org/10.1007/978-3-031-13185-1_17

[8]

Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, and Andrey Rybalchenko. 2014. A constraint-based approach to solving games on infinite graphs. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, Suresh Jagannathan and Peter Sewell (Eds.). ACM, 221–234. https://doi.org/10.1145/2535838.2535860

[9]

Roderick Bloem, Krishnendu Chatterjee, and Barbara Jobstmann. 2018. Graph Games and Reactive Synthesis. In Handbook of Model Checking, Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (Eds.). Springer, 921–962. https://doi.org/10.1007/978-3-319-10575-8_27

[10]

Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, and Yaniv Sa’ar. 2012. Synthesis of Reactive(1) designs. J. Comput. Syst. Sci., 78, 3 (2012), 911–938. https://doi.org/10.1016/j.jcss.2011.08.007

[11]

Marijke H. L. Bodlaender, Cor A. J. Hurkens, Vincent J. J. Kusters, Frank Staals, Gerhard J. Woeginger, and Hans Zantema. 2012. Cinderella versus the Wicked Stepmother. In Theoretical Computer Science - 7th IFIP TC 1/WG 2.2 International Conference, TCS 2012, Amsterdam, The Netherlands, September 26-28, 2012. Proceedings, Jos C. M. Baeten, Thomas Ball, and Frank S. de Boer (Eds.) (Lecture Notes in Computer Science, Vol. 7604). Springer, 57–71. https://doi.org/10.1007/978-3-642-33475-7_5

[12]

Wonhyuk Choi, Bernd Finkbeiner, Ruzica Piskac, and Mark Santolucito. 2022. Can reactive synthesis and syntax-guided synthesis be friends? In PLDI ’22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022, Ranjit Jhala and Isil Dillig (Eds.). ACM, 229–243. https://doi.org/10.1145/3519939.3523429

[13]

Alonzo Church. 1962. Logic, arithmetic and automata. In International congress of mathematicians. 23–35.

[14]

Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar. 2001. Symbolic Algorithms for Infinite-State Games. In CONCUR 2001 - Concurrency Theory, 12th International Conference, Aalborg, Denmark, August 20-25, 2001, Proceedings, Kim Guldstrand Larsen and Mogens Nielsen (Eds.) (Lecture Notes in Computer Science, Vol. 2154). Springer, 536–550. https://doi.org/10.1007/3-540-44685-0_36

[15]

Leonardo Mendonça de Moura and Nikolaj S. Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, C. R. Ramakrishnan and Jakob Rehof (Eds.) (Lecture Notes in Computer Science, Vol. 4963). Springer, 337–340. https://doi.org/10.1007/978-3-540-78800-3_24

[16]

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.

[17]

Azadeh Farzan and Zachary Kincaid. 2018. Strategy synthesis for linear arithmetic games. Proc. ACM Program. Lang., 2, POPL (2018), 61:1–61:30. https://doi.org/10.1145/3158149

[18]

Grigory Fedyukovich, Arie Gurfinkel, and Aarti Gupta. 2019. Lazy but Effective Functional Synthesis. In Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Cascais, Portugal, January 13-15, 2019, Proceedings, Constantin Enea and Ruzica Piskac (Eds.) (Lecture Notes in Computer Science, Vol. 11388). Springer, 92–113. https://doi.org/10.1007/978-3-030-11245-5_5

[19]

Bernd Finkbeiner, Philippe Heim, and Noemi Passing. 2022. Temporal Stream Logic modulo Theories. In Foundations of Software Science and Computation Structures - 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Patricia Bouyer and Lutz Schröder (Eds.) (Lecture Notes in Computer Science, Vol. 13242). Springer, 325–346. https://doi.org/10.1007/978-3-030-99253-8_17

[20]

Bernd Finkbeiner, Felix Klein, Ruzica Piskac, and Mark Santolucito. 2019. Temporal Stream Logic: Synthesis Beyond the Bools. In Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I, Isil Dillig and Serdar Tasiran (Eds.) (Lecture Notes in Computer Science, Vol. 11561). Springer, 609–629. https://doi.org/10.1007/978-3-030-25540-4_35

[21]

Bernd Finkbeiner and Sven Schewe. 2013. Bounded synthesis. Int. J. Softw. Tools Technol. Transf., 15, 5-6 (2013), 519–539. https://doi.org/10.1007/s10009-012-0228-z

[22]

Alain Finkel and Jérôme Leroux. 2002. How to Compose Presburger-Accelerations: Applications to Broadcast Protocols. In FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science, 22nd Conference Kanpur, India, December 12-14, 2002, Proceedings, Manindra Agrawal and Anil Seth (Eds.) (Lecture Notes in Computer Science, Vol. 2556). Springer, 145–156. https://doi.org/10.1007/3-540-36206-1_14

[23]

2002. Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001], Erich Grädel, Wolfgang Thomas, and Thomas Wilke (Eds.) (Lecture Notes in Computer Science, Vol. 2500). Springer. isbn:3-540-00388-6 https://doi.org/10.1007/3-540-36387-4

[24]

Andreas Griesmayer, Roderick Bloem, and Byron Cook. 2006. Repair of Boolean Programs with an Application to C. In Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, Thomas Ball and Robert B. Jones (Eds.) (Lecture Notes in Computer Science, Vol. 4144). Springer, 358–371. https://doi.org/10.1007/11817963_33

[25]

Orna Grumberg, Martin Lange, Martin Leucker, and Sharon Shoham. 2005. Don’t Know in the μ -Calculus. In Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings, Radhia Cousot (Ed.) (Lecture Notes in Computer Science, Vol. 3385). Springer, 233–249. https://doi.org/10.1007/978-3-540-30579-8_16

[26]

Orna Grumberg, Martin Lange, Martin Leucker, and Sharon Shoham. 2007. When not losing is better than winning: Abstraction and refinement for the full mu-calculus. Inf. Comput., 205, 8 (2007), 1130–1148. https://doi.org/10.1016/j.ic.2006.10.009

[27]

Philippe Heim and Rayna Dimitrova. 2023. Artifact of "Solving Infinite-State Games via Acceleration". https://doi.org/10.5281/zenodo.8424953

[28]

Philippe Heim and Rayna Dimitrova. 2023. Solving Infinite-State Games via Acceleration (Full Version). https://doi.org/10.48550/ARXIV.2305.16118 arxiv:2305.16118.

[29]

Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. 2003. Counterexample-Guided Control. In Automata, Languages and Programming, 30th International Colloquium, ICALP 2003, Eindhoven, The Netherlands, June 30 - July 4, 2003. Proceedings, Jos C. M. Baeten, Jan Karel Lenstra, Joachim Parrow, and Gerhard J. Woeginger (Eds.) (Lecture Notes in Computer Science, Vol. 2719). Springer, 886–902. https://doi.org/10.1007/3-540-45061-0_69

[30]

Andreas Katis, Grigory Fedyukovich, Huajun Guo, Andrew Gacek, John Backes, Arie Gurfinkel, and Michael W. Whalen. 2018. Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. In Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II, Dirk Beyer and Marieke Huisman (Eds.) (Lecture Notes in Computer Science, Vol. 10806). Springer, 176–193. https://doi.org/10.1007/978-3-319-89963-3_10

[31]

Hadas Kress-Gazit, Georgios E. Fainekos, and George J. Pappas. 2009. Temporal-Logic-Based Reactive Mission and Motion Planning. IEEE Trans. Robotics, 25, 6 (2009), 1370–1381. https://doi.org/10.1109/TRO.2009.2030225

[32]

Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, and Christoph M. Wintersteiger. 2013. Loop summarization using state and transition invariants. Formal Methods Syst. Des., 42, 3 (2013), 221–261. https://doi.org/10.1007/s10703-012-0176-y

[33]

Jérôme Leroux and Grégoire Sutre. 2006. Flat counter automata almost everywhere!. In Software Verification: Infinite-State Model Checking and Static Program Analysis, 19.02. - 24.02.2006, Parosh Aziz Abdulla, Ahmed Bouajjani, and Markus Müller-Olm (Eds.) (Dagstuhl Seminar Proceedings, Vol. 06081). Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany. http://drops.dagstuhl.de/opus/volltexte/2006/729

[34]

Benedikt Maderbacher and Roderick Bloem. 2021. Reactive Synthesis Modulo Theories Using Abstraction Refinement. CoRR, abs/2108.00090 (2021), arXiv:2108.00090. arxiv:2108.00090

[35]

Oliver Markgraf, Chih-Duo Hong, Anthony W. Lin, Muhammad Najib, and Daniel Neider. 2020. Parameterized Synthesis with Safety Properties. In Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Fukuoka, Japan, November 30 - December 2, 2020, Proceedings, Bruno C. d. S. Oliveira (Ed.) (Lecture Notes in Computer Science, Vol. 12470). Springer, 273–292. https://doi.org/10.1007/978-3-030-64437-6_14

[36]

Philipp J. Meyer, Salomon Sickert, and Michael Luttenberger. 2018. 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, Hana Chockler and Georg Weissenbacher (Eds.) (Lecture Notes in Computer Science, Vol. 10981). Springer, 578–586. https://doi.org/10.1007/978-3-319-96145-3_31

[37]

Daniel Neider and Ufuk Topcu. 2016. An Automaton Learning Approach to Solving Safety Games over Infinite Graphs. In Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, Marsha Chechik and Jean-François Raskin (Eds.) (Lecture Notes in Computer Science, Vol. 9636). Springer, 204–221. https://doi.org/10.1007/978-3-662-49674-9_12

[38]

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, and Cesare Tinelli. 2021. Syntax-Guided Quantifier Instantiation. In Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II, Jan Friso Groote and Kim Guldstrand Larsen (Eds.) (Lecture Notes in Computer Science, Vol. 12652). Springer, 145–163. https://doi.org/10.1007/978-3-030-72013-1_8

[39]

Stanly Samuel, Deepak D’Souza, and Raghavan Komondoor. 2021. GenSys: a scalable fixed-point engine for maximal controller synthesis over infinite state spaces. In ESEC/FSE ’21: 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Athens, Greece, August 23-28, 2021, Diomidis Spinellis, Georgios Gousios, Marsha Chechik, and Massimiliano Di Penta (Eds.). ACM, 1585–1589. https://doi.org/10.1145/3468264.3473126

[40]

Stanly Samuel, Deepak D’Souza, and Raghavan Komondoor. 2023. Towards Efficient Controller Synthesis Techniques for Logical LTL Games. arxiv:2306.02427v2.

[41]

Paulo Tabuada. 2009. Verification and Control of Hybrid Systems - A Symbolic Approach. Springer. isbn:978-1-4419-0223-8 http://www.springer.com/mathematics/applications/book/978-1-4419-0223-8

[42]

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. arxiv:2007.03656

[43]

Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen. 2023. Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification. Proc. ACM Program. Lang., 7, POPL (2023), 2111–2140. https://doi.org/10.1145/3571265

[44]

Adam Walker and Leonid Ryzhyk. 2014. Predicate abstraction for reactive synthesis. In Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014. IEEE, 219–226. https://doi.org/10.1109/FMCAD.2014.6987617

[45]

Igor Walukiewicz. 2001. Pushdown Processes: Games and Model-Checking. Inf. Comput., 164, 2 (2001), 234–263. https://doi.org/10.1006/inco.2000.2894

[46]

Woeginger. 2009. Combinatorics problem C5. 33–35 pages.

Cited By

Tsukada TUnno HPadon OShoham S(2025)A Primal-Dual Perspective on Program Verification AlgorithmsProceedings of the ACM on Programming Languages10.1145/37049049:POPL(2025-2056)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704904
Heim PDimitrova R(2025)Translation of Temporal Logic for Efficient Infinite-State Reactive SynthesisProceedings of the ACM on Programming Languages10.1145/37048889:POPL(1536-1567)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704888
Rodríguez AGorostiaga FSánchez C(2024)Predictable and Performant Reactive Synthesis Modulo Theories via Functional SynthesisAutomated Technology for Verification and Analysis10.1007/978-3-031-78750-8_2(28-50)Online publication date: 21-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-78750-8_2
Show More Cited By

Index Terms

Solving Infinite-State Games via Acceleration
1. Software and its engineering
  1. Software creation and management
    1. Software development techniques
      1. Automatic programming
2. Theory of computation
  1. Logic
    1. Logic and verification

Recommendations

A constraint-based approach to solving games on infinite graphs
POPL '14

We present a constraint-based approach to computing winning strategies in two-player graph games over the state space of infinite-state programs. Such games have numerous applications in program verification and synthesis, including the synthesis of ...
A constraint-based approach to solving games on infinite graphs
POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

We present a constraint-based approach to computing winning strategies in two-player graph games over the state space of infinite-state programs. Such games have numerous applications in program verification and synthesis, including the synthesis of ...
Strategy synthesis for linear arithmetic games

Many problems in formal methods can be formalized as two-player games. For several applications—program synthesis, for example—in addition to determining which player wins the game, we are interested in computing a winning strategy for that player. This ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 8, Issue POPL

January 2024

2820 pages

EISSN:2475-1421

DOI:10.1145/3554315

Editor:
Michael Hicks
Amazon, USA

Issue’s Table of Contents

Copyright © 2024 Owner/Author.

This work is licensed under a Creative Commons Attribution 4.0 International License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 January 2024

Published in PACMPL Volume 8, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
385
Total Downloads

Downloads (Last 12 months)317
Downloads (Last 6 weeks)38

Reflects downloads up to 03 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Tsukada TUnno HPadon OShoham S(2025)A Primal-Dual Perspective on Program Verification AlgorithmsProceedings of the ACM on Programming Languages10.1145/37049049:POPL(2025-2056)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704904
Heim PDimitrova R(2025)Translation of Temporal Logic for Efficient Infinite-State Reactive SynthesisProceedings of the ACM on Programming Languages10.1145/37048889:POPL(1536-1567)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704888
Rodríguez AGorostiaga FSánchez C(2024)Predictable and Performant Reactive Synthesis Modulo Theories via Functional SynthesisAutomated Technology for Verification and Analysis10.1007/978-3-031-78750-8_2(28-50)Online publication date: 21-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-78750-8_2
Maderbacher BWindisch FBloem R(2024)Synthesis from Infinite-State Generalized Reactivity(1) SpecificationsLeveraging Applications of Formal Methods, Verification and Validation. Software Engineering Methodologies10.1007/978-3-031-75387-9_17(281-301)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-75387-9_17
Schmuck AHeim PDimitrova RNayak S(2024)Localized Attractor Computations for Infinite-State GamesComputer Aided Verification10.1007/978-3-031-65633-0_7(135-158)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65633-0_7

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Figures

Tables

Media

View Issue’s Table of Contents