Using games and universal trees to characterise the nondeterministic index of tree languages

TL;DR

The paper tackles the long-standing nondeterministic parity index problem for ω-regular tree languages by developing three interconnected characterisations that connect parity games, attractor decompositions, and universal trees. It extends Lehtinen's register game with counters to form a parity transduction game Reg${J}{n}$, providing an alternative proof framework for a Colcombet–Löding reduction. A second characterisation uses attractor decompositions and a parameterised Strahler notion, the $n$-Strahler number, to relate $J$-feasibility to bounded structural complexity of runs. A third characterisation translates these insights into universal trees extended to automata, showing that $[1,2j]$-feasibility corresponds to the existence of a universal tree with $n$-Strahler number $j$ (finite for Büchi-feasibility). While decidability remains unresolved, the work clarifies deep connections among $J$-feasibility, attractor decompositions, and universal trees, and highlights pathways for progress on the index problem.

Abstract

The parity index problem of tree automata asks, given a regular tree language $L$ and a set of priorities $J$, is $L$ $J$-feasible, that is, recognised by a nondeterministic parity automaton with priorities $J$? This is a long-standing open problem, of which only a few sub-cases and variations are known to be decidable. In a significant but technically difficult step, Colcombet and Löding reduced the problem to the uniform universality of distance-parity automata. In this article, we revisit the index problem using tools from the parity game literature. We add some counters to Lehtinen's register game, originally used to solve parity games in quasipolynomial time, and use this novel game to characterise $J$-feasibility. This provides a alternative proof to Colcombet and Löding's reduction. We then provide a second characterisation, based on the notion of attractor decompositions and the complexity of their structure, as measured by a parameterised version of their Strahler number, which we call $n$-Strahler number. Finally, we rephrase this result using the notion of universal tree extended to automata: a guidable automaton recognises a $[1,2j]$-feasible language if and only if it admits a universal tree with $n$-Strahler number $j$, for some $n$. In particular, a language recognised by a guidable automaton $A$ is Büchi-feasible if and only if there is a uniform bound $n\in \mathbb{N}$ such that all trees in the language admit an accepting run with an attractor decomposition of width bounded by $n$, or, equivalently, if and only $A$ admits a \textit{finite} universal tree. While we do not solve the decidability of the index problem, our work makes the state-of-the-art more accessible and brings to light the deep relationships between the $J$-feasibility of a language and attractor decompositions, universal trees and Lehtinen's register game.

Figures (2)

• Figure 1: An "ordered tree" of depth 4, of 3-"Strahler number" 3, as exemplified by the red edges.
• Figure 2: The recursion step in the construction of $\mathcal{U}_{\alpha,n,k,d}$.

Theorems & Definitions (32)

• Theorem 1
• Theorem 2
• Theorem 3
• Lemma 3
• Lemma 3
• Theorem 4: Guidable
• Theorem 4
• Lemma 4
• Lemma 4
• Lemma 4