Mostowski Index via extended register games

Karoliina Lehtinen; Olivier Idir

REVIEW 4 major objections 6 minor 1 cited by

Mostowski Index via extended register games

T0 review · 4 major / 6 minor · reviewed 2026-08-11 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper claims that for guidable tree automata, a language is recognizable with a given priority index exactly when a single uniform counter bound makes Eve's win in an extended register game coincide with membership in the language.

desk verdict Promising game-based characterization of the Mostowski index, but the forward direction's key lemma has a real gap and the proof is only a sketch; worth referee time, not acceptance as is. read the letter →

arxiv 2412.16793 v1 pith:ZWU53VXD submitted 2024-12-21 cs.FL

Olivier Idir , Karoliina Lehtinen This is my paper · ORCID

classification cs.FL MSC 03D0568Q45

keywords Mostowskiindexparityproblemtreeautomataregistergamestransductionguidablenondeterministic

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper tackles the Mostowski index problem: given a regular tree language, what is the least number of priorities a nondeterministic parity tree automaton needs to recognize it? The authors define parity transduction games, an extension of register games with bounded counters, parameterized by a target index $J$ and a counter bound $N$. They claim that for any guidable automaton $A$ — an automaton that resolves its nondeterminism by reading an accepting run of any equivalent automaton — the language $L(A)$ is $J$-feasible if and only if some uniform $N$ makes Eve's winning in $T^N_J(G(A,t))$ exactly coincide with $t \in L(A)$ for every tree $t$. If true, this reduces the index question to a uniform finitary parameter of a game, re-deriving the known reduction to distance-parity automata with a simpler proof. The paper is a brief informal note; the forward direction's key pumping lemma is sketched rather than fully proved.

What carries the argument

The central object is the parity transduction game $T^N_J$, an extension of the register games used in a known quasipolynomial-time parity-game algorithm. Played over a parity game $G = (V,E,L)$ whose edges carry priorities in an index $I$, the game outputs a priority in $J$: at each step Adam picks an edge, Eve picks a register $r_j$ (one per even $2j \in J$, plus possibly $r_0$), and the outputs are determined by whether the register's stored value is even, with counters $c_{i,j}$ for odd $i$ limiting how often Eve can delay outputting an odd priority. Her goal is that the infinite output sequence is parity accepting. The counter bound $N$ is the uniformity parameter: the theorem says the index problem is equivalent to the existence of a single finite $N$ working for all trees. Guidability drives the forward direction: an accepting run of the hypothetical $J$-automaton determines Eve's register choices, and the pumping lemma ensures no counter can reach $N+1$ on a branch that is even-dominated in the guiding run.

What would settle it

Exhibit an automaton $B$ guiding an automaton $A$, accepting runs $\rho_B$ and $\rho_A$ on some tree, and a pumpable pair of positions $u, uv$ with $\rho_A(u)=\rho_A(uv)$ and $\rho_B(u)=\rho_B(uv)$, such that the highest priority in $\rho_B$'s segment from $u$ to $uv$ is even while the highest in $\rho_A$'s segment is odd; that refutes Lemma 3 and, since Lemma 5 relies on it, invalidates the forward direction of Theorem 1.

Watch

Extended reading notes

Core claim

The central result is Theorem 1: given a guidable automaton $A$ and an index $J$, the language $L(A)$ is $J$-feasible exactly when there exists a natural number $N$ such that for every $\Sigma$-tree $t$, $t \in L(A)$ if and only if Eve wins the parity transduction game $T^N_J(G(A,t))$ on the acceptance parity game of $t$ in $A$. The forward direction assumes a $J$-automaton $B$ recognizing $L(A)$ and lets $B$ guide Eve: her register choices follow $B$'s priorities, and a pumping argument (Lemma 3) shows that the counters can never overflow, because an overflow would produce a pumpable segment where $B$'s run is even-dominated but $A$'s run is odd-dominated, contradicting guidability. The backward direction encodes the configurations of $T^N_J$ as states of a finite automaton and composes it with $A$ to obtain an automaton of index $J$ recognizing the same language. Since every regular tree language is recognized by some guidable automaton, a fact the paper recalls, the characterization covers all regular tree languages.

Load-bearing premise

The main theorem's forward direction rests on the lemma that whenever a repeating segment of the guiding run is dominated by an even priority, the corresponding segment of the guided run is even too, and this lemma is only sketched in the paper.

Editorial extensions

If this is right

If $L(A)$ is $J$-feasible, the witness automaton $B$ of size $|B|$ gives a concrete bound $N = |A||B| + 1$ for which Eve can win $T^N_J$ on every accepted tree, so the existential bound in Theorem 1 is instantiated by a product of the two automata sizes.
Conversely, whenever such a uniform $N$ exists, the paper constructs a genuine $J$-automaton by composing $A$ with a finite-state automaton whose states are the configurations of the transduction game; this yields $J$-feasibility.
The games are parity games, hence determined, so for each tree $t$ and each $N$ exactly one of Eve or Adam wins $T^N_J(G(A,t))$; this makes the characterization two-sided rather than a one-way containment.
Because every regular tree language is recognized by a guidable automaton, the equivalence is not restricted to a special subclass: it holds for all regular tree languages.
As the paper notes, encoding the counters into the distance of a distance-parity automaton recovers the shape of the established reduction to distance-parity automata, connecting the two approaches.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

A natural testable extension is to ask whether the bound $N = |A||B|+1$ can be turned into an effective procedure: if a candidate $J$-automaton $B$ and a bound are given, the construction of Lemma 6 yields the equivalent $J$-automaton, which could support a search algorithm for $J$-feasibility over guidable automata.
The counter structure suggests a quantitative measure of the 'distance' between a language's true index and a proposed index $J$: the minimal $N$ needed (if any) behaves like a budget of tolerated odd dominations, which may give finer information than the bare index and could be compared directly against distance costs in distance-parity automata.
If Lemma 3 were formalized and made constructive, it would yield an algorithm for synthesizing Eve's winning register strategy from the guiding run, potentially simplifying the practical computation of winning strategies in these games.
One could investigate whether the same game characterization extends to non-guidable automata, or whether the failure of local preservation of even domination is exactly the obstruction; the paper's theorem does not address non-guidable automata.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Colleague,

The paper is an informal note giving a game-based characterization of the Mostowski index for guidable tree automata, extending Lehtinen's register games with counters. The main theorem says J-feasibility of L(A) for guidable A is equivalent to the existence of N such that the parity transduction game T^N_J on G(A,t) captures membership. That statement is new, and it offers a simpler-looking route to the Colcombet-Löding reduction. The authors are upfront that it's informal, which is honest.

What's genuinely good: the parity transduction game is a natural extension, the counter mechanism is neat, and the backward direction (Lemma 6) is plausible—encode configurations into a finite automaton, compose with A, use determinacy. It's sketched but standard and likely fixable. Lemma 4, Adam winning on non-even graphs, is essentially correct.

The soft spot is the forward direction, Lemma 5. The strategy is to pick register j when the guiding B-run has priority in [2j,2j+1]. The proof then asserts that infinitely often r_j* = i* when j* is picked, where 2j* is B's maximal recurrent priority and i* is A's. That equality does not follow. The register r_j* is updated to the A-priority at the moment it's chosen, so it equals i* only if A's i* occurs at the same positions where B has priority 2j* (or 2j*+1). Guidability gives global acceptance preservation, not local alignment of maxima. The stress-test note is right to flag this. The counter-overflow argument that follows is meant to handle the case where r_j* is odd, but it rests on an invariant about pumpable segments that is only asserted, not derived. Lemma 3 itself is proved in a paragraph and seems okay, but the forward implication as written is unsupported.

This is a real gap, but it may be repairable. The claimed equivalence is plausible, and the machinery is close to existing work. I'd like to see a full version with rigorous proofs, especially for the register/counter invariant. The citation pattern is fine: self-citation to Lehtinen's game is appropriate, and Colcombet-Löding gets credit.

Who is it for? People working on the Mostowski index or game-based reductions. I'd bring it to a reading group and encourage the authors to write it up properly. I wouldn't cite it in my own work until the proof is solid.

Recommendation: send to review, but expect heavy revision; the current form should not be accepted. It deserves referee time because the idea is new and the area is important.

Referee Report

4 major / 6 minor

Summary. The paper introduces "parity transduction games" T^N_J, which extend Lehtinen's register games from her quasipolynomial-time algorithm for parity games by adding bounded counters. The main result (Theorem 1) states that for a guidable nondeterministic parity tree automaton A, the language L(A) is J-feasible (i.e., recognized by some nondeterministic parity tree automaton with priorities in the index J) if and only if there exists a natural number N such that for every Σ-tree t, t is in L(A) exactly when Eve wins the parity transduction game T^N_J played on the acceptance game G(A,t). The forward direction uses the guidability of A: given an accepting run of a hypothetical J-automaton B for L(A), a guided run of A is obtained, and Eve's register strategy in the transduction game is based on the priorities of that guiding run; a pumping argument is invoked to show that the counters never overflow. The backward direction encodes the finite-state configuration space of the transduction game into a nondeterministic J-automaton and composes it with A. The paper is explicitly labeled an informal note, and all proofs are presented as sketches.

Significance. If correct, the main theorem provides a new game-based characterization of the Mostowski (parity) index problem, which is a long-standing open problem. The use of guidable automata is well motivated: they are fully expressive for regular tree languages, so the characterization applies to the general index problem. The connection between Lehtinen's register games and the Colcombet-Löding distance-parity automaton reduction is conceptually attractive, and the paper's approach has the potential to yield a more accessible proof of this important reduction. The paper also benefits from grounding the proof in an existing, well-studied game framework (Lehtinen's register games) and from explicitly identifying guidability as the key automaton-theoretic condition. At the same time, the significance is currently limited by the informal, sketch-level presentation: the soundness of the central construction is plausible but not yet established at the standard of rigor expected for a journal publication.

major comments (4)

[Lemma 5, Section 3] The claim "inﬁnitely often, rj∗ = i∗ when the register j∗ is picked" is not justified by the text. The equality does not follow immediately from the fact that i* and 2j* are the respective limsup priorities along the branch: the runs ρA and ρB are not aligned, and the register r_j* can be reset to a lower value each time j* is picked. A rigorous proof would need to argue that every occurrence of an A-priority equal to i* (after the cutoff point) sets r_j* to i*, because at such a step the register chosen by the strategy has index at most j*, and the update rule raises all higher-index registers to max(i*, ·); since r_j* can only decrease when j* itself is picked, infinitely many j* picks must occur after an A-i* event and therefore see r_j* = i*. As written, this load-bearing claim is unsupported.
[Lemma 5, Section 3 (counter-overflow argument)] The counter-overflow argument is only sketched. To prove that no counter c_{i,2j*} overflows, the text asserts that an overflow would yield a pumpable segment whose A-maximum is odd i and whose B-maximum is even 2j*, contradicting Lemma 3. However, the construction of this segment is not made precise: one must specify the sequence of N+1 occurrences of the pair (A-priority i, B-priority 2j*), apply the pigeonhole principle with N > |A×B| to obtain repeated state pairs, and then verify that the segment between the repeated positions indeed has no priority larger than i in A and no priority larger than 2j* in B, so that Lemma 3 applies. This step is essential because it is the only mechanism that rules out infinitely many outputs 2j*+1, and without it the output sequence could have an odd limsup.
[Lemma 3, Section 2.3] The proof of Lemma 3 is a sketch. The construction of t*, ρ*A and ρ*B should be formalized: the recursive replacement of subtrees needs a precise definition, and one must prove that ρ*A is exactly the run of A guided by ρ*B (i.e., ρ*A = g(ρ*B)). The argument that every branch of ρ*B is accepting is compressed into a single sentence; in particular, the branches of the form u·v^k·w with w ≠ v^ω require a careful justification that their suffixes are clones of accepting branches of ρB. Since Lemma 5 relies on Lemma 3 for the pumping argument, this lemma must have a complete proof.
[Section 3, definition of T^N_J] The definition of the parity transduction game T^N_J contains ambiguities that affect the automaton construction in Lemma 6. The update rule "∀j′ < j, crj ,j ′ := 0" is unclear; the second index should presumably refer to the counter associated with the current value i (e.g., c_{i,j′}), not to r_j. The order between the output step and the register/counter updates is also not fully specified. Since the states of the automaton C in Lemma 6 are the configurations of T^N_J, a rigorous treatment of the game is necessary for the backward direction to be verifiable.

minor comments (6)

[Abstract / Section 1] The abstract contains several typos: "based on on the games" should be "based on the games", "automaton" should be "automaton", and "interger" should be "integer".
[Section 2.1] In the definition of a strategy for Eve, the phrase "if ρ|n ends in a vertex v ∈ VE, σ(ρ|n) follows an edge from v" should explicitly state that σ is defined on finite plays ending in Eve vertices; the current wording is slightly ambiguous.
[Lemma 3, Section 2.3] The line "ρA(u) = ρB(u) = ρA(u·v) = ρB(u·v)" is a typo: it should read ρA(u) = ρA(u·v) and ρB(u) = ρB(u·v), since ρA and ρB take values in different state sets.
[Lemma 5, Section 3] The text says "T N k outputs a 2j∗" where the subscript "k" is undefined; it should be "T^N_J". Also, "looses" should be "loses".
[Theorem 1, Section 3] The statement of Theorem 1 uses "n" for the bound in the existential quantifier, while the rest of the paper uses "N"; this inconsistent notation should be harmonized.
[Lemma 4, Section 3] In the proof of Lemma 4, the phrase "the game only outputs min(I)" when j*=0 should refer to the output of the register r0, which is 1 if it exists; the notation ρ(p) is also used without definition (it should likely be L(e) or the priority of the current position).

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; the main theorem is derived from guidability and game definitions, with only a non-load-bearing self-citation to Lehtinen's register games.

full rationale

The derivation is self-contained in the relevant sense. The paper's only self-citation is [4], Lehtinen's register games, and it is used as the starting point for defining parity transduction games (Section 3, "based on the register games from Lehtinen's algorithm in [4]"); however, the properties that the proof actually needs—determinacy of T^N_J, monotonicity of registers, and the counter-overflow contradiction—are re-proved in Lemmas 4 and 5 rather than imported as black boxes. The expressiveness of guidable automata is imported from Colcombet and Löding [2, Theorem 1], not from the authors' own work. Theorem 1's equivalence is not definitional: T^N_J(G(A,t)) is defined independently of J-feasibility, with J and N as game parameters; the forward direction translates a witnessing J-automaton's run into Eve's register strategy using the guidability hypothesis, and the backward direction constructs a J-automaton whose state space is the finite configuration set of the game. Lemma 5's contested step ("infinitely often, r_j* = i* when the register j* is picked") may be a proof gap, but it does not assume the theorem's conclusion; it is an assertion about the dynamics of the game under the described strategy. No fitted parameter is renamed as a prediction, and no load-bearing claim is justified only by a self-citation. Therefore no circularity.

Assumptions & free parameters 0 free parameters · 3 assumptions · 1 invented entities

The central claim rests on the cited theorem that guidable automata are fully expressive, and on the informally proved pumping lemma. No numerical parameters are fitted to data.

assumptions (3)

standard math Borel determinacy of parity games
Used to conclude that T^N_J(G) is determined (Section 3, 'Note that whatever its input, T^N_J corresponds to a parity game, and is therefore determined.').
domain assumption Guidable automata are fully expressive (Theorem 2 from [2])
The main theorem is stated only for guidable automata; the proof of the forward direction assumes a guide exists for any J-feasible language.
domain assumption Guidability implies the local domination preservation (Lemma 3)
Proved in Section 2.3 but relies on a pumping construction; the proof is informal and load-bearing for Lemma 5.

invented entities (1)

Parity transduction game T^N_J
purpose: Characterize J-feasibility of guidable automata via the existence of a counter bound N
A formal game defined in Section 3; its equivalence to the index problem is exactly the paper's theorem, so it is not independently evidenced.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Mostowski Index via extended register games." pith.science (2026). https://pith.science/paper/ZWU53VXD

@misc{pith2026241216793,
  author       = {Pith},
  title        = {Pith review of: Mostowski Index via extended register games},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ZWU53VXD}},
  note         = {Machine review of arXiv:2412.16793}
}

read the original abstract

The parity index problem of tree automata asks, given a regular tree language L, what is the least number of priorities of a nondeterministic parity tree automaton that recognises L. This is a long-standing open problem, also known as the Mostowski or Rabin-Mostowski index problem, of which only a few sub-cases and variations are known to be decidable. In a significant step, Colcombet and L\"oding reduced the problem to the uniform universality of distance-parity automata. In this brief note, we present a similar result, with a simplified proof, based on on the games in Lehtinen's quasipolynomial algorithm for parity games. We define an extended version of these games, which we call parity transduction games, which take as parameters a parity index J and an integer bound N. We show that the language of a guidable automaton A is recognised by a nondeterministic automaton of index J if and only if there is a bound N such that the parity transduction game with parameters J and N captures membership of the language, that is, for all trees t, Eve wins the parity transduction game on the acceptance parity game of t in A if and only in t is in L(A).

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

A Dichotomy Theorem for Ordinal Ranks in MSO
cs.LO 2025-01 accept novelty 7.0 of 10

For any MSO formula over the infinite binary tree whose existential witness is well-founded, the minimal ordinal rank bound is either strictly below ω² or equal to ω1, and it is decidable which holds.

Reference graph

Works this paper leans on

9 extracted references · 9 canonical work pages · cited by 1 Pith paper

[1]

Deciding the weak deﬁnability of büchi deﬁnable tree l anguages

Thomas Colcombet, Denis Kuperberg, Christof Löding, an d Michael Vanden Boom. Deciding the weak deﬁnability of büchi deﬁnable tree l anguages. In Annual Conference for Computer Science Logic , 2013

work page 2013
[2]

The non-determin istic mostowski hierarchy and distance-parity automata

Thomas Colcombet and Christof Löding. The non-determin istic mostowski hierarchy and distance-parity automata. In International Colloquium on Automata, Languages and Programming , 2008

work page 2008
[3]

Rabin- mostowski index problem: A step beyond deterministic autom ata

Alessandro Facchini, Filip Murlak, and Michal Skrzypcz ak. Rabin- mostowski index problem: A step beyond deterministic autom ata. In 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science , pages 499–508, 2013

work page 2013
[4]

A modal mu perspective on solving pa rity games in quasi-polynomial time

Karoliina Lehtinen. A modal mu perspective on solving pa rity games in quasi-polynomial time. In Proceedings of the 33rd Annual ACM/IEEE Sym- posium on Logic in Computer Science , LICS ’18, page 639–648, New York, NY, USA, 2018. Association for Computing Machinery

work page 2018
[5]

Logic and automata over inﬁnite trees

Christof Löding. Logic and automata over inﬁnite trees. Habilitation, RWTH Aachen, Germany, 2009. 10

work page 2009
[6]

Donald A. Martin. Borel determinacy. Annals of Mathematics , 102(2):363– 371, 1975

work page 1975
[7]

On guidable inde x of tree au- tomata

Damian Niwinski and Michal Skrzypczak. On guidable inde x of tree au- tomata. In Filippo Bonchi and Simon J. Puglisi, editors, 46th Inter- national Symposium on Mathematical Foundations of Compute r Science, MFCS 2021, August 23-27, 2021, Tallinn, Estonia , volume 202 of LIPIcs, pages 81:1–81:14. Schloss Dagstuhl - Leibniz-Zentrum für I nformatik, 2021

work page 2021
[8]

Deciding nondete rministic hierar- chy of deterministic tree automata

Damian Niwinski and Igor Walukiewicz. Deciding nondete rministic hierar- chy of deterministic tree automata. In Ruy J. G. B. de Queiroz and Patrick Cégielski, editors, Proceedings of the 11th Workshop on Logic, Language, Information and Computation, WoLLIC 2004, Fontainebleau, France, July 19-22, 2004 , volume 123 of Electronic Notes in Theoretical Comput...

work page 2004

Show all 9 references

[9]

Deciding the to pological com- plexity of büchi languages

Michal Skrzypczak and Igor Walukiewicz. Deciding the to pological com- plexity of büchi languages. In Ioannis Chatzigiannakis, Mi chael Mitzen- macher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 201...

2016

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.

[1] [1]

Deciding the weak deﬁnability of büchi deﬁnable tree l anguages

Thomas Colcombet, Denis Kuperberg, Christof Löding, an d Michael Vanden Boom. Deciding the weak deﬁnability of büchi deﬁnable tree l anguages. In Annual Conference for Computer Science Logic , 2013

work page 2013

[2] [2]

The non-determin istic mostowski hierarchy and distance-parity automata

Thomas Colcombet and Christof Löding. The non-determin istic mostowski hierarchy and distance-parity automata. In International Colloquium on Automata, Languages and Programming , 2008

work page 2008

[3] [3]

Rabin- mostowski index problem: A step beyond deterministic autom ata

Alessandro Facchini, Filip Murlak, and Michal Skrzypcz ak. Rabin- mostowski index problem: A step beyond deterministic autom ata. In 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science , pages 499–508, 2013

work page 2013

[4] [4]

A modal mu perspective on solving pa rity games in quasi-polynomial time

Karoliina Lehtinen. A modal mu perspective on solving pa rity games in quasi-polynomial time. In Proceedings of the 33rd Annual ACM/IEEE Sym- posium on Logic in Computer Science , LICS ’18, page 639–648, New York, NY, USA, 2018. Association for Computing Machinery

work page 2018

[5] [5]

Logic and automata over inﬁnite trees

Christof Löding. Logic and automata over inﬁnite trees. Habilitation, RWTH Aachen, Germany, 2009. 10

work page 2009

[6] [6]

Donald A. Martin. Borel determinacy. Annals of Mathematics , 102(2):363– 371, 1975

work page 1975

[7] [7]

On guidable inde x of tree au- tomata

Damian Niwinski and Michal Skrzypczak. On guidable inde x of tree au- tomata. In Filippo Bonchi and Simon J. Puglisi, editors, 46th Inter- national Symposium on Mathematical Foundations of Compute r Science, MFCS 2021, August 23-27, 2021, Tallinn, Estonia , volume 202 of LIPIcs, pages 81:1–81:14. Schloss Dagstuhl - Leibniz-Zentrum für I nformatik, 2021

work page 2021

[8] [8]

Deciding nondete rministic hierar- chy of deterministic tree automata

Damian Niwinski and Igor Walukiewicz. Deciding nondete rministic hierar- chy of deterministic tree automata. In Ruy J. G. B. de Queiroz and Patrick Cégielski, editors, Proceedings of the 11th Workshop on Logic, Language, Information and Computation, WoLLIC 2004, Fontainebleau, France, July 19-22, 2004 , volume 123 of Electronic Notes in Theoretical Comput...

work page 2004