pith. sign in

arxiv: 2309.17022 · v5 · submitted 2023-09-29 · 💻 cs.LO

Positionality in Sigma₀² and a completeness result

Pierre Ohlmann , Micha{\l} Skrzypczak This is my paper

Pith reviewed 2026-05-24 06:42 UTC · model grok-4.3

classification 💻 cs.LO
keywords positionalityinfinite gamesΣ₀² objectivesco-Büchi automataneutral lettermean-payoffgame graphsprefix-independent objectives
0
0 comments X

The pith

Prefix-independent Σ₀² objectives that are positional and admit a strongly neutral letter are exactly those recognized by history-deterministic monotone co-Büchi automata over countable ordinals.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes an exact characterization for a class of objectives in two-player infinite games on arbitrary graphs. Objectives in Σ₀² that are prefix-independent, positional for the protagonist, and equipped with a strongly neutral letter turn out to be precisely the languages accepted by history-deterministic monotone co-Büchi automata whose state space is a countable ordinal. The result extends an earlier criterion and supplies a fresh argument that these objectives remain closed under union. Two concrete consequences are derived: the mean-payoff objective becomes positional on every game graph, and every prefix-independent objective with a weakly neutral letter that is positional on finite graphs admits an equivalent version that remains positional on arbitrary graphs.

Core claim

Prefix-independent objectives in Σ₀² which are positional and admit a (strongly) neutral letter are exactly those that are recognised by history-deterministic monotone co-Büchi automata over countable ordinals.

What carries the argument

History-deterministic monotone co-Büchi automata over countable ordinals, which serve as the canonical recognizers for the positional objectives that carry a strongly neutral letter.

If this is right

  • The mean-payoff objective is positional over arbitrary game graphs.
  • For any prefix-independent objective with a weakly neutral letter that is positional over finite graphs there exists an equivalent objective that is positional over arbitrary graphs.
  • The class is closed under union.
  • The characterization generalizes the 2006 criterion of Kopczyński.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The automata representation may supply a decision procedure for positionality within Σ₀² once the automata are effectively presented.
  • Similar automata characterizations could be sought for objectives lying in higher levels of the Borel hierarchy.
  • The completeness construction suggests that positionality on finite graphs can often be lifted without changing the objective on finite instances.

Load-bearing premise

The objectives must be prefix-independent and must admit a strongly neutral letter.

What would settle it

An explicit prefix-independent Σ₀² objective that is positional on every game graph, possesses a strongly neutral letter, yet fails to be recognized by any history-deterministic monotone co-Büchi automaton whose states form a countable ordinal.

read the original abstract

We study the existence of positional strategies for the protagonist in infinite duration games over arbitrary game graphs. We prove that prefix-independent objectives in $\Sigma_0^2$ which are positional and admit a (strongly) neutral letter are exactly those that are recognised by history-deterministic monotone co-B\"chi automata over countable ordinals. This generalises a criterion proposed by [Kopczy\'nski, ICALP 2006] and gives an alternative proof of closure under union for these objectives, which was known from [Ohlmann, TheoretiCS 2023]. We then give two applications of our result. First, we prove that the mean-payoff objective is positional over arbitrary game graphs. Second, we establish the following completeness result: for any objective $W$ which is prefix-independent, admits a (weakly) neutral letter, and is positional over finite game graphs, there is an objective $W'$ which is equivalent to $W$ over finite game graphs and positional over arbitrary game graphs.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 1 minor

Summary. The paper proves that prefix-independent Σ₀² objectives which are positional and admit a strongly neutral letter are exactly those recognised by history-deterministic monotone co-Büchi automata over countable ordinals. This generalises Kopczyński's 2006 criterion and yields an alternative proof of closure under union. Two applications are given: (1) the mean-payoff objective is positional on arbitrary graphs, and (2) for any prefix-independent objective with a weakly neutral letter that is positional on finite graphs, there exists an equivalent objective that is positional on arbitrary graphs.

Significance. If the central characterisation holds, the result supplies a concrete automata-theoretic test for positionality inside Σ₀² and strengthens the toolkit for infinite-duration games on arbitrary graphs. The completeness result is potentially useful for lifting finite-graph theorems. The alternative proof of union-closure is a concrete contribution provided the main equivalence is established without circularity.

major comments (1)
  1. [applications / mean-payoff paragraph] Application section (mean-payoff): the manuscript invokes the main theorem to conclude that mean-payoff is positional on arbitrary graphs. However, mean-payoff is Π₀³ (outer intersection over m of Σ₀² sets), not Σ₀². The left-to-right direction of the stated equivalence therefore does not apply, and no separate general argument for the 'automaton implies positional' direction outside Σ₀² is indicated in the abstract or theorem statement. This undermines the first application claim.
minor comments (1)
  1. [abstract] Abstract: 'co-Büchi' is misspelled as 'co-Büchi' with an escaped quote; correct the typesetting.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading and for highlighting this issue regarding the mean-payoff application. We address the comment below and will revise the manuscript to clarify the scope of the relevant implication.

read point-by-point responses

  1. Referee: [applications / mean-payoff paragraph] Application section (mean-payoff): the manuscript invokes the main theorem to conclude that mean-payoff is positional on arbitrary graphs. However, mean-payoff is Π₀³ (outer intersection over m of Σ₀² sets), not Σ₀². The left-to-right direction of the stated equivalence therefore does not apply, and no separate general argument for the 'automaton implies positional' direction outside Σ₀² is indicated in the abstract or theorem statement. This undermines the first application claim.

    Authors: We agree that the mean-payoff objective lies in Π₀³ rather than Σ₀². The left-to-right direction of the main characterisation (positional + neutral letter implies automaton) is indeed stated only for Σ₀² objectives. However, the converse direction (automaton implies positional) is proved without using the Σ₀² assumption; its argument applies to arbitrary prefix-independent objectives. In the application we explicitly construct a history-deterministic monotone co-Büchi automaton over countable ordinals recognising mean-payoff and rely on this general implication. We will revise the abstract, the statement of the main theorem, and the application section to make this generality explicit, thereby justifying the claim without circularity. The same general implication also supports the alternative proof of union-closure referenced in the referee summary. revision: yes

Circularity Check

0 steps flagged

No significant circularity; main characterization is independent of self-citations

full rationale

The central result is an iff characterization of positional prefix-independent Σ₀² objectives (with neutral letter) via history-deterministic monotone co-Büchi automata over countable ordinals. This is presented as a new theorem that generalizes an external criterion (Kopczyński 2006) and supplies an alternative proof of a known closure property (Ohlmann 2023). The self-citation is explicitly non-load-bearing and concerns only the alternative proof of a prior result. No self-definitional equations, no fitted parameters renamed as predictions, and no uniqueness theorems imported from the authors' own prior work appear in the derivation. The two applications are stated as consequences of the main theorem; even if the mean-payoff claim requires additional justification outside Σ₀², that is a scope/correctness issue rather than a reduction of the derivation to its own inputs by construction. The paper is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on standard definitions from automata theory and infinite game theory with no new free parameters, invented entities, or ad-hoc axioms introduced in the abstract.

axioms (1)
  • domain assumption Standard definitions and closure properties of Σ₀² sets, prefix-independence, and neutral letters for objectives
    These are background assumptions from the field of automata and games invoked to state the characterization.

pith-pipeline@v0.9.0 · 5713 in / 1238 out tokens · 34037 ms · 2026-05-24T06:42:03.682906+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

17 extracted references · 17 canonical work pages

  1. [1]

    How deterministic are good-for-games automata? In FSTTCS, volume 93 ofLIPIcs, pages 18:1–18:14

    1 Udi Boker, Orna Kupferman, and Michał Skrzypczak. How deterministic are good-for-games automata? In FSTTCS, volume 93 ofLIPIcs, pages 18:1–18:14. Schloss Dagstuhl - Leibniz- Zentrum für Informatik, 2017.doi:10.4230/LIPIcs.FSTTCS.2017.18. 2 Patricia Bouyer, Antonio Casares, Mickael Randour, and Pierre Vandenhove. Half-positional objectives recognized by ...

    work page doi:10.4230/lipics.fsttcs.2017.18 2017

  2. [2]

    4 Antonio Casares

    doi:10.1007/s10703-010-0105-x. 4 Antonio Casares. Structural properties of ω-automata and strategy complexity in infinite duration games. PhD thesis, Université de Bordeaux,

    work page doi:10.1007/s10703-010-0105-x

  3. [3]

    Thilikos, and Alexandre Vigny

    5 Antonio Casares and Pierre Ohlmann. Positional ω-regular languages. In LICS, pages 21:1–21:14. ACM, 2024.doi:10.1145/3661814.3662087. 6 Antonio Casares and Pierre Ohlmann. Characterising memory in infinite games.Log. Methods Comput. Sci., 21(1),

    work page doi:10.1145/3661814.3662087 2024

  4. [4]

    46298/LMCS-21(1:28)2025

    URL: https://doi.org/10.46298/lmcs-21(1:28)2025, doi:10. 46298/LMCS-21(1:28)2025. 7 Thomas Colcombet. Forms of determinism for automata (invited talk). InSTACS, volume 14 of LIPIcs, pages 1–23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012.doi:10.4230/ LIPIcs.STACS.2012.1. 8 Thomas Colcombet, Nathanaël Fijalkow, Paweł Gawrychowski, and Pierre Oh...

    work page doi:10.46298/lmcs-21(1:28)2025 2025

  5. [5]

    9 Thomas Colcombet and Damian Niwiński

    doi:10.46298/lmcs-18(3:29)2022. 9 Thomas Colcombet and Damian Niwiński. On the positional determinacy of edge-labeled games. Theor. Comput. Sci., 352(1-3):190–196, 2006.doi:10.1016/j.tcs.2005.10.046. 10 Morton Davis. Infinite games of perfect information. InAdvances in game theory, pages 85–101. Princeton Univ. Press, Princeton, N.J.,

    work page doi:10.46298/lmcs-18(3:29)2022 2022

  6. [6]

    Positional strategies for mean payoff games.Interna- tional Journal of Game Theory, 109(8):109–113, 1979.doi:10.1007/BF01768705

    11 Andrzej Ehrenfeucht and Jan Mycielski. Positional strategies for mean payoff games.Interna- tional Journal of Game Theory, 109(8):109–113, 1979.doi:10.1007/BF01768705. 12 E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). In 32nd Annual Symposium on Foundations of Computer Science, San Juan, Puerto ...

    work page doi:10.1007/bf01768705 1979

  7. [7]

    doi:10.1109/SFCS.1991.185392. 13 Nathanaël Fijalkow, Nathalie Bertrand, Patricia Bouyer-Decitre, Romain Brenguier, Arnaud Carayol, John Fearnley, Hugo Gimbert, Florian Horn, Rasmus Ibsen-Jensen, Nicolas Markey, Benjamin Monmege, Petr Novotný, Mickael Randour, Ocan Sankur, Sylvain Schmitz, Olivier Serre, and Mateusz Skomra.Games on Graphs. Online. 14 David...

    work page doi:10.1109/sfcs.1991.185392 1991

  8. [8]

    Parity and exploration games on infinite graphs

    15 Hugo Gimbert. Parity and exploration games on infinite graphs. In Jerzy Marcinkowski and Andrzej Tarlecki, editors,Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings, volume 3210 ofLecture Notes in Computer Science, pages 56–70. Springer,

    work page 2004

  9. [9]

    16 Hugo Gimbert and Wiesław Zielonka

    doi:10.1007/978-3-540-30124-0\_8. 16 Hugo Gimbert and Wiesław Zielonka. Games where you can play optimally without any memory. InCONCUR, volume 3653 ofLecture Notes in Computer Science, pages 428–442. Springer,

    work page doi:10.1007/978-3-540-30124-0

  10. [10]

    17 Thomas A

    doi:10.1007/11539452\_33. 17 Thomas A. Henzinger and Nir Piterman. Solving games without determinization. In Zoltán Ésik, editor,Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual 20 Positionality in Σ0 2 and a completeness result Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings, volume 4207 ofLecture No...

    work page doi:10.1007/11539452 2006

  11. [11]

    Differential Privacy,

    20 Eryk Kopczyński. Half-positional determinacy of infinite games. InICALP, volume 4052 of Lecture Notes in Computer Science, pages 336–347. Springer, 2006.doi:10.1007/11787006\ _29. 21 Eryk Kopczyński.Half-positional determinacy of infinite games. PhD thesis, University of Warsaw,

    work page doi:10.1007/11787006 2006

  12. [12]

    22 Alexander Kozachinskiy

    URL:https://www.mimuw.edu.pl/~erykk/papers/hpwc.pdf. 22 Alexander Kozachinskiy. Energy games over totally ordered groups.CoRR, abs/2205.04508,

    work page arXiv

  13. [13]

    22 Alexander Kozachinskiy

    arXiv:2205.04508, doi:10.48550/arXiv.2205.04508. 23 Denis Kuperberg and Michał Skrzypczak. On determinisation of good-for-games automata. In ICALP, volume 9135 ofLecture Notes in Computer Science, pages 299–310. Springer,

    work page doi:10.48550/arxiv.2205.04508

  14. [14]

    24 Donald A

    doi:10.1007/978-3-662-47666-6\_24. 24 Donald A. Martin. Borel determinacy.Annals of Mathematics, 102(2):363–371,

    work page doi:10.1007/978-3-662-47666-6

  15. [15]

    28 Pierre Ohlmann

    URL:https://theoretics.episciences.org/10878, doi:10.46298/theoretics.23.3. 28 Pierre Ohlmann. Positionality of mean-payoff games on infinite graphs, 2023.arXiv:2305. 00347. 29 Michael O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society, 141:1–35,

    work page doi:10.46298/theoretics.23.3 2023

  16. [16]

    org/stable/1995086

    URL:http://www.jstor. org/stable/1995086. 30 Bader Abu Radi and Orna Kupferman. Minimization and canonization of GFG transition-based automata. Log. Methods Comput. Sci., 18(3),

    work page arXiv

  17. [17]

    31 Lloyd S

    doi:10.46298/lmcs-18(3:16)2022. 31 Lloyd S. Shapley. Stochastic games. 39(10):1095–1100, 1953.doi:10.1073/pnas.39.10.1095. 32 Michał Skrzypczak. Topological extension of parity automata.Information and Computation, 228:16–27,

    work page doi:10.46298/lmcs-18(3:16)2022 2022