Skip to main content
SpringerLink
Log in
Book cover

International Computer Science Symposium in Russia

CSR 2015: Computer Science -- Theory and Applications pp 412–425Cite as

Delay Games with WMSO\(+\)U Winning Conditions

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9139))

Abstract

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.

Martin Zimmermann — Supported by the DFG projects “TriCS” (ZI 1516/1-1) and “AVACS” (SFB/TR 14).

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    Here, the second-order quantifiers are restricted to finite sets.

  2. 2.

    See Example 1 in [2] for more details.

  3. 3.

    Here, and later whenever convenient, we treat \(\delta \) as relation \(\delta \subseteq Q \times \varSigma \times Q\).

  4. 4.

    See, e.g., [15] for a detailed definition of parity games.

  5. 5.

    This implies that \(\mathcal {G}(\mathcal {A})\) is determined, as max-regular conditions are Borel [1, 22].

References

  1. Bojańczyk, M.: Weak MSO with the unbounding quantifier. Theory Comput. Syst. 48(3), 554–576 (2011)

    Article  MATH  MathSciNet  Google Scholar 

  2. Bojańczyk, M.: Weak MSO+U with path quantifiers over infinite trees. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014, Part II. LNCS, vol. 8573, pp. 38–49. Springer, Heidelberg (2014)

    Google Scholar 

  3. Bojańczyk, M., Gogacz, T., Michalewski, H., Skrzypczak, M.: On the decidability of MSO+U on infinite trees. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014, Part II. LNCS, vol. 8573, pp. 50–61. Springer, Heidelberg (2014)

    Google Scholar 

  4. Bojańczyk, M., Parys, P., Toruńczyk, S.: The MSO+U theory of \((\mathbb{N}\), \(<\)) is undecidable (2015). arXiv:1502.04578

  5. Bojańczyk, M., Toruńczyk, S.: Weak MSO+U over infinite trees. In: Dürr, C., Wilke, T. (eds.) STACS 2012. LIPIcs, vol. 14, pp. 648–660. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2012)

    Google Scholar 

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

    Google Scholar 

  7. Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc. 138, 295–311 (1969)

    Article  MATH  MathSciNet  Google Scholar 

  8. Carayol, A., Löding, C.: MSO on the infinite binary tree: choice and order. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 161–176. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  9. Carayol, A., Löding, C.: Uniformization in automata theory. In: Schroeder-Heister, P., Heinzmann, G., Hodges, W., Bour, P.E. (eds.) International Congress of Logic, Methodology and Philosophy of Science. College Publications, London (2012, to appear)

    Google Scholar 

  10. Chatterjee, K., Henzinger, T.A., Horn, F.: Finitary winning in omega-regular games. ACM Trans. Comput. Log. 11(1) (2009)

    Google Scholar 

  11. Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy (extended abstract). In: FOCS 1991, pp. 368–377. IEEE (1991)

    Google Scholar 

  12. Faymonville, P., Zimmermann, M.: Parametric linear dynamic logic. http://dblp.uni-trier.de/rec/bibtex/journals/corr/FaymonvilleZ14

  13. Fijalkow, N., Zimmermann, M.: Parity and Streett Games with Costs. LMCS 10(2) (2014)

    Google Scholar 

  14. Fridman, W., Löding, C., Zimmermann, M.: Degrees of lookahead in context-free infinite games. In: Bezem, M. (ed.) CSL 2011. LIPIcs, vol. 12, pp. 264–276. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2011)

    Google Scholar 

  15. Grädel, E., Thomas, W., Wilke, T. (eds.): Automata Logics, and Infinite Games: A Guide to Current Research. LNCS, vol. 2500. Springer, Heidelberg (2002)

    Google Scholar 

  16. Gurevich, Y., Shelah, S.: Rabin’s uniformization problem. J. Symbolic Logic 48, 1105–1119 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  17. Holtmann, M., Kaiser, L., Thomas, W.: Degrees of lookahead in regular infinite games. LMCS 8(3) (2012)

    Google Scholar 

  18. Hosch, F.A., Landweber, L.H.: Finite delay solutions for sequential conditions. In: ICALP 1972. pp. 45–60 (1972)

    Google Scholar 

  19. Klein, F., Zimmermann, M.: How much lookahead is needed to win infinite games? (2014). arXiv: 1412.3701

  20. Kupferman, O., Piterman, N., Vardi, M.Y.: From liveness to promptness. Formal Methods Syst. Des. 34(2), 83–103 (2009)

    Article  MATH  Google Scholar 

  21. Löding, C., Winter, S.: Synthesis of deterministic top-down tree transducers from automatic tree relations. http://dblp.uni-trier.de/rec/bibtex/journals/corr/LodingW14

  22. Martin, D.A.: Borel determinacy. Ann. Math. 102, 363–371 (1975)

    Article  MATH  Google Scholar 

  23. Mostowski, A.: Games with forbidden positions. Technical report 78, University of Gdańsk (1991)

    Google Scholar 

  24. Thomas, W.: Infinite games and uniformization. In: Banerjee, M., Seth, A. (eds.) Logic and Its Applications. LNCS, vol. 6521, pp. 19–21. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  25. Thomas, W., Lescow, H.: Logical specifications of infinite computations. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) A Decade of Concurrency, Reflections and Perspectives. LNCS, vol. 803, pp. 583–621. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  26. Trakhtenbrot, B., Barzdin, I.: Finite Automata: Behavior and Synthesis. Fundamental Studies in Computer Science, vol. 1. North-Holland Publishing Company, American Elsevier, Amsterdam, New York (1973)

    MATH  Google Scholar 

  27. Zimmermann, M.: Optimal bounds in parametric LTL games. Theor. Comput. Sci. 493, 30–45 (2013)

    Article  MATH  Google Scholar 

  28. Zimmermann, M.: Delay games with WMSO+U winning conditions (2014). arXiv: 1412.3978

Download references

Author information

Authors and Affiliations

  1. Reactive Systems Group, Saarland University, Saarbrücken, Germany

    Martin Zimmermann

Authors
  1. Martin Zimmermann
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Martin Zimmermann .

Editor information

Editors and Affiliations

  1. Steklov Mathematical Institute of Russian Academy of Sciences, Lomonosov Moscow State University and National Research University Higher School of Economics, Moscow, Russia

    Lev D. Beklemishev

  2. Moscow Institute of Physics and Technology, Moscow, Russia and Kazan (Volga Region) Federal University, Kazan, Kabardino-Balkar.Rep, Russia

    Daniil V. Musatov

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Zimmermann, M. (2015). Delay Games with WMSO\(+\)U Winning Conditions. In: Beklemishev, L., Musatov, D. (eds) Computer Science -- Theory and Applications. CSR 2015. Lecture Notes in Computer Science(), vol 9139. Springer, Cham. https://doi.org/10.1007/978-3-319-20297-6_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-20297-6_26

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-20296-9

  • Online ISBN: 978-3-319-20297-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation