Document Open Access Logo

Extending Finite-Memory Determinacy by Boolean Combination of Winning Conditions

Authors Stéphane Le Roux, Arno Pauly, Mickael Randour

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2018.38.pdf
  • Filesize: 482 kB
  • 20 pages

Document Identifiers

Author Details

Stéphane Le Roux
  • LSV, CNRS & ENS Cachan, Université Paris-Saclay, Cachan, France
Arno Pauly
  • Swansea University, Swansea, United Kingdom
Mickael Randour
  • F.R.S.-FNRS & UMONS - Université de Mons, Mons, Belgium

Funding

Research partially supported by F.R.S.-FNRS under Grant n° F.4520.18 (ManySynth).
  • Randour, Mickael: F.R.S.-FNRS Research Associate.

Cite AsGet BibTex

Stéphane Le Roux, Arno Pauly, and Mickael Randour. Extending Finite-Memory Determinacy by Boolean Combination of Winning Conditions. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 38:1-38:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSTTCS.2018.38

Abstract

We study finite-memory (FM) determinacy in games on finite graphs, a central question for applications in controller synthesis, as FM strategies correspond to implementable controllers. We establish general conditions under which FM strategies suffice to play optimally, even in a broad multi-objective setting. We show that our framework encompasses important classes of games from the literature, and permits to go further, using a unified approach. While such an approach cannot match ad-hoc proofs with regard to tightness of memory bounds, it has two advantages: first, it gives a widely-applicable criterion for FM determinacy; second, it helps to understand the cornerstones of FM determinacy, which are often hidden but common in proofs for specific (combinations of) winning conditions.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • games on graphs
  • finite-memory determinacy
  • multiple objectives

Metrics

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

Related Versions

References

  1. 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: http://dx.doi.org/10.1007/978-3-319-10575-8_27.
  2. Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey, and Jiří Srba. Infinite Runs in Weighted Timed Automata with Energy Constraints. In Franck Cassez and Claude Jard, editors, Formal Modeling and Analysis of Timed Systems, volume 5215 of Lecture Notes in Computer Science, pages 33-47. Springer Berlin Heidelberg, 2008. URL: http://dx.doi.org/10.1007/978-3-540-85778-5_4.
  3. Patricia Bouyer, Piotr Hofman, Nicolas Markey, Mickael Randour, and Martin Zimmermann. Bounding Average-Energy Games. In Javier Esparza and Andrzej S. Murawski, editors, Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 179-195, 2017. URL: http://dx.doi.org/10.1007/978-3-662-54458-7_11.
  4. Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim G. Larsen, and Simon Laursen. Average-energy games. Acta Inf., 55(2):91-127, 2018. URL: http://dx.doi.org/10.1007/s00236-016-0274-1.
  5. Romain Brenguier, Lorenzo Clemente, Paul Hunter, Guillermo A. Pérez, Mickael Randour, Jean-François Raskin, Ocan Sankur, and Mathieu Sassolas. Non-Zero Sum Games for Reactive Synthesis. In Adrian-Horia Dediu, Jan Janousek, Carlos Martín-Vide, and Bianca Truthe, editors, Language and Automata Theory and Applications - 10th International Conference, LATA 2016, Prague, Czech Republic, March 14-18, 2016, Proceedings, volume 9618 of Lecture Notes in Computer Science, pages 3-23. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-30000-9_1.
  6. Véronique Bruyère, Quentin Hautem, and Mickael Randour. Window parity games: an alternative approach toward parity games with time bounds. In Domenico Cantone and Giorgio Delzanno, editors, Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016, Catania, Italy, 14-16 September 2016., volume 226 of EPTCS, pages 135-148, 2016. URL: http://dx.doi.org/10.4204/EPTCS.226.10.
  7. Véronique Bruyère, Quentin Hautem, and Jean-François Raskin. On the Complexity of Heterogeneous Multidimensional Games. In Josée Desharnais and Radha Jagadeesan, editors, 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada, volume 59 of LIPIcs, pages 11:1-11:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2016.11.
  8. Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, and Mariëlle Stoelinga. Resource Interfaces. In Rajeev Alur and Insup Lee, editors, EMSOFT, volume 2855 of Lecture Notes in Computer Science, pages 117-133. Springer, 2003. URL: http://dx.doi.org/10.1007/978-3-540-45212-6_9.
  9. Krishnendu Chatterjee and Laurent Doyen. Energy parity games. Theor. Comput. Sci., 458:49-60, 2012. URL: http://dx.doi.org/10.1016/j.tcs.2012.07.038.
  10. Krishnendu Chatterjee, Laurent Doyen, Mickael Randour, and Jean-François Raskin. Looking at mean-payoff and total-payoff through windows. Inf. Comput., 242:25-52, 2015. URL: http://dx.doi.org/10.1016/j.ic.2015.03.010.
  11. Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdzinski. Mean-Payoff Parity Games. In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings, pages 178-187. IEEE Computer Society, 2005. URL: http://dx.doi.org/10.1109/LICS.2005.26.
  12. 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: http://dx.doi.org/10.1007/978-3-540-71389-0_12.
  13. Krishnendu Chatterjee, Mickael Randour, and Jean-François Raskin. Strategy synthesis for multi-dimensional quantitative objectives. Acta Inf., 51(3-4):129-163, 2014. URL: http://dx.doi.org/10.1007/s00236-013-0182-6.
  14. Stefan Dziembowski, Marcin Jurdzinski, and Igor Walukiewicz. How Much Memory is Needed to Win Infinite Games? In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997, pages 99-110. IEEE Computer Society, 1997. URL: http://dx.doi.org/10.1109/LICS.1997.614939.
  15. Andrzej Ehrenfeucht and Jan Mycielski. Positional Strategies for Mean Payoff Games. Int. Journal of Game Theory, 8(2):109-113, 1979. Google Scholar
  16. Hugo Gimbert and Wieslaw Zielonka. When Can You Play Positionally? In Jirí Fiala, Václav Koubek, and Jan Kratochvíl, editors, Mathematical Foundations of Computer Science 2004, 29th International Symposium, MFCS 2004, Prague, Czech Republic, August 22-27, 2004, Proceedings, volume 3153 of Lecture Notes in Computer Science, pages 686-697. Springer, 2004. URL: http://dx.doi.org/10.1007/978-3-540-28629-5_53.
  17. Hugo Gimbert and Wieslaw Zielonka. Games Where You Can Play Optimally Without Any Memory. In Martín Abadi and Luca de Alfaro, editors, CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings, volume 3653 of Lecture Notes in Computer Science, pages 428-442. Springer, 2005. URL: http://dx.doi.org/10.1007/11539452_33.
  18. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001], volume 2500 of Lecture Notes in Computer Science. Springer, 2002. URL: http://dx.doi.org/10.1007/3-540-36387-4.
  19. Marcin Jurdzinski, Ranko Lazic, and Sylvain Schmitz. Fixed-Dimensional Energy Games are in Pseudo-Polynomial Time. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 260-272. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-47666-6_21.
  20. Eryk Kopczynski. Half-Positional Determinacy of Infinite Games. In Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo Wegener, editors, Automata, Languages and Programming, 33rd International Colloquium, ICALP 2006, Venice, Italy, July 10-14, 2006, Proceedings, Part II, volume 4052 of Lecture Notes in Computer Science, pages 336-347. Springer, 2006. URL: http://dx.doi.org/10.1007/11787006_29.
  21. Donald A. Martin. Borel determinacy. Annals of Mathematics, 102(2):363-371, 1975. Google Scholar
  22. Mickael Randour. Automated Synthesis of Reliable and Efficient Systems Through Game Theory: A Case Study. In Proc. of ECCS 2012, Springer Proceedings in Complexity XVII, pages 731-738. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-319-00395-5_90.
  23. Stéphane Le Roux and Arno Pauly. Extending finite-memory determinacy to multi-player games. Inf. Comput., 261(Part):676-694, 2018. URL: http://dx.doi.org/10.1016/j.ic.2018.02.024.
  24. Stéphane Le Roux, Arno Pauly, and Mickael Randour. Extending finite-memory determinacy by Boolean combination of winning conditions. CoRR, abs/1808.05791, 2018. URL: http://arxiv.org/abs/1808.05791.
  25. Yaron Velner. Robust Multidimensional Mean-Payoff Games are Undecidable. In Andrew M. Pitts, editor, Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, volume 9034 of Lecture Notes in Computer Science, pages 312-327. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-46678-0_20.
  26. Yaron Velner, Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Alexander Moshe Rabinovich, and Jean-François Raskin. The complexity of multi-mean-payoff and multi-energy games. Inf. Comput., 241:177-196, 2015. URL: http://dx.doi.org/10.1016/j.ic.2015.03.001.
  27. Wieslaw Zielonka. Infinite Games on Finitely Coloured Graphs with Applications to Automata on Infinite Trees. Theor. Comput. Sci., 200(1-2):135-183, 1998. URL: http://dx.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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact