Document Open Access Logo

Optimal Strategies in Pushdown Reachability Games

Authors Arnaud Carayol, Matthew Hague

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2018.42.pdf
  • Filesize: 456 kB
  • 14 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
Keywords
  • Pushdown Systems
  • Reachability Games
  • Optimal Strategies
  • Formal Methods
  • Context Free

Metrics

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

Abstract

An algorithm for computing optimal strategies in pushdown reachability games was given by Cachat. We show that the information tracked by this algorithm is too coarse and the strategies constructed are not necessarily optimal. We then show that the algorithm can be refined to recover optimality. Through a further non-trivial argument the refined algorithm can be run in 2EXPTIME by bounding the play-lengths tracked to those that are at most doubly exponential. This is optimal in the sense that there exists a game for which the optimal strategy requires a doubly exponential number of moves to reach a target configuration.

Cite As Get BibTex

Arnaud Carayol and Matthew Hague. Optimal Strategies in Pushdown Reachability Games. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 42:1-42:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.MFCS.2018.42

Author Details

Arnaud Carayol
  • Université Paris-Est, LIGM (UMR 8049), CNRS, ENPC, ESIEE Paris, UPEM, France
Matthew Hague
  • Royal Holloway, University of London, UK

Funding

  • Carayol, Arnaud: Supported by the French National Research Agency (ANR), through the excellence program Bézout (ANR-10-LABX-58).
  • Hague, Matthew: Supported by EPSRC [EP/K009907/1].

References

  1. A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In CONCUR, pages 135-150, 1997. Google Scholar
  2. R. J Büchi. Regular canonical systems. Archive for Mathematical Logic, 6(3):91-111, 1964. URL: http://dx.doi.org/10.1007/BF01969548.
  3. T. Cachat. Symbolic strategy synthesis for games on pushdown graphs. In ICALP, pages 704-715, 2002. URL: http://dx.doi.org/10.1007/3-540-45465-9_60.
  4. T. Cachat. Games on Pushdown Graphs and Extensions. PhD thesis, RWTH Aachen, 2003. URL: http://darwin.bth.rwth-aachen.de/opus3/volltexte/2004/957/pdf/Cachat_Thierry.pdf.
  5. Arnaud Carayol and Matthew Hague. Regular strategies in pushdown reachability games. In Reachability Problems - 8th International Workshop, RP 2014, Oxford, UK, September 22-24, 2014. Proceedings, pages 58-71, 2014. URL: http://dx.doi.org/10.1007/978-3-319-11439-2_5.
  6. D. Caucal. Récritures suffixes de mots. Research Report RR-0871, INRIA, 1988. Google Scholar
  7. A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model checking pushdown systems. In INFINITY, volume 9, pages 27-37, 1997. Google Scholar
  8. Wladimir Fridman. Formats of winning strategies for six types of pushdown games. In Proceedings First Symposium on Games, Automata, Logic, and Formal Verification, GANDALF 2010, Minori (Amalfi Coast), Italy, 17-18th June 2010., pages 132-145, 2010. URL: http://dx.doi.org/10.4204/EPTCS.25.14.
  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. URL: http://dx.doi.org/10.1007/3-540-36387-4.
  10. N. D. Jones and S. S. Muchnick. Even simple programs are hard to analyze. J. ACM, 24:338-350, April 1977. URL: http://dx.doi.org/10.1145/322003.322016.
  11. O. Kupferman, N. Piterman, and M. Y. Vardi. An automata-theoretic approach to infinite-state systems. In Essays in Memory of Amir Pnueli, pages 202-259, 2010. URL: http://dx.doi.org/10.1007/978-3-642-13754-9_11.
  12. N. Piterman and M. Y. Vardi. Global model-checking of infinite-state systems. In CAV, pages 387-400, 2004. Google Scholar
  13. S. Schwoon. Model-checking Pushdown Systems. PhD thesis, Technical University of Munich, 2002. Google Scholar
  14. O. Serre. Contribution à l’étude des jeux sur des graphes de processus à pile. PhD thesis, Université Paris 7 - Denis Diderot, UFR d’informatique, 2004. URL: http://tel.archives-ouvertes.fr/tel-00011326.
  15. I. Walukiewicz. Pushdown processes: Games and model-checking. Inf. Comput., 164(2):234-263, 2001. URL: http://dx.doi.org/10.1006/inco.2000.2894.
  16. W. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact