Positionality in Σ_0^2 and a completeness result

This paper establishes that prefix-independent positional objectives in $\Sigma_0^2$ with a neutral letter are characterized by history-deterministic monotone co-Büchi automata over countable ordinals, a result that generalizes prior criteria, provides a new proof of closure under union, proves the positionality of mean-payoff games over arbitrary graphs, and demonstrates a completeness property for objectives positional over finite graphs.

The Gist

Imagine you are playing a very long, perhaps even infinite, board game against an opponent. The game takes place on a map (which could be a small town or a sprawling, infinite universe). Every time you move a piece, you pick up a "token" with a number or a letter on it. The goal is to create a specific pattern with the sequence of tokens you collect over time.

In this paper, the authors are studying a special kind of strategy called a "positional strategy."

The Core Concept: The "Amnesiac" Player

Usually, to win a complex game, you need a memory. You might think, "I went left twice and then right once, so now I should go up." This is a strategy based on history.

A positional strategy is like playing with amnesia. You only look at where you are right now. You don't care how you got there.

• The Question: For which types of games can you win without remembering the past? If you have a winning strategy, does a "forgetful" (positional) strategy also exist?

The authors focus on a specific class of games called $\Sigma^0_2$ objectives. In plain English, these are games where the winning condition is a bit complex but not impossible to describe: "You win if, eventually, you stop doing something bad, or if you do something good infinitely often, but with a specific structure."

The Big Discovery: The "Magic Filter"

The authors found a way to describe exactly which of these "forgetful-friendly" games exist. They proved that a game allows for a positional strategy if and only if it can be recognized by a specific type of machine called a "History-Deterministic Monotone Co-Büchi Automaton."

Let's break down that scary name with an analogy:

1. The Machine (Automaton): Imagine a robot that watches your game. It has a set of rooms (states) it can be in.
2. Monotone: The robot's rooms are arranged on a staircase. You can only move down the stairs or stay on the same step. You can never go back up. This means the robot is "simplifying" the game as it goes along.
3. History-Deterministic: This is the magic trick. Usually, a robot might need to guess which path to take based on the past. But this specific robot is smart enough to make the right choice just by looking at the current step and the current move, without needing to guess. It's like a GPS that never gets lost, even if you take a wrong turn, because it instantly recalculates the best path forward.
4. Co-Büchi: This is the rule for winning. The robot wins if it stops visiting a specific "bad" room after a while.

The Takeaway: If your game's rules can be translated into this "staircase robot" that never needs to guess, then you can win the game by just looking at your current location. You don't need a memory.

The "Neutral Letter" Secret Sauce

The paper mentions a "neutral letter." Think of this as a "Do Nothing" button.

• In a game of chess, a neutral move might be passing your turn (if allowed).
• In a game of collecting numbers, it might be adding a zero.

The authors found that if your game has this "Do Nothing" button that doesn't change the outcome, their "staircase robot" rule works perfectly. It's a safety net that makes the math work out.

Real-World Applications: The Mean-Payoff Game

One of the most famous games in this field is the Mean-Payoff Game. Imagine you are a delivery driver. Every road you take has a cost (or a reward).

• Goal: You want your average cost per mile to be negative (meaning you make a profit on average).
• The Problem: It was known that on finite maps (small towns), you can win with a simple, forgetful strategy. But on infinite maps (the whole world), people thought you needed a complex memory to win.

The Paper's Breakthrough:
The authors proved that even on infinite maps, if you tweak the rules slightly (specifically, if you want your average to be strictly less than zero, not just less than or equal to), you can win with a simple, forgetful strategy! They showed that this complex game is actually just a fancy version of a "bounded" game, which we already know is simple to play.

The "Completeness" Result: The Universal Translator

Finally, the paper offers a "Completeness Result." This is like a universal translator for game rules.

Imagine you have a game rule that is easy to win on small maps (finite arenas) but impossible to win on big maps without a memory. The authors say:

"Don't worry! We can translate your rule into a new rule that is equivalent on small maps, but is simple enough to be won with a forgetful strategy even on infinite maps."

It's like taking a complicated recipe that only works in a small kitchen and rewriting it so it works in a giant industrial kitchen, without changing the taste of the dish for the small kitchen.

Summary

1. The Problem: When can you win an infinite game without remembering the past?
2. The Answer: When the game's rules can be modeled by a "staircase robot" that simplifies the game as it goes and never needs to guess.
3. The Proof: They proved this for a wide class of games ($\Sigma^0_2$) and showed that if a game has a "neutral" move, this rule holds.
4. The Result: They solved a long-standing mystery about "Mean-Payoff" games, proving they are simpler than we thought, and provided a method to turn "hard" finite-game rules into "easy" infinite-game rules.

In short: If your game has a certain mathematical structure (like a staircase), you don't need a memory to win. And if it doesn't, we can often rewrite the rules so that you do.

Technical Summary

Here is a detailed technical summary of the paper "Positionality in $\Sigma^0_2$ and a Completeness Result" by Pierre Ohlmann and Michał Skrzypczak.

1. Problem Statement and Context

The paper investigates positional strategies in infinite-duration games played on graphs (arenas).

• The Game: Two players, Eve (proponent) and Adam (opponent), move a token along a directed graph with edges labeled by a set $C$. Eve wins if the infinite sequence of labels belongs to a target set $W \subseteq C^\omega$ (the objective).
• Positionality: An objective $W$ is positional if, whenever Eve has a winning strategy, she also has a positional strategy (one that depends only on the current vertex, not the history of the play).
• The Gap: While positionality is well-understood for specific objectives (like Parity games and Mean-Payoff games over finite arenas) and for objectives over finite arenas generally, the characterization of objectives that are positional over arbitrary (potentially infinite) arenas remains incomplete.
• Specific Focus: The authors focus on objectives in the Borel class $\Sigma^0_2$ (countable unions of closed sets) that are prefix-independent (invariant under adding/removing finite prefixes) and admit a neutral letter (a symbol that can be inserted or removed without changing the membership in $W$).

2. Methodology

The authors employ a combination of automata theory, graph theory, and structural game theory.

• Structuration Results: They utilize a technique developed by Ohlmann involving universal graphs. Specifically, they rely on the existence of monotone and well-founded graphs that can "simulate" any graph satisfying the objective.
• History-Deterministic Automata: They characterize objectives using co-Büchi automata that are:
  • Countable: The state space is countable.
  • Monotone: The graph structure respects a total order on states.
  • Well-founded: The order on states has no infinite descending chains.
  • History-Deterministic (HD): There exists a deterministic "resolver" that can resolve non-determinism based on the input history to accept the same language.
• Finitary Substitution: To bridge finite and infinite arenas, they define a "finitary substitute" $W_{fin}$ for an objective $W$, consisting of all infinite words that can be generated by some finite graph satisfying $W$.

3. Key Contributions and Results

A. Characterization of Positional $\Sigma^0_2$ Objectives (Theorem 1.2)

The authors provide a complete characterization (up to neutral letters) of prefix-independent $\Sigma^0_2$ objectives that are positional over arbitrary arenas.

• Theorem: A prefix-independent $\Sigma^0_2$ objective $W$ admitting a strongly neutral letter is positional over arbitrary arenas if and only if it is recognized by a countable, history-deterministic, well-founded, monotone co-Büchi automaton.
• Significance: This generalizes Kopczyński's earlier results on monotone objectives. It establishes a direct link between the structural property of the objective (positional) and its automata-theoretic representation (HD monotone co-Büchi).

B. Closure Under Countable Unions (Corollary 1.2)

A major open question (Kopczyński's Conjecture) was whether positional objectives are closed under unions.

• Result: The class of prefix-independent, positional $\Sigma^0_2$ objectives (admitting strongly neutral letters) is closed under countable unions.
• Mechanism: The proof constructs a new automaton from the disjoint union of the automata for individual objectives, adding transitions to simulate a "round-robin" strategy that ensures history-determinism is preserved.

C. Positionality of Mean-Payoff Games (Proposition 4.3)

The paper resolves the status of Mean-Payoff games over arbitrary arenas.

• Context: The standard Mean-Payoff objective ($\limsup \frac{1}{k}\sum w_i \leq 0$) is known not to be positional over arbitrary arenas.
• Result: The strict variant Mean-Payoff$<0$ ($\limsup \frac{1}{k}\sum w_i < 0$) is positional over arbitrary arenas.
• Proof Strategy: The authors show that Mean-Payoff$<0$ is the countable union of "Tilted-Bounded" objectives (which are positional). By the closure under union result, the union is positional.

D. Completeness Result (Theorem 1.3)

This is a structural result regarding the relationship between finite and arbitrary arenas.

• Theorem: Let $W$ be a prefix-independent objective admitting a weakly neutral letter. If $W$ is positional over finite arenas, then there exists an objective $W' \subseteq W$ such that:
  1. $W'$ is finitely equivalent to $W$ (Eve wins the same finite arenas for both).
  2. $W'$ is positional over arbitrary arenas.
• Implication: Any objective that behaves well on finite graphs can be "approximated" by a "better" objective that behaves well on all graphs, without changing the outcome on finite graphs. This suggests that the failure of positionality on infinite graphs is often due to the specific structure of the objective, which can be "fixed" by restricting the objective to its finitary behavior.

4. Significance and Impact

1. Unification of Theory: The paper unifies the study of positionality for a broad class of objectives ($\Sigma^0_2$) under a single automata-theoretic framework (HD monotone co-Büchi automata).
2. Resolution of Conjectures: It positively answers Kopczyński's conjecture for the specific case of $\Sigma^0_2$ objectives (with neutral letters), proving closure under countable unions.
3. Refinement of Mean-Payoff: It clarifies the subtle boundary between positional and non-positional Mean-Payoff objectives, identifying the strict inequality variant as positional.
4. Finite vs. Infinite: The completeness result provides a powerful tool for transferring results from finite arenas (where many algorithms exist) to arbitrary arenas, provided a neutral letter exists.
5. Future Directions: The authors identify the characterization of positionality in $\Delta^0_3$ and the removal of the prefix-independence assumption as the next major challenges.

Summary of Technical Flow

1. Definitions: Establish graphs, arenas, strategies, and the specific classes of objectives ($\Sigma^0_2$, neutral letters).
2. Structuration: Use Ohlmann's lemma to embed graphs satisfying the objective into monotone, well-founded graphs.
3. Automata Construction: Convert these monotone graphs into history-deterministic co-Büchi automata.
4. Characterization: Prove the equivalence between the existence of such automata and positionality.
5. Applications: Apply the characterization to prove closure under unions and the positionality of strict Mean-Payoff.
6. Completeness: Define the finitary substitute $W_{fin}$, prove it is $\Sigma^0_2$ and positional, and show it is finitely equivalent to the original $W$.