Prompt Delay

TL;DR

This paper investigates delay games with Prompt-LTL winning conditions, establishing their computational complexity, bounds on lookahead and scope, and demonstrating Prompt-LTL as a well-behaved class for such games.

Contribution

It introduces Prompt-LTL delay games, proves their triply-exponential complexity, and provides tight bounds, positioning Prompt-LTL as a new well-behaved class for delay games.

Findings

Solving Prompt-LTL delay games is triply-exponential complete.

Tight triply-exponential bounds on lookahead and operator scope are established.

Techniques extend to delay games with -regular winning conditions, answering open questions.

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.