Prompt Delay



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

[img] Text
promptdelay.pdf - Published version

Download (530kB) | Preview

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.

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: 19 Jan 2023 00:37
DOI: 10.4230/LIPIcs.FSTTCS.2016.43
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/3049684