Document Open Access Logo

Prompt Delay

Authors Felix Klein, Martin Zimmermann

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2016.43.pdf
  • Filesize: 0.5 MB
  • 14 pages

Document Identifiers

Author Details

Felix Klein
Martin Zimmermann

Cite As Get BibTex

Felix Klein and Martin Zimmermann. Prompt Delay. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 43:1-43:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.FSTTCS.2016.43

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. Recently, such games with quantitative winning conditions in weak MSO with the unbounding quantifier were studied, but their properties turned out to be unsatisfactory. In particular, unbounded lookahead is in general necessary.

Here, we study delay games with winning conditions given by Prompt-LTL, Linear Temporal Logic equipped with a parameterized eventually operator whose scope is bounded. Our main result shows that solving Prompt-LTL delay games is complete for triply-exponential time. Furthermore, we give tight triply-exponential bounds on the necessary lookahead and on the scope of the parameterized eventually operator. Thus, we identify Prompt-LTL as the first known class of well-behaved quantitative winning conditions for delay games.

Finally, we show that applying our techniques to delay games with omega-regular winning conditions answers open questions in the cases where the winning conditions are given by non-deterministic, universal, or alternating automata.

Subject Classification

Keywords
  • Infinite Games
  • Delay Games
  • Prompt-LTL
  • LTL

Metrics

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

References

  1. Rajeev Alur, Kousha Etessami, Salvatore La Torre, and Doron Peled. Parametric temporal logic for "model measuring". ACM Trans. Comput. Log., 2(3):388-407, 2001. Google Scholar
  2. Rajeev Alur and Salvatore La Torre. Deterministic generators and games for LTL fragments. ACM Trans. Comput. Log., 5(1):1-25, 2004. Google Scholar
  3. Mikołaj Bojańczyk. A bounding quantifier. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, CSL 2004, volume 3210 of LNCS, pages 41-55. Springer, 2004. Google Scholar
  4. Rüdiger Ehlers. Symbolic bounded synthesis. Form. Method. Syst. Des., 40(2):232-262, 2012. Google Scholar
  5. E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). In FOCS 1991, pages 368-377. IEEE, 1991. Google Scholar
  6. Peter Faymonville and Martin Zimmermann. Parametric linear dynamic logic. In Adriano Peron and Carla Piazza, editors, GandALF 2014, volume 161 of EPTCS, pages 60-73, 2014. Google Scholar
  7. Emmanuel Filiot, Naiyong Jin, and Jean-François Raskin. Antichains and compositional algorithms for LTL synthesis. Form. Method. Syst. Des., 39(3):261-296, 2011. Google Scholar
  8. Bernd Finkbeiner and Sven Schewe. Bounded synthesis. STTT, 15(5-6):519-539, 2013. Google Scholar
  9. Wladimir Fridman, Christof Löding, and Martin Zimmermann. Degrees of lookahead in context-free infinite games. In Marc Bezem, editor, CSL 2011, volume 12 of LIPIcs, pages 264-276. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. Google Scholar
  10. Paul Gastin and Denis Oddoux. Fast LTL to Büchi automata translation. In Gérard Berry, Hubert Comon, and Alain Finkel, editors, CAV 2001, volume 2102 of LNCS, pages 53-65. Springer, 2001. Google Scholar
  11. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of LNCS. Springer, 2002. Google Scholar
  12. Michael Holtmann, Łukasz Kaiser, and Wolfgang Thomas. Degrees of lookahead in regular infinite games. LMCS, 8(3), 2012. Google Scholar
  13. Florian Horn, Wolfgang Thomas, Nico Wallmeier, and Martin Zimmermann. Optimal strategy synthesis for request-response games. RAIRO - Theor. Inf. and Applic., 49(3):179-203, 2015. Google Scholar
  14. Frederick A. Hosch and Lawrence H. Landweber. Finite delay solutions for sequential conditions. In ICALP 1972, pages 45-60, 1972. Google Scholar
  15. Felix Klein and Martin Zimmermann. What are strategies in delay games? Borel determinacy for games with lookahead. In Stephan Kreutzer, editor, CSL 2015, volume 41 of LIPIcs, pages 519-533. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. Google Scholar
  16. Felix Klein and Martin Zimmermann. How much lookahead is needed to win infinite games? LMCS, 12(3), 2016. Google Scholar
  17. Felix Klein and Martin Zimmermann. Prompt delay. arXiv, 1602.05045, 2016. Google Scholar
  18. Orna Kupferman, Nir Piterman, and Moshe Y. Vardi. From liveness to promptness. Form. Method. Syst. Des., 34(2):83-103, 2009. Google Scholar
  19. Orna Kupferman and Moshe Y. Vardi. Safraless decision procedures. In FOCS 2005, pages 531-542. IEEE Computer Society, 2005. Google Scholar
  20. Andrzej Mostowski. Games with forbidden positions. Technical Report 78, University of Gdańsk, 1991. Google Scholar
  21. Amir Pnueli. The temporal logic of programs. In FOCS 1977, pages 46-57. IEEE, 1977. Google Scholar
  22. Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. In POPL 1989, pages 179-190. ACM Press, 1989. Google Scholar
  23. Amir Pnueli and Roni Rosner. On the synthesis of an asynchronous reactive module. In Giorgio Ausiello, Mariangiola Dezani-Ciancaglini, and Simona Ronchi Della Rocca, editors, ICALP 1989, volume 372 of LNCS, pages 652-671. Springer, 1989. Google Scholar
  24. Sven Schewe. Tighter bounds for the determinisation of Büchi automata. In Luca de Alfaro, editor, FOSSACS 2009, volume 5504 of LNCS, pages 167-181. Springer, 2009. Google Scholar
  25. Martin Zimmermann. Optimal bounds in parametric LTL games. Theor. Comput. Sci., 493:30-45, 2013. Google Scholar
  26. Martin Zimmermann. Parameterized linear temporal logics meet costs: Still not costlier than LTL. In Javier Esparza and Enrico Tronci, editors, GandALF 2015, volume 193 of EPTCS, pages 144-157, 2015. Google Scholar
  27. Martin Zimmermann. Delay games with WMSO+U winning conditions. RAIRO - Theor. Inf. and Applic., 2016. To appear. 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