Delay Games with WMSO+U Winning Conditions
Martin Zimmermann
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. These are the first results on delay games with quantitative winning conditions.