Using Games and Universal Trees to Characterise the Nondeterministic Index of Tree Languages

Parity games are infinite two-player games in which two players, Adam and Eve, take turns moving a token along the edges of a graph labelled with integer priorities. Eve’s goal is to ensure that the infinite path taken by the token satisfies the parity condition, that is, that the highest priority occuring infinitely often along the path is even. The acceptance of a tree by a parity tree automaton is determined by whether Eve wins a parity game based on the input tree and the automaton.

In this article, we use the data-structure introduced in Lehtinen’s quasipolynomial parity game algorithm [15]. Lehtinen reduces solving a parity game to solving a new game, in which Eve must map the original game’s priorities into a smaller priority range using a purpose-built data-structure, while guaranteeing that the sequence of outputs in this smaller range still satisfies the parity condition. Lehtinen shows that for a parity game of size $n$, Eve wins if and only if she also wins this new game with output range $O(\log n)$, which can be solved in quasipolynomial time.

Here we extend this game to the acceptance parity games of nondeterministic parity tree automata, that is, parity games with unbounded or even infinite arenas. We furthermore add some counters (inspired by the Colcombet and Löding construction), which give Eve some additional (but bounded) leeway in her mapping. We obtain a game that we call the parity transduction game ${𝒯}_J^n(G)$, played over a parity game $G$, parameterised by the output priority range $J$ , and the bound $n$ on the counters.

Our first contribution is showing that the $J$-feasibility of the language of a guidable automaton $A$ (and we can always make the input guidable) is characterised by the existence of an integer $n$ such that the parity transduction game with parameters $J$ and $n$ coincides with the acceptance game of $A$, written $𝒢(A,t)$ for an input tree $t$. In other words, a language is $J$-feasible whenever there is a uniform parameter $n$, such that whenever Eve wins the acceptance game $𝒢(A,t)$, she also wins the transduction game over it, with output range $J$ and parameter $n$.

This corresponds to our version of the Colcombet-Löding reduction. We then proceed to reinterpret this characterisation in terms of attractor decompositions and universal trees.

describe the structure of Eve’s winning strategies in a parity game, or, equivalently, of accepting runs of a parity tree automaton. While this notion appears at least implicitly in many seminal works, e.g. Zielonka’s algorithm for parity games [27], Kupferman and Vardi’s automata transformations [14] and Klarlund’s [13] proof of Rabin’s complementation theorem, it has more recently been explicitly studied for mean payoff parity games [6] and parity games [7, 12].

While similar in spirit and structure to progress-measures [11], which count the number of odd priorities that might occur before a higher priority, attractor decompositions are more suitable for parity games on infinite arenas, where Eve might see an unbounded number of odd priorities in a row, as long as she is advancing in the attractor of some larger even priority. While progress measures, bounded by the size of a finite game, can be seen as a way to reduce parity games to safety games, here we use attractor decompositions with bounded structure to reduce the priority range of the parity condition. Like progress-measures, attractor decompositions have a tree-like structure, where the play only moves to the right if a suitably high even priorities occurs. The structure of these trees turns out to be closely tied to the index of a language.

The Strahler number of a tree $t$ consists in the largest $h$ such that $t$ admits a complete binary tree of height $h$ as a minor. Daviaud, Jurdziński and Thejaswini [8] proved an equivalence between the output range that Eve needs in Lehtinen’s game, called the game’s register index, and the Strahler-number of the attractor decompositions of Eve’s strategies. Inspired by this, we define, for $n\in \mathbb{N}$, the $n$-Strahler number of a tree $t$, that consists in the largest $h$ such that $t$ admits a complete $(n+1)$-ary tree of height $h$ as a minor (by subtree deletion and single-child contraction; we do not allow edge contraction in the presence of siblings). The Strahler number corresponds to our $1$-Strahler number. Our second characterisation of the index of a languages is based on the $n$-Strahler number of attractor decompositions.

In particular, Büchi feasibility coincides with the existence of a uniform bound on the width (i.e branching degree) of attractor decompositions needed by Eve. Finally, we restate this result in terms of universal trees, extended to automata, as follows.

Given a set $𝒯$ of ordered trees of bounded depth, a tree $U$ is said to be universal for $𝒯$ if all $t\in 𝒯$ can be obtained from $U$ by removing subtrees. We then say that $t$ is isomorphically embedded in $U$. This elegant notion emerged in the analysis of quasi-polynomial time parity game algorithms, as a unifying combinatorial structure that can be extracted from the different algorithms [5].

We say that an ordered tree $U$ is universal for an automaton $A$ if for all regular trees in the language of $A$, there exists an accepting run with an attractor decomposition (seen as a tree) that can be isomorphically embedded in $U$.

Then, the $[1,2j]$-feasibility of the language of a guidable automaton $A$ is characterised by the existence of an ordered tree universal for $A$ of $n$-Strahler $j$, for some $n\in \mathbb{N}$. Büchi-feasibility is equivalent to the existence of a finite universal tree for $A$.

While our work does not give us the decidability of the index problem, it provides new tools for tackling it and makes the state-of-the-art more accessible by relating it to other familiar concepts. We hope that the deep link between the index of a language and the structure of attractor decompositions will be helpful for future work. The remarkably simple characterisation of Büchi feasible languages, as those with attractor decompositions of bounded width, or, equivalently a finite universal tree, is particularly encouraging, as deciding Büchi-feasibillity is the next challenge for advancing on the index problem.

A full version of this article, with all the missing proofs, can be found on Arxiv [16].

If the underlying play in the parity graph sees a maximal odd priority $i$ infinitely often, then the most significant register $r_j$ that Eve picks infinitely often contains $i$ infinitely often when picked. The counter $c_{i,j}$, which is eventually never reset, reaches $n$ infinitely often, making the maximal output priority that occurs infinitely often odd. $◀$

Then, it remains to show that if the language of guidable $A$ is $J$-feasible, then for some $n\in \mathbb{N}$ Eve wins ${𝒯}_J^n(𝒢(A,t))$ for all $t\in ℒ(A)$. To do so, we first analyse the relation between guided and guiding runs, and show that the preservation of global acceptance implies a more local version that resctricts differences in the parity of the dominant priority over long segments of both runs. We will then use this to show that Eve can win the transduction game by using a run of $A$ guided by an accepting run of an equivalent $J$-automaton and choosing registers corresponding to the priorities of the guiding run.

The following lemma, obtained by a simple pumping argument (see full version) expresses that between all pumpable pairs of states, that is, pairs of states that are not distinguished by either run, if the guiding run is dominated by en even priority, then so is the guided one.

We now capture this relation with the notion of a labelling being $n$-bounded by the other. Let $L_I:E\to I$ and $L_J:E\to J$ be two labellings of a graph $G=(V,E)$ (or tree) and let $n\in \mathbb{N}$. We say that $L_I$ is $n$-bound by $L_J$ if there is no finite path $\pi$ in $G$, segmented into consecutive paths ${\pi }_0,{\pi }_1,\mathrm{\dots }{\pi }_n$ such that for some odd $i$ and some even $j$, the maximal priority on the $L_I$- and $L_J$-labels of each ${\pi }_m,m\in [0,n]$ are $i$ and $j$, respectively.

From Lemma 9 we obtain that the labelling induced by a guided run is $n$-bound by the one induced by its guide, with $n$ the product of the sizes of the two automata:

We use $n$-boundedness to show that Eve can use a run ${\rho }_B$ of an equivalent $J$-automaton to choose her registers to win in ${𝒯}_J^{n+1}({\rho }_A)$ for ${\rho }_A$ accepting run of $A$ guided by ${\rho }_B$.

We will describe a winning strategy $\sigma$ for Eve in ${𝒯}_J^n({\rho }_I)$. We recall that at each step, she has two choices : the choice of register and the choice of some $i\in I$ (choice $\mathrm{♯}$). We once again suppose for convenience that $\min (J)\in \{1,2\}$. After seeing an edge of priority $i^{\prime }$ in ${\rho }_I$, Eve chooses $i:=i^{\prime }$. Given priority $j^{\prime }$ seen in ${\rho }_J$, for $j:=\lfloor \frac{j^{\prime }}{2}\rfloor$, Eve chooses the register $r_j$. This strategy being fixed, let us verify that Eve wins in all plays consistent with $\sigma$. Let $b$ such a play.

As ${\rho }_J$ is even, its maximal infinitely recurring priority along $b$ is even; we denote it $2j^{\ast }\in J$ (and $j^{\ast }\ne 0$, as $0\notin J$). We look past the position where we no longer see any priority superior to $2j^{\ast }$. Then, as $2j^{\ast }$ is infinitely recurring, we observe that infinitely often the output is $w_l=2j^{\ast }$, as this is the default output when choosing the register $r_{j^{\ast }}$. Let us show that the game outputs at most $\lceil \frac{|I|}{2}\rceil$ times $2j^{\ast }+1$.

If it were to output $2j^{\ast }+1$ more than $\lceil \frac{|I|}{2}\rceil$ times, then there would be some counter $c_{i,2j^{\ast }}$ that would reach $n+2$ twice, for some odd $i$. We look at the first time $t_0$ where this counter reaches $n+2$: after time $t_0$, the counter $c_{i,j^{\ast }}$ has value $0$. We look at the $n+2$ times at which $c_{i,2j^{\ast }}$ is incremented after $t^{\ast }$, denoted ${(t_l)}_{l\in [1,n+2]}$, and note ${\pi }_l$ the path between $t_l$ and $t_{l+1}$. Along these paths, we encounter no priority greater than $i$ in ${\rho }_I$, nor greater than $j^{\ast }$ in ${\rho }_J$, as these would reset $c_{i,j^{\ast }}$ (except, possibly, at time $t_{n+2}$ where we can witness a $i^{\prime }>i$ after the counter has reached $n+2$). Additionally, for $l\in [1,n+1]$, as $c_{i,j^{\ast }}$ is incremented at time $t_l$, then there is a $2j^{\ast }$ in ${\rho }_J$ at the edge preceding $t_l$ (as this priority cannot be $2j^{\ast }+1$) and $r_{j^{\ast }}=i$ at time $t_l$, after which $r_{j^{\ast }}$ becomes the priority just seen in ${\rho }_I$. Therefore, $\forall l\in [1,n+1]$ between $t_{l-1}$ and $t_l$, we see at least once a $2j^{\ast }$ in ${\rho }_J$, and at least once a $i$ in ${\rho }_I$ – and they thus dominate these segments. This contradicts that ${\rho }_I$ is $n$-bound by ${\rho }_J$; therefore the output $2j^{\ast }+1$ does not repeat more than $\lceil \frac{|I|}{2}\rceil$ times.

If $2j^{\ast }=\max (J)$, we set $t_0:=0$. The hypothesis used for the previous reasoning still hold – initially all counters have value 0 and there is no $2j^{\ast }+1$ in ${\rho }_J$ – so we obtain that there no counter $c_{i,j\ast }$ that reaches $n+2$, which prevents instant loss. Therefore, the play along $b$ is won by Eve, which concludes. $◀$

Lemma 8 implies that Eve loses ${𝒯}_J^{n+1}(𝒢(A,t))$ for $t\notin ℒ(A)$. If $ℒ(A)$ is $J$-feasible as witnessed by a $J$-automaton $B$, then for all $t\in ℒ(A)$, from Lemma 10, Eve has a run ${\rho }_A$ that is $n$-bounded by an accepting run of $B$, which, from Lemma 11, implies that Eve wins ${𝒯}_J^{n+1}(𝒢(A,t))$, concluding the proof of Theorem 1.

We proceed by induction on $(d,k)$ ordered by the sum $d+k$.

• $\mathrm{■}$

  If $(d,k)=(1,1)$, the result is immediate.

• $\mathrm{■}$

  Else, by induction ${𝒰}_{n,k-1,d-1}$ is defined and has $n$-Strahler number $k-1$, and if defined ${𝒰}_{n,k,d-1}$ has $n$-Strahler number $k$. We observe that ${𝒮}_n({𝒰}_{n,k,d})=k$, as it has at most $n$ children of $n$-Strahler number $k$, and more than $n$ children of $n$-Strahler number $k-1$.

$◀$

We can now prove its universality:

We reason by recurrence on $(d,k)$ ordered by the sum $d+k$.
If $k=d=1$, then $\forall T\in 𝒯,T=⟨⟩$, and is trivially isomorphically embedded in ${𝒰}_{n,1,1}$.
Else, let $(d,k)\ne (1,1)$, and we suppose by recurrence that $\forall (d^{\prime },k^{\prime })$ such that , the proposition holds. If , then there is no ordered tree of depth $d$ and $n$-Strahler number $k$: they all are of $n$-Strahler number at most $d$. Then, by recurrence, as , ${𝒰}_{n,d,d}$ is universal for $𝒯$.

Else, ${𝒰}_{n,k,d}=⟨\omega ({𝒰}_{n,k-1,d-1}),{𝒰}_{n,k,d-1},\omega ({𝒰}_{n,k-1,d-1}),\mathrm{\dots },{𝒰}_{n,k,d-1},\omega ({𝒰}_{n,k-1,d-1})⟩$, with $n$ repetitions of ${𝒰}_{\alpha ,n,k,d-1}$ if it is defined (else zero such repetition). Let $T\in 𝒯$. By definition, if $T=⟨⟩$, it is isomorphically embedded in all ordered trees. Else, for $T=⟨{(T_i)}_{i\in I}⟩$, then ${𝒮}_n(T)⩽k$, and notably it admits at most $n$ $T_i$’s of $n$-Strahler number $k$. We denote the corresponding indices $(i_1,\mathrm{\dots },i_m)$ with $m⩽n$. Denoting $(j_1,\mathrm{\dots },j_n)$ the (ordinal) indices of the ${𝒰}_{n,k,d-1}$’s in ${𝒰}_{n,k,d}$, we define $\psi :i_l\mapsto j_l$, for all $l⩽m$. By recurrence, we have that $\forall l⩽m,T_{i_l}$ is isomorphically embedded in $U_{\alpha ,n,k,d-1}$ (as ). All the other $T_i$’s are such that ${𝒮}_n(T_i)⩽k-1$, and are thus isomorphically embedded in ${𝒰}_{\alpha ,n,k-1,d-1}$ by recurrence (if $k-1\ne 0$, that is. If $k-1=0$, these $T_i$ do not exist, as they would be of $n$-Strahler number $0$). Then, defining $i_0=-1$ and $i_m=\omega$ as for all $l\in [0,m]$ there is only a finite number of such ordered trees $T_i$ between the indices $i_l$ and $i_{l+1}$, we can easily map in order ${(T_i)}_{i\in [i_l,i_{l+1})}$ in the corresponding $\omega ({𝒰}_{n,k,d-1})$ with a map ${\varphi }_l$. We finally observe that the function obtained by combining $\psi$ and the different ${\varphi }_l$ is indeed injective, increasing, and that it maps $T_i$’s to ordered trees in which they are isomorphically embedded, and thus describes an isomorphic embedding of $T$ in ${𝒰}_{n,k,d}$. $◀$