Finite-Memory Strategies in Two-Player Infinite Games

Abstract

We study infinite two-player win/lose games (A,B,W) where A,B are finite and W ⊆ (A×B)^ω. At each round Player 1 and Player 2 concurrently choose one action in A and B, respectively. Player 1 wins iff the generated sequence is in W. Each history h ∈ (A×B)^* induces a game (A,B,W_h) with W_h : = {ρ ∈ (A×B)^ω ∣ h ρ ∈ W}. We show the following: if W is in Δ⁰₂ (for the usual topology), if the inclusion relation induces a well partial order on the W_h’s, and if Player 1 has a winning strategy, then she has a finite-memory winning strategy. Our proof relies on inductive descriptions of set complexity, such as the Hausdorff difference hierarchy of the open sets.
Examples in Σ⁰₂ and Π⁰₂ show some tightness of our result. Our result can be translated to games on finite graphs: e.g. finite-memory determinacy of multi-energy games is a direct corollary, whereas it does not follow from recent general results on finite memory strategies.