Delay Games with WMSO$+$U Winning Conditions

Zimmermann, Martin

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 50 (2016) no. 2, pp. 145-165.

Delay games are two-player games of infinite duration in which one player may delay her moves to obtain a lookahead on her opponent’s moves. We consider delay games with winning conditions expressed in weak monadic second order logic with the unbounding quantifier, which is able to express (un)boundedness properties. We show that it is decidable whether the delaying player has a winning strategy using bounded lookahead and give a doubly-exponential upper bound on the necessary lookahead. In contrast, we show that bounded lookahead is not always sufficient: we present a game that can be won with unbounded lookahead, but not with bounded lookahead. Then, we consider such games with unbounded lookahead and show that the exact evolution of the lookahead is irrelevant: the winner is always the same, as long as the initial lookahead is large enough and the lookahead is unbounded.

M. Bojańczyk, A bounding quantifier. In CSL 2004. Edited by J. Marcinkowski and A. Tarlecki. Vol. 3210 of Lect. Notes Comput. Sci. Springer (2004) 41–55. | MR | Zbl

M. Bojańczyk, Weak MSO with the unbounding quantifier. Theory Comput. Syst. 48 (2011) 554–576. | DOI | MR | Zbl

M. Bojańczyk, Weak MSO+U with path quantifiers over infinite trees. In ICALP 2014, edited by Esparza et al. (2014) 38–49. | MR

M. Bojańczyk and Th. Colcombet, Bounds in $\omega$-regularity. In LICS 2006. IEEE Computer Society (2006) 285–296.

M. Bojańczyk, T. Gogacz, H. Michalewski and M. Skrzypczak, On the decidability of MSO+U on infinite trees. In ICALP 2014, edited by Esparza et al. (2014) 50–61. | MR

M. Bojańczyk, P. Parys and S. Toruńczyk, The MSO+U theory of $(N,<)$ is undecidable. In STACS 2016, edited by N. Ollinger and H. Vollmer. Vol. 47 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016) 21: 1–21:8. | MR

M. Bojańczyk and S. Toruńczyk, Deterministic automata and extensions of weak MSO. In FSTTCS 2009, edited by Kannan and Kumar (2009) 73–84. | MR | Zbl

M. Bojańczyk and S. Toruńczyk, Weak MSO+U over infinite trees. In STACS 2012, edited by Dürr and Wilke. Vol. 14 of LIPIcs. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012) 648–660. | MR | Zbl

J. Richard Büchi, On a decision method in restricted second-order arithmetic. In International Congress on Logic, Methodology, and Philosophy of Science. Stanford University Press (1962) 1–11. | MR | Zbl

J. Richard Büchi and L.H. Landweber, Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc. 138 (1969) 295–311. | DOI | MR | Zbl

J. Cabessa, J. Duparc, A. Facchini and F. Murlak, The Wadge hierarchy of max-regular languages. In FSTTCS 2009, edited by Kannan and Kumar (2009) 121–132. | MR | Zbl

A. Carayol and Ch. Löding, MSO on the infinite binary tree: Choice and order. In CSL 2007, edited by J. Duparc and Th.A. Henzinger. Vol. 4646 of Lect. Notes Comput. Sci. Springer (2007) 161–176. | MR | Zbl

A. Carayol and Ch. Löding, Uniformization in automata theory. In International Congress of Logic, Methodology and Philosophy of Science, edited by P. Schroeder-Heister, G. Heinzmann, W. Hodges and P. Edouard Bour. College Publications (2015). | MR

K. Chatterjee, Th.A. Henzinger and F. Horn, Finitary winning in omega-regular games. ACM Trans. Comput. Log. 11 (2009). | DOI | MR | Zbl

J. Esparza, P. Fraigniaud, Th. Husfeldt and E. Koutsoupias, ICALP 2014, Part II. Vol. 8573 of Lect. Notes Comput. Sci. Springer (2014). | MR

P. Faymonville and M. Zimmermann, Parametric linear dynamic logic. In GandALF 2014, edited by Peron and Piazza (2014) 60–73. | MR

N. Fijalkow and M. Zimmermann, Parity and Streett games with costs. LMCS 10 (2014) 14. | MR | Zbl

W. Fridman, Ch. Löding and M. Zimmermann, Degrees of lookahead in context-free infinite games. In CSL 2011, edited by M. Bezem, Vol. 12 of LIPIcs. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011) 264–276. | MR | Zbl

Y. Gurevich and S. Shelah, Rabin’s uniformization problem. J. Symbolic Logic 48 (1983) 1105–1119. | DOI | MR | Zbl

M. Holtmann, Ł. Kaiser and W. Thomas, Degrees of lookahead in regular infinite games. LMCS 8 (2012) 24. | MR | Zbl

F.A. Hosch and L.H. Landweber, Finite delay solutions for sequential conditions. In ICALP 1972 (1972) 45–60. | MR

S. Hummel and M. Skrzypczak, The topological complexity of MSO+U and related automata models. Fund. Inform. 119 (2012) 87–111. | MR | Zbl

R. Kannan and K.N. Kumar, FSTTCS 2009. Vol. 4 of LIPIcs. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009).

F. Klein and M. Zimmermann, How much lookahead is needed to win infinite games? In ICALP 2015, Part II, edited by Halldórsson et al. Vol. 9135 of Lect. Notes Comput. Sci. Springer (2015) 452–463. | MR

F. Klein and M. Zimmermann, What are strategies in delay games? borel determinacy for games with lookahead. In CSL 2015, edited by Kreutze. Vol. 41 of LIPIcs. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) 519–533. | MR

F. Klein and M. Zimmermann, Prompt delay. Preprint (2016). | arXiv | MR

O. Kupferman, N. Piterman and M.Y. Vardi, From liveness to promptness. Form. Methods Syst. Des. 34 (2009) 83–103. | DOI | Zbl

Ch. Löding and S. Winter, Synthesis of deterministic top-down tree transducers from automatic tree relations. In GandALF 2014, edited by Peron and Piazza (2014) 88–101. | MR

A. Peron and C. Piazza, GandALF 2014. Vol. 161 of EPTCS (2014).

W. Thomas, Infinite games and uniformization. In ICLA, edited by Banerjee and Seth. Vol. 6521 of Lect. Notes Comput. Sci. Springer (2011) 19–21. | MR | Zbl

W. Thomas and H. Lescow, Logical specifications of infinite computations. In A Decade of Concurrency, Reflections and Perspectives, REX School/Symposium, edited by de Bakker et al. Vol. 803 of Lect. Notes Comput. Sci. Springer (1993) 583–621. | MR

B.A. Trakhtenbrot and Ya.M. Barzdin, Finite Automata; Behavior and Synthesis. In vol. of Fund. Stud. Comput. Sci. North-Holland Publishing Company. New York: American Elsevier (1973). | MR | Zbl

M. Zimmermann, Optimal Bounds in Parametric LTL Games. Theoret. Comput. Sci. 493 (2013) 30–45. | DOI | MR | Zbl

M. Zimmermann, Delay games with WMSO+U winning conditions. In CSR 2015, edited by Lev D. Beklemishev and Daniil V. Musatov. Vol. 9139 of Lect. Notes Ccompu. Sci. Springer (2015) 412–425. | MR