Unbounded Lookahead in WMSO+U Games

TL;DR

This paper investigates delay games with winning conditions expressed in WMSO+U logic, showing that unbounded lookahead can be necessary and that beyond a certain size, the initial lookahead does not affect the outcome.

Contribution

It demonstrates that unbounded lookahead can be essential in WMSO+U delay games and that the winner remains the same once the lookahead surpasses a certain threshold.

Findings

Bounded lookahead may be insufficient for winning in some WMSO+U delay games.

Unbounded lookahead can be necessary for winning in certain cases.

The winner is unaffected by initial lookahead once it is sufficiently large.

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. We consider delay games with winning conditions expressed in weak monadic second order logic with the unbounding quantifier (WMSO+U), which is able to express (un)boundedness properties. It is decidable whether the delaying player is able to win such a game with bounded lookahead, i.e., if she only skips a finite number of moves. However, bounded lookahead is not always sufficient: we present a game that can be won with unbounded lookahead, but not with bounded lookahead. Then, we consider WMSO+U delay games with unbounded lookahead and show that the exact evolution of the lookahead is irrelevant: the winner is always the same, as long as the initial lookahead is large enough and the lookahead tends to infinity.