×

Prompt delay. (English) Zbl 1391.68073

Lal, Akash (ed.) et al., 36th IARCS annual conference on foundations of software technology and theoretical computer science (FSTTCS 2016), Chennai, India, December 13–15, 2016. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-95977-027-9). LIPIcs – Leibniz International Proceedings in Informatics 65, Article 43, 14 p. (2016).
Summary: 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.
For the entire collection see [Zbl 1354.68012].

MSC:

68Q45 Formal languages and automata
03B44 Temporal logic
03D05 Automata and formal grammars in connection with logical questions
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
91A43 Games involving graphs
PDFBibTeX XMLCite
Full Text: DOI arXiv