Unbounded Lookahead in WMSO+U Games
- Prelegent(ci)
- Martin Zimmermann
- Afiliacja
- Saarland University
- Termin
- 25 listopada 2015 14:15
- Pokój
- p. 5870
- Seminarium
- Seminarium „Teoria automatów”
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.
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.