The interplay between parity games and universal trees

The theorem was state here is the key technical point of a joint work with Thomas Colcombet, about universal trees (see this post). It has been published in a journal paper about universal graphs, proving in particular that separating automata (see the corresponding post) have at least quasipolynomial size.

This is an elaboration of the classical result about signature assignments or progress measures being witnesses of positional winning strategies in parity games (see e.g. the small progress measure treatment). The novelty here is to phrase this theorem using universal trees.

Theorem:
Let G be a graph and T a universal tree. The following statements are equivalent:
* G satisfies parity,
* there exists a tree t and a progress measure \phi : G \to t,
* there exists a progress measure \psi : G \to T.

This result is the main ingredient for the value iteration algorithm (see the corresponding post), and also for proving a quasipolynomial lower bound on the size of separating automata (see this post). We refer to this technical report for full details.

Missing definitions

We let \text{Parity} \subseteq [0,d-1]^\omega denote the set of infinite words such that the maximal priority appearing infinitely often is even. A path is a sequence of triples (v,i,v’) in E such that the third component of a triple in the sequence matches the first component of the next triple. (As a special case we also have empty paths consisting of only one vertex.) For a path \rho we write \pi(\rho) for its projection over the priorities, meaning the induced sequence of priorities.

We say that a graph satisfies parity if all paths in the graph satisfy the parity objective. Note that this is equivalent to asking whether all cycles are even, meaning the maximal priority appearing in the cycle is even.

We assume the reader knows about universal trees (see this post). The point of trees is to induce a family of nested orders that we define now. We label the levels of a tree by priorities from bottom to top. More precisely, even priorities sit on levels corresponding to nodes, and odd priorities inbetween levels, as illustrated below.

Let T be a tree. We define the relations \vartriangleleft_p for each p \in [0,d-1]
* for p even and \ell,\ell’ two leaves, we have \ell \vartriangleleft_p \ell’ if the ancestor at level p of \ell is to the left of or equal to the (node) ancestor at the same level of \ell’,
* for p odd and \ell,\ell’ two vertices, we have \ell \vartriangleleft_p \ell’ if \ell \vartriangleleft_{p-1} \ell’ and not \ell’ \vartriangleleft_{p-1} \ell.

Equivalently, for p odd we have \ell \vartriangleleft_p \ell’ if and only if the (edge) ancestor at level p of v is strictly to the left of the (edge) ancestor at the same level of v’.

Definition:
Consider a graph G with n vertices and priorities in [0,d-1]. A progress measure for G over a tree t is a function \mu : V \to t mapping vertices to leaves of t such that
for (v,p,v’) \in E, we have \mu(v) \vartriangleleft_p \mu(v’).

Proof of the theorem

The implication 1 \implies 2 works by induction over d, building the tree t. We refer to the journal paper for full details: the proof is about one page long.

The implication 2 \implies 3 is by definition of universal trees: indeed, since T is universal t maps into T, which yields a progress measure over T.

The implication 3 \implies 1 is given by the following lemma.

Lemma:
Let G be a graph such that there exists a tree t and a progress measure \phi : G \to t,
then G satisfies parity.

Proof:
We consider a loop in G.

(v_1, p_1, v_2) (v_2, p_2, v_3) \cdots (v_k, p_k, v_1)

Let us assume towards contradiction that its maximal priority is odd and without loss of generality it is p_1. Applying the progres measure \phi we have

\phi(v_1) \triangleleft_{p_1} \phi(v_2) \triangleleft_{p_2} \ldots \triangleleft_{p_k} \phi(v_1)

We obtain that \phi(v_1) \triangleleft_{p_1} \phi(v_1), which contradicts that for p odd \triangleleft_{p} is non-reflexive.