Solving Infinite Games in the Baire Space

TL;DR

This paper extends classical game theory results to infinite Gale-Stewart games in the Baire space, showing determinacy and computability of winning strategies using automata defined by monadic second-order logic.

Contribution

It introduces a new class of parity automata over natural numbers and proves that the B"uchi-Landweber Theorem applies to these automata-based infinite games.

Findings

Games are determined and winners can be computed.

Winning strategies can be realized by automata-based transducers.

Classical results extend to the Baire space setting.

Abstract

Infinite games (in the form of Gale-Stewart games) are studied where a play is a sequence of natural numbers chosen by two players in alternation, the winning condition being a subset of the Baire space $\omega^\omega$. We consider such games defined by a natural kind of parity automata over the alphabet $\mathbb{N}$, called $\mathbb{N}$-MSO-automata, where transitions are specified by monadic second-order formulas over the successor structure of the natural numbers. We show that the classical B\"uchi-Landweber Theorem (for finite-state games in the Cantor space $2^\omega$) holds again for the present games: A game defined by a deterministic parity $\mathbb{N}$-MSO-automaton is determined, the winner can be computed, and an $\mathbb{N}$-MSO-transducer realizing a winning strategy for the winner can be constructed.