Unbounded Lookahead in WMSO+U Games

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, it is also known that bounded lookahead is not always sufficient: there is a game that can be won with unbounded lookahead, but not with bounded lookahead.

Therefore, we consider WMSO+U delay games with unbounded lookahead and show that the exact evolution of the lookahead is irrelevant. Then, we investigate whether the winner of such a game with unbounded lookahead is effectively computable: we reduce this problem to a delay-free infinite game with WMSO+U winning condition, whose winner is effectively computable. However, we leave open whether the reduction is effective, thereby leaving decidability also open. Time permitting, we discuss the open problem.