Prompt Delay

Klein, Felix and Zimmermann, Martin ORCID: 0000-0002-8038-2453
(2016) Prompt Delay. .

[thumbnail of promptdelay.pdf] Text
promptdelay.pdf - Published version

Download (530kB) | Preview


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.

Item Type: Conference or Workshop Item (Unspecified)
Uncontrolled Keywords: cs.GT, cs.GT, cs.FL, cs.LO
Depositing User: Symplectic Admin
Date Deposited: 15 Jul 2019 12:59
Last Modified: 06 Jun 2024 14:04
DOI: 10.4230/LIPIcs.FSTTCS.2016.43
Related URLs: