vix.ing · top · new · best · stats · spec

Unbounded Lookahead in WMSO+U Games

2015/09/24 by Martín Zimmermann, Zimmermann, Martin
Computer Science · #Computability, Logic, AI Algorithms #Computer Science and Game Theory (cs.GT) #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Logic, programming, and type systems #semigroups and automata theory

paper · pdf · doi:10.48550/arxiv.1509.07495

openalex publication_date 2015/09/24 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Related