Rabin–Mostowski index problem

A finite set of rules reads a tree that branches left and right forever. Can exactly the same trees be recognized using a smaller range of long-run checking labels? These labels are priorities: a branch succeeds when the greatest priority recurring infinitely often is even. A branch labeled 3 once, then 1, 2, 1, 2 forever succeeds; alternating 2 and 3 forever fails. A nondeterministic automaton may choose a run, but one accepting run must satisfy the rule on every branch.[1] [2]

Can a simpler long-run acceptance condition recognize exactly the same indefinitely branching inputs? Along one branch, 3 followed by repeating 1, 2 has greatest infinitely recurring priority 2 and accepts; repeating 2, 3 instead rejects. A tree run must pass on every branch, and a nondeterministic automaton accepts an input if some run does so.

Given a finite nondeterministic parity automaton $A$ over full infinite binary trees labeled by a finite alphabet $\Sigma$, and a requested priority interval $[i,j]$ with $i\in\{0,1\}$ and $j\geq i$, decide whether another nondeterministic automaton $B$ over the same alphabet recognizes exactly $L(A)$ using only priorities in that interval. The greatest infinitely recurring priority must be even. The procedure must halt; no polynomial-time bound or limit on the number of states of $B$ is imposed.[1] [2]

For an arbitrary tree automaton, no general algorithm is known that decides whether a requested smaller priority range will suffice. Algorithms do exist for infinite strings and for some restricted tree automata. Branching makes the general problem harder.[1] [2]

The v1 register/counter note characterizes the requested index for a guidable automaton by existence of one finite counter bound that works uniformly over all input trees. It does not supply a general method for finding the bound. STACS 2026 proves undecidability for monadic logic extended with index queries and parameters, while explicitly leaving a single unparameterized index query potentially decidable. That richer-logic theorem does not resolve this target.[1] [2]

Automata describe rules for behavior that continues indefinitely. Understanding the smallest necessary acceptance condition would reveal which distinctions are essential and which are merely artifacts of the original description.[1] [2]

A finite automaton can describe conditions such as recurring success or eventual absence of failure on infinitely many paths. Priority ranges organize the complexity of these long-run conditions separately from the amount of finite-state memory: allowing more states need not remove a language’s acceptance requirements. The index problem therefore connects semantic expressiveness to effective classification. Its game reformulations must preserve behavior across all input trees, not just find a winner in one finite game.[1] [2]