Document Open Access Logo

Two-Player Boundedness Counter Games

Authors Emmanuel Filiot, Edwin Hamel-de le Court

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2022.21.pdf
  • Filesize: 0.88 MB
  • 23 pages

Document Identifiers

Author Details

Emmanuel Filiot
  • Université libre de Bruxelles, Belgium
Edwin Hamel-de le Court
  • Université libre de Bruxelles, Belgium

Funding

This work was supported by the Fonds de la Recherche Scientifique – F.R.S.-FNRS under the MIS project F451019F. Emmanuel Filiot is a senior research associate at F.R.S.-FNRS.

Acknowledgements

We warmly thank Jean-François Raskin for his valuable inputs.

Cite AsGet BibTex

Emmanuel Filiot and Edwin Hamel-de le Court. Two-Player Boundedness Counter Games. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 21:1-21:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CONCUR.2022.21

Abstract

We consider two-player zero-sum games with winning objectives beyond regular languages, expressed as a parity condition in conjunction with a Boolean combination of boundedness conditions on a finite set of counters which can be incremented, reset to 0, but not tested. A boundedness condition requires that a given counter is bounded along the play. Such games are decidable, though with non-optimal complexity, by an encoding into the logic WMSO with the unbounded and path quantifiers, which is known to be decidable over infinite trees. Our objective is to give tight or tighter complexity results for particular classes of counter games with boundedness conditions, and study their strategy complexity. In particular, counter games with conjunction of boundedness conditions are easily seen to be equivalent to Streett games, so, they are CoNP-c. Moreover, finite-memory strategies suffice for Eve and memoryless strategies suffice for Adam. For counter games with a disjunction of boundedness conditions, we prove that they are in solvable in NP∩CoNP, and in PTime if the parity condition is fixed. In that case memoryless strategies suffice for Eve while infinite memory strategies might be necessary for Adam. Finally, we consider an extension of those games with a max operation. In that case, the complexity increases: for conjunctions of boundedness conditions, counter games are EXPTIME-c.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Automata over infinite objects
Keywords
  • Controller synthesis
  • Game theory
  • Counter Games
  • Boundedness objectives

Metrics

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

Related Versions

References

  1. Nathalie Bertrand, Miheer Dewaskar, Blaise Genest, Hugo Gimbert, and Adwait Amit Godbole. Controlling a population. Log. Methods Comput. Sci., 15(3), 2019. URL: https://doi.org/10.23638/LMCS-15(3:6)2019.
  2. Roderick Bloem, Krishnendu Chatterjee, and Barbara Jobstmann. Graph games and reactive synthesis. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 921-962. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_27.
  3. Mikolaj Bojanczyk. Weak MSO with the unbounding quantifier. Theory Comput. Syst., 48(3):554-576, 2011. URL: https://doi.org/10.1007/s00224-010-9279-2.
  4. Mikolaj Bojanczyk. Weak MSO with the unbounding quantifier. Theory Comput. Syst., 48(3):554-576, 2011. Google Scholar
  5. Mikolaj Bojanczyk. Weak MSO+U with path quantifiers over infinite trees. In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias, editors, Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II, volume 8573 of Lecture Notes in Computer Science, pages 38-49. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-43951-7_4.
  6. Mikolaj Bojanczyk and Thomas Colcombet. Bounds in w-regularity. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 285-296. IEEE Computer Society, 2006. URL: https://doi.org/10.1109/LICS.2006.17.
  7. Mikolaj Bojanczyk, Tomasz Gogacz, Henryk Michalewski, and Michal Skrzypczak. On the decidability of MSO+U on infinite trees. In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias, editors, Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II, volume 8573 of Lecture Notes in Computer Science, pages 50-61. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-43951-7_5.
  8. Mikolaj Bojanczyk and Szymon Torunczyk. Deterministic automata and extensions of weak MSO. In Ravi Kannan and K. Narayan Kumar, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2009, December 15-17, 2009, IIT Kanpur, India, volume 4 of LIPIcs, pages 73-84. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2009. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2009.2308.
  9. Véronique Bruyère. Computer aided synthesis: A game-theoretic approach. In Émilie Charlier, Julien Leroy, and Michel Rigo, editors, Developments in Language Theory - 21st International Conference, DLT 2017, Liège, Belgium, August 7-11, 2017, Proceedings, volume 10396 of Lecture Notes in Computer Science, pages 3-35. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-62809-7_1.
  10. Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasipolynomial time. In STOC, pages 252-263, 2017. Google Scholar
  11. Krishnendu Chatterjee and Nathanaël Fijalkow. Infinite-state games with finitary conditions. In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy, volume 23 of LIPIcs, pages 181-196. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. URL: https://doi.org/10.4230/LIPIcs.CSL.2013.181.
  12. Krishnendu Chatterjee, Thomas A. Henzinger, and Florian Horn. Finitary winning in omega-regular games. ACM Trans. Comput. Log., 11(1):1:1-1:27, 2009. URL: https://doi.org/10.1145/1614431.1614432.
  13. Krishnendu Chatterjee, Thomas A. Henzinger, and Florian Horn. The complexity of request-response games. In LATA, volume 6638, pages 227-237, 2011. Google Scholar
  14. Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Generalized parity games. In Helmut Seidl, editor, Foundations of Software Science and Computational Structures, 10th International Conference, FOSSACS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24-April 1, 2007, Proceedings, volume 4423 of Lecture Notes in Computer Science, pages 153-167. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-71389-0_12.
  15. Thomas Colcombet and Christof Löding. The non-deterministic mostowski hierarchy and distance-parity automata. In Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz, editors, Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part II - Track B: Logic, Semantics, and Theory of Programming & Track C: Security and Cryptography Foundations, volume 5126 of Lecture Notes in Computer Science, pages 398-409. Springer, 2008. Google Scholar
  16. Hubert Comon, Max Dauchet, Rémi Gilleron, Florent Jacquemard, Denis Lugiez, Christof Löding, Sophie Tison, and Marc Tommasi. Tree Automata Techniques and Applications, 2008. URL: https://hal.inria.fr/hal-03367725.
  17. E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). In 32nd Annual Symposium on Foundations of Computer Science, San Juan, Puerto Rico, 1-4 October 1991, pages 368-377. IEEE Computer Society, 1991. Google Scholar
  18. E. Allen Emerson and Charanjit S. Jutla. The complexity of tree automata and logics of programs. SIAM J. Comput., 29(1):132-158, 1999. Google Scholar
  19. Léo Exibard, Emmanuel Filiot, and Ayrat Khalimov. Church synthesis on register automata over linearly ordered data domains. In Markus Bläser and Benjamin Monmege, editors, 38th International Symposium on Theoretical Aspects of Computer Science, STACS 2021, March 16-19, 2021, Saarbrücken, Germany (Virtual Conference), volume 187 of LIPIcs, pages 28:1-28:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  20. Nathanaël Fijalkow and Martin Zimmermann. Cost-parity and cost-streett games. In Deepak D'Souza, Telikepalli Kavitha, and Jaikumar Radhakrishnan, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012, December 15-17, 2012, Hyderabad, India, volume 18 of LIPIcs, pages 124-135. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2012.124.
  21. Emmanuel Filiot and Edwin Hamel-de Le Court. Two-player Boundedness Counter Games. working paper or preprint, March 2022. URL: https://doi.org/10.4230/LIPIcs.
  22. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata Logics, and Infinite Games: A Guide to Current Research. Springer-Verlag, Berlin, Heidelberg, 2002. Google Scholar
  23. Orna Kupferman, Nir Piterman, and Moshe Y. Vardi. Pushdown specifications. In LPAR, volume 2514, pages 262-277, 2002. Google Scholar
  24. Donald A. Martin. Borel determinacy. Annals of Mathematics, 102(2):363-371, 1975. Google Scholar
  25. Nir Piterman and Amir Pnueli. Faster solutions of rabin and streett games. In LICS, pages 275-284, 2006. Google Scholar
  26. Martin Zimmermann. Delay games with WMSO+U winning conditions. RAIRO Theor. Informatics Appl., 50(2):145-165, 2016. URL: https://doi.org/10.1051/ita/2016018.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact