Document Open Access Logo

On the Complexity of Branching Games with Regular Conditions

Authors Marcin Przybylko, Michal Skrzypczak

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2016.78.pdf
  • Filesize: 0.49 MB
  • 14 pages

Document Identifiers

Author Details

Marcin Przybylko
Michal Skrzypczak

Cite As Get BibTex

Marcin Przybylko and Michal Skrzypczak. On the Complexity of Branching Games with Regular Conditions. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 78:1-78:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.MFCS.2016.78

Abstract

Infinite duration games with regular conditions are one of the crucial tools in the areas of verification and synthesis. In this paper we consider a branching variant of such games - the game contains branching vertices that split the play into two independent sub-games. Thus, a play has the form of~an~infinite tree. The winner of the play is determined by a winning condition specified as a set of infinite trees. Games of this kind were used by Mio to provide a game semantics for the probabilistic mu-calculus. He used winning conditions defined in terms of parity games on trees. In this work we consider a more general class of winning conditions, namely those definable by finite automata  on infinite trees. Our games can be seen as a branching-time variant of the stochastic games on graphs.

We address the question of determinacy of a branching game and the problem of computing the optimal game value for each of the players. We consider both the stochastic and non-stochastic variants of the games. The questions under consideration are parametrised by the family of strategies we allow: either mixed, behavioural, or pure.

We prove that in general, branching games are not determined under mixed strategies. This holds even for topologically simple winning conditions (differences of two open sets) and non-stochastic arenas. Nevertheless, we show that the games become determined under mixed strategies if we restrict the winning conditions to open sets of trees. We prove that the problem of comparing the game value to a rational threshold is undecidable for branching games with regular conditions in all  non-trivial stochastic cases. In the non-stochastic cases we provide exact bounds on the complexity of the problem. The only case left open is the 0-player stochastic case, i.e. the problem of computing the measure of a given regular language of infinite trees.

Subject Classification

Keywords
  • stochastic games
  • meta-parity games
  • infinite trees
  • regular languages
  • parity automata

Metrics

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

References

  1. Eugene Asarin, Julien Cervelle, Aldric Degorre, Catalin Dima, Florian Horn, and Victor Kozyakin. Entropy games. CoRR, abs/1506.04885, 2015. URL: http://arxiv.org/abs/1506.04885.
  2. Robert J. Aumann. Mixed and behavior strategies in infinite extensive games. Research Memorandum 32, Economic Research Program, Princeton University, 1961. Google Scholar
  3. Julius Richard Büchi and Lawrence H. Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society, 138:295-311, 1969. Google Scholar
  4. Krishnendu Chatterjee and Laurent Doyen. The complexity of partial observation parity games. In In Proc. LPAR’10, LNCS 6397. Springer, 2010. Google Scholar
  5. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. A survey of partial-observation stochastic parity games. Formal Methods in System Design, 43(2):268-284, 2012. Google Scholar
  6. Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Algorithms for omega-regular games with imperfect information. CoRR, abs/0706.2619, 2007. URL: http://arxiv.org/abs/0706.2619.
  7. Krishnendu Chatterjee and Thomas A. Henzinger. A survey of stochastic ω-regular games. J. Comput. Syst. Sci., 78(2):394-413, 2012. Google Scholar
  8. Taolue Chen, Klaus Dräger, and Stefan Kiefer. Model checking stochastic branching processes. In MFCS, pages 271-282, 2012. Google Scholar
  9. Thomas Colcombet and Damian Niwiński. On the positional determinacy of edge-labeled games. Theor. Comput. Sci., 352(1-3):190-196, 2006. Google Scholar
  10. Stefan Dziembowski, Marcin Jurdziński, and Igor Walukiewicz. How much memory is needed to win infinite games? In LICS, pages 99-110, 1997. Google Scholar
  11. Hugo Gimbert and Youssouf Oualhadj. Probabilistic automata on finite words: Decidable and undecidable problems. In ICALP (2), pages 527-538, 2010. Google Scholar
  12. Irving Leonard Glicksberg. Minimax Theorem for Upper and Lower Semi-continuous Payoffs. Memorandum (Rand Corporation). Rand Corporation, 1950. Google Scholar
  13. Tomasz Gogacz, Henryk Michalewski, Matteo Mio, and Michał Skrzypczak. Measure properties of game tree languages. In MFCS, pages 303-314, 2014. Google Scholar
  14. Alexander Kechris. Classical descriptive set theory. Springer-Verlag, New York, 1995. Google Scholar
  15. Donald A. Martin. Borel determinacy. Annals of Mathematics, 102(2):363-371, 1975. Google Scholar
  16. Donald A. Martin. The determinacy of Blackwell games. The Journal of Symbolic Logic, 63(4):1565-1581, 1998. Google Scholar
  17. Robert McNaughton. Infinite games played on finite graphs. Annals of Pure and Applied Logic, 65(2):149-184, 1993. Google Scholar
  18. P. Wolfe Melvin Dresher, A. W. Tucker. Contributions to the Theory of Games. Number 3 in Annals of mathematics studies. Princeton University Press, 1957. Google Scholar
  19. Henryk Michalewski and Matteo Mio. On the problem of computing the probability of regular sets of trees. In FSTTCS, pages 489-502, 2015. Google Scholar
  20. Matteo Mio. Game Semantics for Probabilistic μ-Calculi. PhD thesis, University of Edinburgh, 2012. Google Scholar
  21. Matteo Mio. On the equivalence of game and denotational semantics for the probabilistic mu-calculus. Logical Methods in Computer Science, 8(2), 2012. Google Scholar
  22. Marcin Przybyłko. Tree games with regular objectives. In GandALF, pages 231-244, 2014. Google Scholar
  23. Michael Oser Rabin. Decidability of second-order theories and automata on infinite trees. Trans. of the American Math. Soc., 141:1-35, 1969. Google Scholar
  24. Wolfgang Thomas. Languages, automata, and logic. In Handbook of Formal Languages, pages 389-455. Springer, 1996. Google Scholar
  25. Wolfgang Thomas and Helmut Lescow. Logical specifications of infinite computations. In REX School/Symposium, pages 583-621, 1993. 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