Document Open Access Logo

Positional-Player Games

Authors Orna Kupferman , Noam Shenwald

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2025.64.pdf
  • Filesize: 0.79 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Semantics and reasoning
Keywords
  • Games
  • ω-Regular Objectives
  • Memory
  • Complexity

Metrics

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

Abstract

In reactive synthesis, we transform a specification to a system that satisfies the specification in all environments. For specifications in linear-temporal logic, research on bounded synthesis, where the sizes of the system and the environment are bounded, captures realistic settings and has lead to algorithms of improved complexity and implementability. In the game-based {a}pproach to synthesis, the system and its environment are modeled by strategies in a two-player game with an ω-regular objective, induced by the specification. There, bounded synthesis corresponds to bounding the memory of the strategies of the players. The memory requirement for various objectives has been extensively studied. In particular, researchers have identified positional objectives, where the winning player can follow a memoryless strategy - one that needs no memory.
In this work we study bounded synthesis in the game setting. Specifically, we define and study positional-player games, in which one or both players are restricted to memoryless strategies, which correspond to non-intrusive control in various applications. We study positional-player games with Rabin, Streett, and Muller objectives, as well as with weighted multiple Büchi and reachability objectives. Our contribution covers their theoretical properties as well as a complete picture of the complexity of deciding the game in the various settings.

Cite As Get BibTex

Orna Kupferman and Noam Shenwald. Positional-Player Games. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 64:1-64:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.MFCS.2025.64

Author Details

Orna Kupferman
  • School of Engineering and Computer Science, Hebrew University, Jerusalem, Israel
Noam Shenwald
  • School of Engineering and Computer Science, Hebrew University, Jerusalem, Israel

References

  1. B. Abu Radi and O. Kupferman. Minimization and canonization of GFG transition-based automata. Log. Methods Comput. Sci., 18(3), 2022. URL: https://doi.org/10.46298/LMCS-18(3:16)2022.
  2. B. Abu Radi, O. Kupferman, and O. Leshkowitz. A hierarchy of nondeterminism. In 46th Int. Symp. on Mathematical Foundations of Computer Science, volume 202 of LIPIcs, pages 85:1-85:21, 2021. URL: https://doi.org/10.4230/LIPICS.MFCS.2021.85.
  3. B. Aminof, O. Kupferman, and R. Lampert. Formal analysis of online algorithms. In 9th Int. Symp. on Automated Technology for Verification and Analysis, volume 6996 of Lecture Notes in Computer Science, pages 213-227. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-24372-1_16.
  4. T. Babiak, F. Blahoudek, A. Duret-Lutz, J. Klein, J. Kretínský, D. Müller, D. Parker, and J. Strejcek. The hanoi omega-automata format. In Proc. 27th Int. Conf. on Computer Aided Verification, volume 9206 of Lecture Notes in Computer Science, pages 479-486. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21690-4_31.
  5. C. Beeri. On the membership problem for functional and multivalued dependencies in relational databases. ACM Trans. on Database Systems, 5:241-259, 1980. URL: https://doi.org/10.1145/320613.320614.
  6. U. Boker. On the (in)succinctness of muller automata. In Proc. 26th Annual Conf. of the European Association for Computer Science Logic, volume 82 of LIPIcs, pages 12:1-12:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPICS.CSL.2017.12.
  7. P. Bouyer, A. Casares, M Randour, and P. Vandenhove. Half-Positional Objectives Recognized by Deterministic Büchi Automata. In Proc. 33rd Int. Conf. on Concurrency Theory, volume 243 of Leibniz International Proceedings in Informatics (LIPIcs), pages 20:1-20:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.CONCUR.2022.20.
  8. P. Bouyer, Fijalkow N, M. Randour, and P. Vandenhove. How to play optimally for regular objectives?, 2023. URL: https://doi.org/10.4230/LIPICS.ICALP.2023.118.
  9. N. Bulling and V. Goranko. Combining quantitative and qualitative reasoning in concurrent multi-player games. In Proceedings of the 21st International Conference on Autonomous Agents and Multiagent Systems, page 1926?1928. International Foundation for Autonomous Agents and Multiagent Systems, 2022. Google Scholar
  10. A. Casares. On the minimisation of transition-based rabin automata and the chromatic memory requirements of muller conditions. In Proc. 30th Annual Conf. of the European Association for Computer Science Logic, volume 216 of LIPIcs, pages 12:1-12:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.CSL.2022.12.
  11. A. Casares and P. Ohlmann. Positional ω-regular languages. In Proc. 39th ACM/IEEE Symp. on Logic in Computer Science. Association for Computing Machinery, 2024. Google Scholar
  12. K. Chatterjee, W. Dvorak, M. Henzinger, and V. Loitzenbauer. Conditionally optimal algorithms for generalized büchi games. In 41st Int. Symp. on Mathematical Foundations of Computer Science, volume 58 of LIPIcs, pages 25:1-25:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPICS.MFCS.2016.25.
  13. K. Chatterjee, R. Majumdar, and M. Jurdzinski. On Nash equilibria in stochastic games. In Proc. 13th Annual Conf. of the European Association for Computer Science Logic, volume 3210 of Lecture Notes in Computer Science, pages 26-40. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30124-0_6.
  14. T. Colcombet and D. Niwiński. On the positional determinacy of edge-labeled games. Theoretical Computer Science, 352(1):190-196, 2006. URL: https://doi.org/10.1016/J.TCS.2005.10.046.
  15. R. Condurache, E. Filiot, R. Gentilini, and J.-F. Raskin. The complexity of rational synthesis. In Proc. 43th Int. Colloq. on Automata, Languages, and Programming, volume 55 of LIPIcs, pages 121:1-121:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPICS.ICALP.2016.121.
  16. F. Delgrange, J.P. Katoen, T. Quatmann, and M. Randour. Simple strategies in multi-objective mdps. In Proc. 26th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, pages 346-364. Springer International Publishing, 2020. Google Scholar
  17. J. Dubreil, Ph. Darondeau, and H. Marchand. Supervisory control for opacity. IEEE Transactions on Automatic Control, 55(5):1089-1100, 2010. URL: https://doi.org/10.1109/TAC.2010.2042008.
  18. S. Dziembowski, M. Jurdzinski, and I. Walukiewicz. How much memory is needed to win infinite games. In Proc. 12th ACM/IEEE Symp. on Logic in Computer Science, pages 99-110, 1997. Google Scholar
  19. R. Ehlers. Symbolic bounded synthesis. In Proc. 22nd Int. Conf. on Computer Aided Verification, volume 6174 of Lecture Notes in Computer Science, pages 365-379. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14295-6_33.
  20. E.A. Emerson and C. Jutla. The complexity of tree automata and logics of programs. In Proc. 29th IEEE Symp. on Foundations of Computer Science, pages 328-337, 1988. Google Scholar
  21. E.A. Emerson and C. Jutla. Tree automata, μ-calculus and determinacy. In Proc. 32nd IEEE Symp. on Foundations of Computer Science, pages 368-377, 1991. Google Scholar
  22. E. Filiot, N. Jin, and J.-F. Raskin. An antichain algorithm for LTL realizability. In Proc. 21st Int. Conf. on Computer Aided Verification, volume 5643, pages 263-277, 2009. URL: https://doi.org/10.1007/978-3-642-02658-4_22.
  23. D. Fisman, O. Kupferman, and Y. Lustig. Rational synthesis. In Proc. 16th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 6015 of Lecture Notes in Computer Science, pages 190-204. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12002-2_16.
  24. S. Fortune, J. Hopcroft, and J. Wyllie. The directed subgraph homeomorphism problem. Theoretical Computer Science, 10(2):111-121, 1980. URL: https://doi.org/10.1016/0304-3975(80)90009-2.
  25. H. Gimbert and W. Zielonka. Games where you can play optimally without any memory. In Proc. 16th Int. Conf. on Concurrency Theory, volume 3653 of Lecture Notes in Computer Science, pages 428-442, 2005. URL: https://doi.org/10.1007/11539452_33.
  26. E. Grädel. Positional determinacy of infinite games. In Proc. 21st Symp. on Theoretical Aspects of Computer Science, volume 2996 of Lecture Notes in Computer Science, pages 4-18, 2004. URL: https://doi.org/10.1007/978-3-540-24749-4_2.
  27. D. Harel, G. Katz, A. Marron, and G. Weiss. Non-intrusive repair of reactive programs. In 17th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2012, Paris, France, July 18-20, 2012, pages 3-12. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/ICECCS.2012.25.
  28. D. Harel and A. Pnueli. On the development of reactive systems. In K. Apt, editor, Logics and Models of Concurrent Systems, volume F-13 of NATO Advanced Summer Institutes, pages 477-498. Springer, 1985. Google Scholar
  29. C. Hugenroth. Zielonka dag acceptance and regular languages over infinite words. In Developments in Language Theory, pages 143-155. Springer Nature Switzerland, 2023. Google Scholar
  30. P. Hunter and A. Dawar. Complexity bounds for regular games. In 30th Int. Symp. on Mathematical Foundations of Computer Science, volume 3618, pages 495-506. Springer, 2005. URL: https://doi.org/10.1007/11549345_43.
  31. P. Hunter, G.A. Pérez, and J.F. Raskin. Reactive synthesis without regret. In Proc. 26th Int. Conf. on Concurrency Theory, volume 42 of Leibniz International Proceedings in Informatics (LIPIcs), pages 114-127. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPICS.CONCUR.2015.114.
  32. N. Immerman. Number of quantifiers is better than number of tape cells. Journal of Computer and Systems Science, 22(3):384-406, 1981. URL: https://doi.org/10.1016/0022-0000(81)90039-8.
  33. B. Jobstmann, A. Griesmayer, and R. Bloem. Program repair as a game. In Proc. 17th Int. Conf. on Computer Aided Verification, volume 3576 of Lecture Notes in Computer Science, pages 226-238, 2005. URL: https://doi.org/10.1007/11513988_23.
  34. M. Jurdzinski. Deciding the winner in parity games is in UP ∩ co-UP. Information Processing Letters, 68(3):119-124, 1998. Google Scholar
  35. N. Klarlund. Progress measures, immediate determinacy, and a subset construction for tree automata. Annals of Pure and Applied Logic, 69(2):243-268, 1994. URL: https://doi.org/10.1016/0168-0072(94)90086-8.
  36. E. Kopczyński. Half-positional determinacy of infinite games. In Proc. 33rd Int. Colloq. on Automata, Languages, and Programming, volume 4052 of Lecture Notes in Computer Science, pages 336-347. Springer, 2006. URL: https://doi.org/10.1007/11787006_29.
  37. D. Kuperberg and A. Majumdar. Width of non-deterministic automata. In Proc. 35th Symp. on Theoretical Aspects of Computer Science, volume 96 of LIPIcs, pages 47:1-47:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPICS.STACS.2018.47.
  38. O. Kupferman, Y. Lustig, M.Y. Vardi, and M. Yannakakis. Temporal synthesis for bounded systems and environments. In Proc. 28th Symp. on Theoretical Aspects of Computer Science, pages 615-626, 2011. Google Scholar
  39. O. Kupferman and N. Shenwald. Games with trading of control. In Proc. 34th Int. Conf. on Concurrency Theory, volume 279 of Leibniz International Proceedings in Informatics (LIPIcs), pages 19:1-19:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.CONCUR.2023.19.
  40. O. Kupferman and N. Shenwald. Games with weighted multiple objectives. In 22nd Int. Symp. on Automated Technology for Verification and Analysis, Lecture Notes in Computer Science. Springer, 2024. Google Scholar
  41. D.A. Martin. Borel determinacy. Annals of Mathematics, 65:363-371, 1975. Google Scholar
  42. S. Nain and M.Y. Vardi. Solving partial-information stochastic parity games. In Proc. 28th ACM/IEEE Symp. on Logic in Computer Science, pages 341-348. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/LICS.2013.40.
  43. N. Nisan, T. Roughgarden, E. Tardos, and V.V. Vazirani. Algorithmic Game Theory. Cambridge University Press, 2007. Google Scholar
  44. P. Ohlmann. Characterizing positionality in games of infinite duration over infinite graphs. In Proc. 37th ACM/IEEE Symp. on Logic in Computer Science. Association for Computing Machinery, 2022. Google Scholar
  45. P. Ohlmann and M. Skrzypczak. Positionality in Σ₀² and a completeness result, 2024. URL: https://arxiv.org/abs/2309.17022.
  46. A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proc. 16th ACM Symp. on Principles of Programming Languages, pages 179-190, 1989. Google Scholar
  47. D. Raju, R. Ehlers, and U. Topcu. Playing against opponents with limited memory. CoRR, abs/2002.07274, 2020. URL: https://arxiv.org/abs/2002.07274.
  48. D. Raju, R. Ehlers, and U. Topcu. Adapting to the behavior of environments with bounded memory. In Proc. 12th International Symposium on Games, Automata, Logics and Formal Verification, 2021. Google Scholar
  49. S. Schewe. Minimising good-for-games automata is NP-complete. In Proc. 40th Conf. on Foundations of Software Technology and Theoretical Computer Science, volume 182 of LIPIcs, pages 56:1-56:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPICS.FSTTCS.2020.56.
  50. S. Schewe and B. Finkbeiner. Bounded synthesis. In 5th Int. Symp. on Automated Technology for Verification and Analysis, volume 4762 of Lecture Notes in Computer Science, pages 474-488. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-75596-8_33.
  51. W. Thomas. On the synthesis of strategies in infinite games. In Proc. 12th Symp. on Theoretical Aspects of Computer Science, volume 900 of Lecture Notes in Computer Science, pages 1-13. Springer, 1995. URL: https://doi.org/10.1007/3-540-59042-0_57.
  52. M. Ummels. The complexity of Nash equilibria in infinite multiplayer games. In Proc. 11th Int. Conf. on Foundations of Software Science and Computation Structures, pages 20-34, 2008. Google Scholar
  53. M.Y. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. Journal of Computer and Systems Science, 32(2):182-221, 1986. URL: https://doi.org/10.1016/0022-0000(86)90026-7.
  54. J. von Neumann and O. Morgenstern. Theory of games and economic behavior. Princeton University Press, 1953. Google Scholar
  55. W. Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science, 200(1-2):135-183, 1998. URL: https://doi.org/10.1016/S0304-3975(98)00009-7.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact