Document Open Access Logo

Faster and Smaller Solutions of Obliging Games

Authors Daniel Hausmann , Nir Piterman

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2024.28.pdf
  • Filesize: 0.75 MB
  • 19 pages

Document Identifiers

Author Details

Daniel Hausmann
  • University of Gothenburg, Gothenburg, Sweden
  • Chalmers University of Technology, Gothenburg, Sweden
  • University of Liverpool, Liverpool, United Kingdom
Nir Piterman
  • University of Gothenburg, Gothenburg, Sweden
  • Chalmers University of Technology, Gothenburg, Sweden

Funding

Both authors supported by the ERC Consolidator grant D-SynMA (No. 772459).
  • Hausmann, Daniel: Supported by the EPSRC through grant EP/Z003121/1.

Cite AsGet BibTex

Daniel Hausmann and Nir Piterman. Faster and Smaller Solutions of Obliging Games. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CONCUR.2024.28

Abstract

Obliging games have been introduced in the context of the game perspective on reactive synthesis in order to enforce a degree of cooperation between the to-be-synthesized system and the environment. Previous approaches to the analysis of obliging games have been small-step in the sense that they have been based on a reduction to standard (non-obliging) games in which single moves correspond to single moves in the original (obliging) game. Here, we propose a novel, large-step view on obliging games, reducing them to standard games in which single moves encode long-term behaviors in the original game. This not only allows us to give a meaningful definition of the environment winning in obliging games, but also leads to significantly improved bounds on both strategy sizes and the solution runtime for obliging games.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Two-player games
  • reactive synthesis
  • Emerson-Lei games
  • parity games

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Christel Baier, Frantisek Blahoudek, Alexandre Duret-Lutz, Joachim Klein, David Müller, and Jan Strejcek. Generic emptiness check for fun and profit. In Automated Technology for Verification and Analysis, ATVA 2019, volume 11781 of LNCS, pages 445-461. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-31784-3_26.
  2. Roderick Bloem, Rüdiger Ehlers, Swen Jacobs, and Robert Könighofer. How to handle assumptions in synthesis. In Workshop on Synthesis, SYNT 2014, volume 157 of EPTCS, pages 34-50, 2014. URL: https://doi.org/10.4204/EPTCS.157.7.
  3. Roderick Bloem, Rüdiger Ehlers, and Robert Könighofer. Cooperative reactive synthesis. In Automated Technology for Verification and Analysis, ATVA 2015, volume 9364 of Lecture Notes in Computer Science, pages 394-410. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24953-7_29.
  4. Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, and Yaniv Sa'ar. Synthesis of reactive(1) designs. J. Comput. Syst. Sci., 78(3):911-938, 2012. URL: https://doi.org/10.1016/J.JCSS.2011.08.007.
  5. Julian C. Bradfield and Igor Walukiewicz. The μ-calculus and model checking. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 871-919. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_26.
  6. Krishnendu Chatterjee, Florian Horn, and Christof Löding. Obliging games. In Concurrency Theory, 21th International Conference, CONCUR 2010, volume 6269 of LNCS, pages 284-296. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_20.
  7. Stefan Dziembowski, Marcin Jurdzinski, and Igor Walukiewicz. How much memory is needed to win infinite games? In Logic in Computer Science, LICS 1997, pages 99-110. IEEE Computer Society, 1997. URL: https://doi.org/10.1109/LICS.1997.614939.
  8. Javier Esparza, Jan Kretínský, Jean-François Raskin, and Salomon Sickert. From linear temporal logic and limit-deterministic Büchi automata to deterministic parity automata. Int. J. Softw. Tools Technol. Transf., 24(4):635-659, 2022. URL: https://doi.org/10.1007/S10009-022-00663-1.
  9. Oliver Friedmann and Martin Lange. Deciding the unguarded modal μ-calculus. J. Appl. Non Class. Logics, 23(4):353-371, 2013. URL: https://doi.org/10.1080/11663081.2013.861181.
  10. Oliver Friedmann, Markus Latte, and Martin Lange. Satisfiability games for branching-time logics. Log. Methods Comput. Sci., 9(4), 2013. URL: https://doi.org/10.2168/LMCS-9(4:5)2013.
  11. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of Lecture Notes in Computer Science. Springer, 2002. URL: https://doi.org/10.1007/3-540-36387-4.
  12. Yuri Gurevich and Leo Harrington. Trees, automata, and games. In Symposium on Theory of Computing, STOC 1982, pages 60-65. ACM, 1982. URL: https://doi.org/10.1145/800070.802177.
  13. Daniel Hausmann. Faster game solving by fixpoint acceleration. CoRR, abs/2404.13687, 2024. URL: https://arxiv.org/abs/2404.13687.
  14. Daniel Hausmann. Faster game solving by fixpoint acceleration. In Fixed Points in Computer Science, FICS 2024, EPTCS, 2024, to appear. Google Scholar
  15. Daniel Hausmann, Mathieu Lehaut, and Nir Piterman. Symbolic solution of Emerson-Lei games for reactive synthesis. In Foundations of Software Science and Computation Structures, FoSSaCS 2024, volume 14574 of LNCS, pages 55-78. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57228-9_4.
  16. Daniel Hausmann and Lutz Schröder. Game-based local model checking for the coalgebraic μ-calculus. In Concurrency Theory, CONCUR 2019, volume 140 of LIPIcs, pages 35:1-35:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPICS.CONCUR.2019.35.
  17. Paul Hunter and Anuj Dawar. Complexity bounds for regular games. In Mathematical Foundations of Computer Science, MFCS 2005, volume 3618 of Lecture Notes in Computer Science, pages 495-506. Springer, 2005. URL: https://doi.org/10.1007/11549345_43.
  18. Michael Luttenberger, Philipp J. Meyer, and Salomon Sickert. Practical synthesis of reactive systems from LTL specifications via parity games. Acta Informatica, 57(1-2):3-36, 2020. URL: https://doi.org/10.1007/s00236-019-00349-3.
  19. Rupak Majumdar, Nir Piterman, and Anne-Kathrin Schmuck. Environmentally-friendly GR(1) synthesis. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2019, volume 11428 of LNCS, pages 229-246. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17465-1_13.
  20. Rupak Majumdar and Anne-Kathrin Schmuck. Supervisory controller synthesis for nonterminating processes is an obliging game. IEEE Trans. Autom. Control., 68(1):385-392, 2023. URL: https://doi.org/10.1109/TAC.2022.3143108.
  21. Donald A. Martin. Borel determinacy. Annals of Mathematics, 102(2):363-371, 1975. URL: https://doi.org/10.2307/1971035.
  22. Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. In Principles of Programming Languages, POPL 1989, pages 179-190. ACM Press, 1989. URL: https://doi.org/10.1145/75277.75293.
  23. Tom van Dijk, Feije van Abbema, and Naum Tomov. Knor: reactive synthesis using oink. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, volume 14570 of LNCS, pages 103-122. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57246-3_7.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact