Document Open Access Logo

Playing Safe

Authors Thomas Colcombet, Nathanael Fijalkow, Florian Horn

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2014.379.pdf
  • Filesize: 455 kB
  • 12 pages

Document Identifiers

Author Details

Thomas Colcombet
Nathanael Fijalkow
Florian Horn

Cite As Get BibTex

Thomas Colcombet, Nathanael Fijalkow, and Florian Horn. Playing Safe. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 379-390, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014) https://doi.org/10.4230/LIPIcs.FSTTCS.2014.379

Abstract

We consider two-player games over graphs and give tight bounds on the memory size of strategies ensuring safety conditions. More specifically, we show that the minimal number of memory states of a strategy ensuring a safety condition is given by the size of the maximal antichain of left quotients with respect to language inclusion. This result holds for all safety conditions without any regularity assumptions, and for all (finite or infinite) graphs of finite degree.

We give several applications of this general principle. In particular, we characterize the exact memory requirements for the opponent in generalized reachability games, and we prove the existence of positional strategies in games with counters.

Subject Classification

Keywords
  • Game Theory
  • Synthesis
  • Safety Specifications
  • Program Verification

Metrics

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

References

  1. Patricia Bouyer, Ulrich Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, and Jirí Srba. Infinite runs in weighted timed automata with energy constraints. In Franck Cassez and Claude Jard, editors, FORMATS, volume 5215 of Lecture Notes in Computer Science, pages 33-47. Springer, 2008. Google Scholar
  2. 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. Google Scholar
  3. Krishnendu Chatterjee and Laurent Doyen. Energy parity games. Theor. Comput. Sci., 458:49-60, 2012. Google Scholar
  4. Thomas Colcombet. Regular cost functions, part I: Logic and algebra over words. Logical Methods in Computer Science, 9(3), 2013. Google Scholar
  5. Stefan Dziembowski, Marcin Jurdziński, and Igor Walukiewicz. How much memory is needed to win infinite games? In LICS, pages 99-110. IEEE Computer Society, 1997. Google Scholar
  6. Nathanaël Fijalkow and Florian Horn. The surprizing complexity of reachability games. CoRR, abs/1010.2420, 2010. Google Scholar
  7. Nathanaël Fijalkow and Florian Horn. Les jeux d'accessibilité généralisée. Technique et Science Informatiques, 32(9-10):931-949, 2013. Google Scholar
  8. Hugo Gimbert. Jeux Positionnels. PhD thesis, Université Paris 7, 2007. Google Scholar
  9. 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. Google Scholar
  10. Eryk Kopczyński. Personal communication. Google Scholar
  11. Eryk Kopczyński. Half-Positional Determinacy of Infinite Games. PhD thesis, University of Warsaw, 2009. Google Scholar
  12. Orna Kupferman. Variations on safety. In Erika Ábrahám and Klaus Havelund, editors, TACAS, volume 8413 of Lecture Notes in Computer Science, pages 1-14. Springer, 2014. Google Scholar
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 About DROPS Imprint Privacy Contact