Mostowski Index via extended register games
Olivier Idir, Karoliina Lehtinen
TL;DR
This work tackles the parity index problem for regular tree languages by introducing parity transduction games parameterized by an output index $J$ and a counter bound $N$. It shows that a guidable automaton $\mathcal{A}$ has language $\Lang(\mathcal{A})$ of index $J$ exactly when there exists $N$ such that, for every input tree $t$, Eve wins the $\Reg{J}{N}$-transduction of the acceptance game on $t$ iff $t \in L(\mathcal{A})$, thereby connecting membership to bounded, on-the-fly priority mapping. The approach extends Lehtinen's quasipolynomial parity-game framework with counters and leads to a bidirectional correspondence: one can deduce $J$-feasibility from such games and, conversely, construct a $J$-index automaton from a transduction-game representation. This provides a simplified, game-based pathway mirroring Colcombet–Löding's reduction to distance-parity universality and may illuminate decidability borders for the parity index problem.
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öding 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).