Finite-memory strategies in two-player infinite games
share
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 Δ^0_2 (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 Σ^0_2 and Π^0_2 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.
READ FULL TEXT