Delay Games with WMSO+U Winning Conditions

TL;DR

This paper investigates delay games with winning conditions expressed in WMSO+U logic, establishing decidability of winning strategies with bounded lookahead and providing bounds on lookahead requirements.

Contribution

It introduces the analysis of delay games with WMSO+U winning conditions, proving decidability of winning strategies with bounded lookahead and establishing bounds on lookahead size.

Findings

Decidability of winning strategies with bounded lookahead.

Doubly-exponential upper bound on necessary lookahead.

Bounded lookahead is not always sufficient for winning.

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, which is able to express (un)boundedness properties. We show that it is decidable whether the delaying player has a winning strategy using bounded lookahead and give a doubly-exponential upper bound on the necessary lookahead. In contrast, we show that bounded lookahead is not always sufficient to win such a game.