Universal Graphs and Good for Games Automata: New Tools for Infinite Duration Games

Let  be a set (of colors). A \(C\)-arena \(A\) is a \(C\)-graph in which vertices are split into \(V=V_\mathrm{E}\uplus V_\mathrm{A}\). The vertices are called positions. The positions in \(V_\mathrm{E}\) are the positions owned by the existential player, and the ones in \(V_\mathrm{A}\) are owned by the universal player. The root is the initial position. The edges are called moves. Infinite paths starting in the initial position are called plays. Finite paths starting in the initial position are called partial plays. The dual of an arena is obtained by swapping \(V_\mathrm{A}\) and \(V_\mathrm{E}\), i.e., exchanging the ownernship of the positions.

A \(\mathbb W\)-game  consists of a \(C\)-arena \(A\) together with a set called the winning condition.

For simplicity, we assume in this paper the following epsilon property¹: there is a special color  such that for all words \(u,v\in C^\omega \), if \(u\) and \(v\) are equal after removing all the \(\varepsilon \)-letters, then \(u\in \mathbb W\) if and only if \(v\in \mathbb W\).

The dual of a game is obtained by dualising the arena, and complementing the winning condition.

We define the following classical winning conditions:    

A strategy s for the existential player \(s_\mathrm{E}\) is a set of partial plays of the game that has the following properties:

A play is compatible with the strategy \(s_\mathrm{E}\) if all its finite prefixes belong to \(s\). A play is winning if it belongs to the winning condition \(\mathbb W\). A game is won by the existential player if there exists a strategy for the existential player such that all plays compatible with it are won by the existential player. Such a strategy is called a winning strategy.

Symmetrically, a (winning) strategy for the universal player is a (winning) strategy for the existential player in the dual game. A game is won by the universal player if there exists a strategy for the universal player such that all infinite plays compatible with it are won by the universal player.

It is not possible that in a strategy defined in this way one reaches an existential position that would have no successor: indeed, 2. would not hold.

There are different ways to define a strategy in the literature. One is as a strategy tree: indeed one can see \(s_\mathrm{E}\) as a set of nodes equipped with prefix ordering as the ancestor relation. Another way is to define a strategy as a partial map from paths to moves. All these definitions are equivalent. The literature also considers randomized strategies (in which the next move is chosen following a probability distribution): this is essential when the games are concurrent or with partial information, but not in the situation we consider in this paper.

There exist winning conditions that are not determined (and it requires the axiom of choice to prove it).

(Martin’s theorem of Borel determinacy [Mar75]). Games with Borel winning conditions are determined.

Given a \(C\)-arena \(A\), an existential player strategy graph \(S_\mathrm{E},\gamma \) in \(A\) is a trimmed \(C\)-graph \(S_\mathrm{E}\) together with a graph morphism \(\gamma \) from \(S_\mathrm{E}\) to \(A\) such that for all vertices \(x\) in \(S_\mathrm{E}\),

The existential player strategy graph \(S_\mathrm{E},\gamma \) is memoryless if \(\gamma \) is injective. In general the memory of the strategy is the maximal cardinality of \(\gamma ^{-1}(v)\) for v ranging over all positions in the arena. For  a \(\mathbb W\)-game with \(\mathbb W\subseteq C^\omega \), an existential player strategy graph \(S_\mathrm{E}\) is winning if the labels of all its paths issued from the root belong to \(\mathbb W\).

The (winning) universal player strategy graphs are defined as the (winning) existential player strategy graphs in the dual game.

The winning condition \(\mathbb W\) is memoryless for the existential player if, whenever the existential player wins in a \(\mathbb W\)-game, there is a memoryless winning existential player strategy graph. It is memoryless for the existential player over finite arenas if this holds for finite \(\mathbb W\)-games only. The dual notion is the one of memoryless for the universal player winning condition.

There exists a winning existential player strategy graph if and only if there exists a winning strategy for the existential player.

A strategy for the existential player \(s_\mathrm{E}\) can be seen as a \(C\)-graph (in fact a tree) \(S_\mathrm{E}\) of vertices \(s_\mathrm{E}\), of root \(\varepsilon \), and with edges of the form \((\pi ,a,\pi a)\) for all \(\pi a\in s_\mathrm{E}\). If the strategy \(s_\mathrm{E}\) is winning, then the strategy graph \(S_\mathrm{E}\) is also winning. Conversely, given an existential player strategy graph \(S_\mathrm{E}\), the set \(s_\mathrm{E}\) of its paths starting from the root is itself a strategy for the existential player. Again, the winning property is preserved.□

([EJ91]). The parity condition is memoryless for the existential player and for the universal player.

([EM79, GKK88]). The mean-payoff condition is memoryless for the existential player over finite arenas as well as for the universal player.

([GH82]). The Rabin condition is memoryless for the existential player, but not in general for the universal player.

([McN93]). Muller conditions are finite-memory for both players.

([CFH14]). Topologically closed conditions for which the residuals are totally ordered by inclusion are memoryless for the existential player.

(automata over infinite words). Let  . A (non-deterministic) \(\mathbb W\)-automaton \(\mathcal {A}\) over the alphabet \(A\) is a \((C\times A)\)-graph. The convention is to call states its vertices, and transitions its edges. The root vertex is called the initial state. The set \(\mathbb W\) is called the accepting condition (whereas it is the winning condition for games). The automaton is obtained from \(\mathcal {A}\) by setting the state \(p\) to be initial.

A run of the automaton \(\mathcal {A}\) over \(u\in A^\omega \) is an infinite path in \(\mathcal {A}\) that starts in the initial state and projects on its \(A\)-component to \(u\). A run is accepting if it projects on its \(C\)-component to a word \(v\in \mathbb W\). The language accepted by \(\mathcal {A}\) is the set  of infinite words \(u\in A^\omega \) such that there exists an accepting run of \(\mathcal {A}\) on u.

An automaton is deterministic (resp. complete) if for all states p and all letters \(a\in A\), there exists at most one (resp. at least one) transition of the form (p, (a, c), q). If the winning condition is parity, this is a parity automaton. If the winning condition is safety, this is a safety automaton, and we do not mention the \(C\)-component since there is only one color. I.e., the transitions form a subset of \(Q\times A\times Q\), and the notion coincides with the one of a \(A\)-graph. For this reason, we may refer to the language \(\mathcal {L}(H)\) accepted by an \(A\)-graph \(H\): this is the set of labelling words of infinite paths starting in the root vertex of \(H\).

Let  be an arena over colors , with positions  and moves  . Let also  be a \(\mathbb W\)-automaton over the alphabet \(C\) with states and transitions  . We construct the product arena as follows:

Note that every game move \(((x,p),\varepsilon ,((x,c,y),p))\) of \(\mathcal {G}\times \mathcal {A}\) can be transformed into a move \((x,c,y)\) of \(\mathcal {G}\), called its game projection. Similarly every automaton move \((((x,c,y),p),d,(y,q))\) can be turned into a transition \((p,(c,d),q)\) of the automaton \(\mathcal {A}\) called its automaton projection. Hence, every play \(\pi \) of the product game can be projected into the pair of a play \(\pi ^\prime \) in \(\mathcal {G}\) of label \(u\) (called the game projection), and an infinite run \(\rho \) of the automaton over \(u\) (called the automaton projection). The product game is the game over the product arena, using the winning condition of the automaton.

(folklore³). Let  be a \(\mathbb V\)-game, and  be a \(\mathbb W\)-automaton that accepts a language  , then if the existential player wins \(\mathcal {G}\times Q_{\mathcal A}\), she wins \(\mathcal {G}\).

Assume that the existential player wins the game \(\mathcal {G}\times \mathcal {A}\) using a strategy \(s_\mathrm{E}\). This strategy can be turned into a strategy for the existential player \(s^\prime _\mathrm{E}\) in \(\mathcal {G}\) by performing a game projection. It is routine to check that this is a valid strategy.

Let us show that this strategy \(s^\prime _\mathrm{E}\) is \(\mathbb V\)-winning, and hence conclude that the existential player wins the game \(\mathcal {G}\). Indeed, let \(\pi ^\prime \) be a play compatible with \(s^\prime _\mathrm{E}\), say labelled by \(u\). This play \(\pi ^\prime \) has been obtained by game projection of a play \(\pi \) compatible with \(s_\mathrm{E}\) in \(\mathcal {G}\times \mathcal {A}\). The automaton projection \(\rho \) of \(\pi \) is a run of \(\mathcal {A}\) over \(u\), and is accepting since \(s_\mathrm{E}\) is a winning strategy. Hence, \(u\) is accepted by \(\mathcal {A}\) and as a consequence belongs to \(\mathbb V\). We have proved that \(s_\mathrm{E}\) is winning.□

Let  be a \(\mathbb V\)-game, and be a deterministic \(\mathbb W\)-automaton that accepts the language \(\mathbb V\), then the games \(\mathcal {G}\) and \(\mathcal {G}\times \mathcal {A}\) have the same winner.

We assume without loss of generality that \(\mathcal {A}\) is deterministic and complete (note that this may require to slightly change the accepting condition, for instance in the case of safety). The results then follows from the application of Lemma 3 to the game \(\mathcal {G}\) and its dual.□

(good for games automata [HP06]). Let  be a language, and  be a \(\mathbb W\)-automaton. Then \(\mathcal {A}\) is good for \(\mathbb V\)-games if for all \(\mathbb V\)-games \(\mathcal {G}\), \(\mathcal {G}\) and \(\mathcal {G}\times \mathcal {A}\) have the same winner.

It may seem strange, a priori, not to require in the definition that \(\mathcal {L}(\mathcal {A})=\mathbb V\). In fact, it holds anyway: if an automaton is good for \(\mathbb V\)-games, then it accepts the language \(\mathbb V\). Indeed, let us assume that there exists a word \(u\in \mathcal {L}(\mathcal {A})\setminus \mathbb V\), then one can construct a game that has exactly one play, labelled \(u\). This game is won by the universal player since \(u\not \in \mathbb V\), but the existential player wins \(\mathcal {G}\times \mathcal {A}\). A contradiction. The same argument works if there is a word in \(\mathbb V\setminus \mathcal {L}(\mathcal {A})\).

We construct an automaton which is not good for games. The alphabet is \(\{a,b\}\). The automaton is a Büchi automaton: it has an initial state from which goes two \(\epsilon \)-transitions: the first transition guesses that the word contains infinitely many a’s, and the second transition guesses that the word contains infinitely many b’s. Note that any infinite word contains either infinitely many a’s or infinitely many b’s, so the language recognised by this automaton is the set of all words. However, this automaton requires a choice to be made at the very first step about which of the two alternatives hold. This makes it not good for games: indeed, consider a game  where the universal player picks any infinite word, letter by letter, and the winning condition is \(\mathbb V\). It has only one position owned by the universal player. The existential player wins \(\mathcal {G}\) because all plays are winning. However, the existential player loses \(\mathcal {G}\times \mathcal {A}\), because in this game she has to declare at the first step whether there will be infinitely many a’s or infinitely many b’s, which the universal player can later contradict.

(composition of good for games automata). Let  be a good for games \(\mathbb W\)-automaton for the language  , and  be good for games \(\mathbb V\)-automaton for the language \(L\), then the composed automaton \(\mathcal {A}\circ \mathcal {B}\) is a good for games \(\mathbb W\)-automaton for the language \(L\).

Let  be a language, and  be a \(\mathbb W\)-automaton. Then \(\mathcal {A}\) is good for \((\mathbb V,n)\)-games if for all \(\mathbb V\)-games \(\mathcal {G}\) with at most \(n\) positions, \(\mathcal {G}\) and \(\mathcal {G}\times \mathcal {A}\) have the same winner (we also write good for small games when there is no need for \(\mathbb V\) and \(n\) to be explicit).

It is strongly good for \((\mathbb V,n)\)-games if it is good for \((\mathbb V,n)\)-games and the language accepted by \(\mathcal {A}\) is contained in \(\mathbb V\).

(automata that are good for small games). We have naturally the following chain of implications:The first implication is from Remark 3, and the second is by definition. Thus the first examples of automata that are strongly good for small games are the automata that are good for games.

We consider the case of the coBüchi condition: recall that the set of colors is \(\{0,1\}\) and the winning plays are the ones such that there ultimately contain only 0’s. It can be shown that if the existential player wins in a coBüchi game with has at most \(n\) positions, then she also wins for the winning condition \(L=(0^*(\varepsilon +1))^{n} 0^\omega \), i.e., the words in which there is at most \(n\) occurrences of 1 (indeed, a winning memoryless strategy for the condition \(\mathtt {coBuchi}\) cannot contain a 1 in a cycle, and hence cannot contain more than \(n\) occurrences of 1 in the same play; thus the same strategy is also winning in the same game with the new winning condition \(L\)). As a consequence, a deterministic safety automaton that accepts the language \(L\subseteq \mathtt {coBuchi}\) (the minimal one has \(n+1\) states) is good for \((\mathtt {coBuchi},n)\)-games.

(composition of good for small games automata). Let  be a good for \(n\)-games \(\mathbb V\)-automaton for the language \(L\) with \(k\) states, and be a good for \(kn\)-games \(\mathbb W\)-automaton for the language  , then the composed automaton \(\mathcal {A}\circ \mathcal {B}\) is a good for n-games \(\mathbb W\)-automaton for the language \(L\).

Assume that there exists an algorithm for solving \(\mathbb W\)-games of size \(\lim \) in time \(f(m)\). Let be a \(\mathbb V\)-game with at most \(n\) positions and be a good for \((\mathbb V,n)\)-games \(\mathbb W\)-automaton of size \(k\), there exists an algorithm for solving \(\mathcal {G}\) of complexity \(f(kn)\).

Construct the game \(\mathcal {G}\times \mathcal {A}\), and solve it.□

([Leh18, BL19]).Given positive integers \(n,d\), there exists a parity automaton with \(n^{(\log d+ O(1))}\) states and \(1 + \lfloor \log n\rfloor \) priorities which is strongly good for \(n\)-games.

Let  be a winning condition which is memoryless for the existential player, then the following quantities coincide for all positive integers \(n\):

An automaton  is strongly \((\mathbb W, n)\)-separating ifin which is the union of all the languages accepted by safety automata with \(n\) states that accept sublanguages of \(\mathbb W\).⁵

In the statement of Theorem 9, (1) \(\Longrightarrow \) (2) \(\Longrightarrow \) (3).

Assume (1), i.e., there exists a strongly \((\mathbb W,n)\)-separating deterministic safety automaton  , then \(\mathcal {L}(\mathcal {A})\subseteq \mathbb W\). Let  be a \(\mathbb W\)-game with at most \(n\) positions. By Lemma 3, if the existential player wins \(\mathcal {G}\times \mathcal {A}\), she wins the game \(\mathcal {G}\). Conversely, assume that the existential player wins \(\mathcal {G}\), then, by assumption she has a winning memoryless strategy graph \(S_\mathrm{E},\gamma :S_\mathrm{E}\rightarrow \mathcal {G}\), i.e., \(\mathcal {L}(S_\mathrm{E})\subseteq \mathbb W\) and \(\gamma \) is injective. By injectivity of \(\gamma \), \(S_\mathrm{E}\) has at most \(n\) vertices and hence \(\mathcal {L}(S_\mathrm{E})\subseteq \mathbb W|_n\subseteq \mathcal {L}(\mathcal {A})\). As a consequence, for every (partial) play \(\pi \) compatible with \(S_\mathrm{E}\), there exists a (partial) run of \(\mathcal {A}\) over the labels of \(\pi \) (call this property ). We construct a new strategy for the existential player in \(\mathcal {G}\times \mathcal {A}\) as follows: When the token is in a game position, the existential player plays as in \(S_\mathrm{E}\); When the token is in an automaton position, the existential player plays the only available move (indeed, the move exists by property  , and is unique by the determinism assumption). Since this is a safety game, the new strategy is winning. Hence the existential player wins \(\mathcal {G}\times \mathcal {A}\), proving that \(\mathcal {A}\) is good for \((\mathbb W, n)\)-games. Item 2 is established.

Assume now (2), i.e., that  is some strongly good for \((\mathbb W, n)\)-games automaton. Then by definition \(\mathcal {L}(\mathcal {A})\subseteq \mathbb W\). Now consider some word \(u\) in \(\mathbb W|_n\). By definition, there exists some safety automaton  with at most \(n\) states such that \(u\in \mathcal {L}(\mathcal {B})\subseteq \mathbb W\). This automaton can be seen as a \(\mathbb W\)-game  in which all positions are owned by the universal player. Since \(\mathcal {L}(\mathcal {B})\subseteq \mathbb W\), the existential player wins the game \(\mathcal {G}\). Since furthermore \(\mathcal {A}\) is good for \((\mathbb W, n)\)-games, the existential player has a winning strategy \(S_\mathrm{E}\) in \(\mathcal {G}\times \mathcal {A}\). Assume now that the universal player is playing the letters of \(u\) in the game \(\mathcal {G}\times \mathcal {A}\), then the winning strategy \(S_\mathrm{E}\) constructs an accepting run of \(\mathcal {A}\) on \(u\). Thus \(u\in \mathcal {L}(\mathcal {A})\), and Item 3 is established.□

Given a winning condition  and a positive integer \(n\), a \(C\)-graph \(U\) is \((\mathbb W, n)\)-universal⁶ if

In the statement of Theorem 9, (4) \(\Longrightarrow \) (1)

Assume that there is a \((\mathbb W,n)\)-universal graph \(U\). We show that \(U\) seen as an safety automaton is strongly good for \((\mathbb W, n)\)-games. One part is straightforward: \(\mathcal {L}(U)\subseteq \mathbb W\) is by assumption. For the other part, consider a \(\mathbb W\)-game  with at most \(n\) positions. Assume that the existential player wins \(\mathcal {G}\), this means that there exists a winning memoryless strategy for the existential player \(S_\mathrm{E},\gamma :S_\mathrm{E}\rightarrow \mathcal {G}\) in \(\mathcal {G}\). We then construct a strategy for the existential player \(S^\prime _\mathrm{E}\) that maintains the property that the only game positions in \(\mathcal {G}\times U\) that are met in \(S^\prime _\mathrm{E}\) are of the form \((x,\gamma (x))\). This is done as follows: when a game position is encountered, the existential player plays like the strategy \(S_\mathrm{E}\), and when an automaton position is encountered, the existential player plays in order to follow \(\gamma \). This is possible since \(\gamma \) is a weak graph morphism.□

A \(C\)-graph \(H\) is \(\mathbb W\)-maximal if \(\mathcal {L}(H)\subseteq \mathbb W\) and if it is not possible to add a single edge to it without breaking this property, i.e., without producing an infinite path from the root vertex that does not belong to \(\mathbb W\).

For a winning condition  which is memoryless for the existential player, and \(H\) a \(\mathbb W\)-maximal graph, then the \(\varepsilon \)-edges in \(H\) form a transitive and total relation.

Transitivity arises from the epsilon property of winning conditions (Definition 1): Consider three vertices \(x\), \(y\) and \(z\) such that \(\alpha =(x,\varepsilon ,y)\) and \(\beta =(y,\varepsilon ,z)\) are edges of \(H\). Let us add a new edge \(\delta =(x,\varepsilon ,y)\) yielding a new graph \(H^\prime \). Let us consider now any infinite path \(\pi \) in \(H^\prime \) starting in the root (this path may contain finitely of infinitely many occurrences of \(\delta \), but not almost only \(\delta \)’s since \(x\ne y\)). Let \(\pi ^\prime \) be obtained from \(\pi \) by replacing each occurrence of \(\delta \) by the sequence \(\alpha \beta \). The resulting path \(\pi ^\prime \) belongs \(H\), and thus its labelling belongs to \(\mathbb W\). But since the labelings of \(\pi \) and \(\pi ^\prime \) agree after removing all the occurrences of \(\varepsilon \), the epsilon property guarantees that the labelling of \(\pi \) belongs to \(\mathbb W\). Since this holds for all choices of \(\pi \), we obtain \(\mathcal {L}(H^\prime )\subseteq \mathbb W\). Hence, by maximality, \(\delta \in H\), which means that the \(\varepsilon \)-edges form a transitive relation.

Let us prove the totality. Let \(x\) and \(y\) be distinct vertices of \(H\). We have to show that either  or  . We can turn \(H\) into a game  as follows:

We claim first that the game \(\mathcal {G}\) is won by the existential player. Let us construct a strategy \(s_\mathrm{E}\) in \(\mathcal {G}\) as follows. The only moment the existential player has a choice to make is when the play reaches the position \(z\). This has to happen after a move of the form \((t,a,z)\). This move originates either from an edge of the form \((t,a,x)\), or from an edge of the form \((t,a,y)\). In the first case the strategy \(s_\mathrm{E}\) chooses the move \((z,\varepsilon ,x)\), and in the second case the move \((z,\varepsilon ,y)\). Let us consider a play \(\pi \) compatible with \(s_\mathrm{E}\), and let \(\pi ^\prime \) be obtained from \(\pi \) by replacing each occurrence of \((t,a,z)(z,\varepsilon ,x)\) with \((t,a,x)\) and each occurrence of \((t,a,z)(z,\varepsilon ,y)\) with \((t,a,y)\). The resulting \(\pi ^\prime \) is a path in \(H\) and hence its labeling belongs to \(\mathbb W\). Since the labelings of \(\pi \) and \(\pi ^\prime \) are equivalent up to \(\varepsilon \)-letters, by the epsilon property, the labeling of \(\pi \) also belongs to \(\mathbb W\). Hence the strategy \(s_\mathrm{E}\) witnesses the victory of the existential player in \(\mathcal {G}\). The claim is proved.

By assumption on \(\mathbb W\), this means that there exists a winning memoryless strategy for the existential player \(S_\mathrm{E}\) in \(\mathcal {G}\). In this strategy, either the existential player always chooses \((z,\varepsilon ,x)\), or she always chooses \((z,\varepsilon ,y)\). Up to symmetry, we can assume the first case. Let now \(H^\prime \) be the graph \(H\) to which a new edge \(\delta =(y,\varepsilon ,x)\) has been added. We aim that \(\mathcal {L}(H^\prime )\subseteq \mathbb W\). Let \(\pi \) be an infinite path in \(H^\prime \) starting from the root vertex. In this path, each occurrences of \(\delta \) are preceded by an edge of the form \((t,a,y)\). Thus, let \(\pi ^\prime \) be obtained from \(\pi \) by replacing each occurrence of a sequence of the form \((t,a,y)\delta \) by \((t,a,y)\). The resulting path is a play compatible with \(S_\mathrm{E}\). Hence the labeling of \(\pi ^\prime \) belongs to \(\mathbb W\), and as a consequence, by the epsilon property, this is also the case for \(\pi \). Since this holds for all choices of \(\pi \), we obtain that \(\mathcal {L}(H^\prime )\subseteq \mathbb W\). Hence, by \(\mathbb W\)-maximality assumption, \((y,\varepsilon ,x)\) is an edge of \(H\).

Overall, the \(\varepsilon \)-edges form a total transitive relation.□

For a winning condition  which is memoryless for the existential player, and \(H\) a \(\mathbb W\)-maximal graph, then the following properties hold:

The first part is obvious from Lemma 9. For the second part, it is sufficient to prove that implies and that implies . Both cases are are similar to the proof of transitivity in Lemma 9⁷. The two next items are almost the same. The difficult direction is to assume the language inclusion, and deduce the existence of an edge (left to right). Let us assume for an instant that \(H\) would be a finite word automaton, with all its states accepting. Then it is an obvious induction to show that if (as languages of finite words), it is safe to add an \(\varepsilon \)-transitions from \(q\) to \(p\) without changing the language. The two above items are then obtained by limit passing (this is possible because the safety condition is topologically closed).□

In the statement of Theorem 9, (3) \(\Longrightarrow \) (4).

Let us start from a strongly \((\mathbb W,n)\)-separating safety automaton  . Without loss of generality, we can assume it is \(\mathbb W\)-maximal. We claim that it is \((\mathbb W,n)\)-universal.

Let us define first for all languages \(K\subseteq C^\omega \), its closure(in case of an empty intersection, we assume \(C^\omega \)). This is a closure operator: \(K\subseteq K'\) implies \(\overline{K}\subseteq \overline{K'}\), \(K\subseteq \overline{K}\), and \(\overline{\overline{K}}=\overline{K}\). Futhermore, \(a\overline{K}\subseteq \overline{aK}\), for all letters \(a\in C\). Let now \(H\) be a trimmed graph with at most \(n\) vertices such that \(\mathcal {L}(H)\subseteq \mathbb W\). We have \(\mathcal {L}(H)\subseteq \mathbb W|_n\) by definition of \(\mathbb W|_n\).

We claim that for each vertex \(x\) of \(H\), there is a state \(\alpha (x)\) of \(\mathcal {A}\) such thatIndeed, note first that, since \(H\) is trimmed, there exists some word \(u\) such that . Hence, using the fact that \(\mathcal {A}\) is strongly \((\mathbb W,n)\)-separating, we get that for all  , \(uv\in \mathcal {L}(H)\subseteq \mathbb W|_n\subseteq \mathcal {L}(\mathcal {A})\). Let \(\beta (v)\) be the state assumed after reading \(u\) by a run of \(\mathcal {A}\) accepting \(uv\). It is such that  . Since \(\mathcal {A}\) is finite and its states are totally ordered under inclusion of residuals (Lemma 10), this means that there exists a state \(\alpha (x)\) (namely the maximum over all the \(\beta (w)\) for  ) such that  .

Let us show that \(\alpha \) is a weak graph morphism⁸ from \(H\) to \(\mathcal {A}\). Consider some edge \((x,a,y)\) of \(H\). We have  . Hencewhich implies by Lemma 10 that . Let now  be some edge. By hypothesis, we haveThus . We obtain  by Lemma 10. Hence, \(\alpha \) is a weak graph morphism.

Since this holds for all choices of \(H\), we have proved that \(\mathcal {A}\) is a \((\mathbb W,n)\)-universal graph.□

In the statement of Theorem 9, (3) \(\Longrightarrow \) (1).

Let us start from a strongly \((\mathbb W,n)\)-separating safety automaton  . Without loss of generality, we can assume it is maximal. Thus Lemma 10 holds.

We now construct a deterministic safety automaton  .

We have to show that this deterministic safety automaton is strongly \((\mathbb W,n)\)-separating. Note first that by definition \(\mathcal {D}\) is obtained from \(\mathcal {A}\) by removing transitions. Hence \(\mathcal {L}(\mathcal {D})\subseteq \mathcal {L}(\mathcal {A})\subseteq \mathbb W\). Consider now some \(u\in \mathbb W|_n\). By assumption, \(u\in \mathcal {L}(\mathcal {A})\). Let \(\rho = (p_0,u_1,p_1)(p_1,u_2,p_2)\cdots \) be the corresponding accepting run of \(\mathcal {A}\). We construct by induction a (the) run of \(\mathcal {D}\) \((q_0,u_1,q_1)(q_1,u_2,q_2)\cdots \) in such a way that \(q_i\leqslant _{\varepsilon }p_i\). For the initial state, \(p_0=q_0\). Assume the run up to \(q_i\leqslant _{\varepsilon }p_i\) has been constructed. By Lemma 10, \((q_i,u_{i+1},p_{i+1})\) is a transition of \(\mathcal {A}\). Hence the least \(r\) such that \((q_i,u_{i+1},r)\) is a transition of \(\mathcal {A}\) does exist, and is \(\leqslant _{\varepsilon }p_{i+1}\). Let us call it \(q_{i+1}\); we indeed have that \((q_i,u_{i+1},q_{i+1})\) is a transition of \(\mathcal {D}\). Hence, \(u\) is accepted by \(\mathcal {D}\). Thus \(\mathbb W|_n\subseteq \mathcal {L}(\mathcal {D})\).

Overall \(\mathcal {D}\) is a strongly \((\mathbb W,n)\)-separating deterministic safety automaton that has at most as many states as \(\mathcal {A}\).□

For a \([i,j]\)-graph \(H\) that has all its vertices reachable from the root, the following properties are equivalent:

Clearly, since all vertices are reachable, \(\mathcal {L}(H)\subseteq \mathbb W\) implies that all the cycles are even. Also, if all cycles are even, then all elementary cycles also are. Finally assume that all the elementary cycles are even. Then we can consider \(H\) as a game, in which every positions is owned by the universal player. Assume that some infinite path from the root would not satisfy \(\mathtt {Parity}_{[i,j]}\), then this path would be a winning strategy for the universal player in this game. Since \(\mathtt {Parity}_{[i,j]}\) is a winning condition memoryless for the universal player, this means that the universal player has a winning memoryless strategy. But this winning memoryless strategy is nothing but a lasso, and thus contains an elementary cycle of maximal odd priority.□

A \(d\)-tree \(t\) is a balanced, unranked, ordered tree of height \(d\) (the root does not count: all branches contain exactly \(d+1\) nodes). The order between nodes of same level is denoted  . Given a leaf \(x\), and \(i=0\ldots i\), we denote the ancestor at depth \(i\) of \(x\) (0 is the root, \(d\) is \(x\)).

The \(d\)-tree \(t\) is \(n\)-universal if for all \(d\)-trees \(s\) with at most \(n\) nodes, there is a \(d\)-tree embedding of \(s\) into \(t\), in which a \(d\)-tree embedding is an injective mapping from nodes of \(s\) to nodes of \(t\) that preserves the height of nodes, the ancestor relation, and the order of nodes. Said differently, \(s\) is obtained from \(t\) by pruning some subtrees (while keeping the structure of a \(d\)-tree).

Given a \(d\)-tree \(t\), is a \([0,2d]\)-graph with the following characteristics:

For all \(d\)-trees \(t\), \(\mathcal {L}(\mathtt {Graph}(t))\subseteq \mathtt {Parity}_{[0,2d]}\).

Using Lemma 13, it is sufficient to prove that all cycle in \(\mathtt {Graph}(t)\) are even. Thus, let us consider a cycle \(\rho \). Assume that the highest priority occurring in \(\alpha \) is \(2(d-i)+1\). Note then that for all edges \(\alpha =(x,k,y)\) occurring in \(\rho \):

As a consequence, the first and last vertex of \(\alpha \) cannot have the same ancestor at level \(i\), and thus are different.□

([CF18]). For all positive integers \(d,n\), the two following quantities are equal:

We shall see below (Definition 14) a construction \(\mathtt {Tree}\) that maps all \(\mathtt {Parity}_{[0,2d]}\)-maximal graphs \(G\) to a \(d\)-tree \(\mathtt {Tree}(G)\) of smaller or same size. Corollary 4 establishes that this construction is in some sense the converse of \(\mathtt {Tree}\) (in fact they form an adjunction). and that this correspondence preserves the notions of universality. This proves the above result: Given a \(n\)-universal \(d\)-tree \(t\), then, by Corollary 4, \(\mathtt {Graph}(t)\) is a \((\mathtt {Parity}_{[0,2d]},n)\)-universal graph that has as many vertices as leaves of graphs. Conversely, consider a \((\mathtt {Parity}_{[0,2d]},n)\)-universal graph \(G\). One can add to it edges until it becomes a \(\mathtt {Parity}_{[0,2d]}\)-maximal graph \(G^\prime \) with as many vertices. Then, by Corollary 4, \(\mathtt {Tree}(G^\prime )\) is an \(n\)-universal \(d\)-tree that has as much or less leaves than vertices of \(G^\prime \).□

The complete \(d\)-tree \(t\) of degree \(n\) (that has \(n^{d}\) leaves) is \(n\)-universal. The \([0,2d]\)-graph \(\mathtt {Graph}(t)\) obtained in this way is used in the small progress measure algorithm [Jur00].

([Fij18, CDF+19]). Given positive integers \(n,d\),

The complexity of solving \(\mathtt {Parity}_{[0,d]}\)-games with at most \(n\)-vertices isand no algorithm based on good for small safety games can be faster than quasipolynomial time.

We shall now analyse in detail the shape of \(\mathtt {Parity}_{[0,2d]}\)-maximal graphs. This analysis culminates with the precise description of such graphs in Lemma 19, that essentially establishes a bijection with graphs of the form \(\mathtt {Graph}(t)\) (Corollary 4).

Let us note that, since the parity condition is memoryless for the existential player, using Lemma 10, and the fact that the parity condition is unchanged by modifying finite prefixes, we can always assume that the root vertex is the minimal one for the \(\leqslant _{\varepsilon }\) ordering. Thus, from now, we do not have to pay attention to the root, in particular in weak graph morphisms. Thus, from now, we just mention the term morphism for weak graph morphisms.

Let us recall preference ordering \(\sqsubseteq\) between the non-negative integers is defined as follows:

Let \(k\sqsubseteq \ell \) and \(u,v\) sequences of priorities. If the maximal priority occurring in \(ukv\) is even, then the maximal priority occurring in \(u\ell v\) is also even.

Let \(G\) be a \(\mathtt {Parity}_{[0,2d]}\)-maximal graph and \(k\sqsubseteq \ell \) be priorities in \([0,2d]\). For all vertices \(x,y\) of \(G\), implies .

Let us add \((x,\ell ,y)\) to \(G\). Let \(u(x,\ell ,y)v\) be some elementary cycle of the new graph involving the new edge \((x,\ell ,y)\). By Lemma 13, \(u(x,k,y)v\) is an even cycle in the original graph. Hence, by Fact 1, \(u(x,\ell ,y)v\) is also an even cycle. Thus, by Lemma 13, \(G\) with the newly added edge also satisfies \(\mathcal {L}(G)\subseteq \mathtt {Parity}_{[0,2d]}\). Using the maximality assumption for \(G\), we obtain that \((x,\ell ,y)\) was already present in \(G\).□

Let \(G\) be a \(\mathtt {Parity}_{[0,2d]}\)-maximal graph. For all vertices \(x,y,z\) of \(G\), if and , then .

Let us add \((x,\max (k,\ell ),z)\) to \(G\). Let \(u(x,\max (k,\ell ),z)v\) be an elementary cycle in the new graph. By Lemma 13, \(u(x,k,y)(y,\ell ,z)v\), being a cycle of \(G\), has to be even. Since, furthermore, the maximal priority that occurs in \(u(x,k,y)(y,\ell ,z)v\) is the same as the maximal one in \(u(x,\max (k,\ell ),z)v\), the cycle \(u(x,\max (k,\ell ),z)v\) is also even. Using the maximality assumption of \(G\), we obtain that \((x,\max (k,\ell ),z)\) was already present in \(G\).□

Let \(G\) be a \(\mathtt {Parity}_{[0,2d]}\)-maximal graph, and \(x,y\) be vertices, then , and .

For  , it is sufficient to notice that adding the edge \((x,0,x)\), if it was not present, simply creates one new elementary cycle to \(G\), namely \((x,0,x)\). Since it is an even cycle, by Lemma 13, the new graph also satisfies \(\mathcal {L}(G)\subseteq \mathtt {Parity}_{[0,2d]}\). Hence, by maximality assumption, the edge was already present in \(G\) before.

Consider the graph \(G\) with an extra edge \((x,2d,y)\) added. Consider now an elementary cycle that contains \((x,2d,y)\), i.e., of the form \(u(x,2d,y)v\). Its maximal priority is \(2d\), and thus even. Hence by Lemma 13 and maximality assumption, the edge was already present in \(G\).□

Let \(G\) be a \(\mathtt {Parity}_{[0,2d]}\)-maximal graph and \(k=0,2,\ldots ,2d-2\). For all vertices \(x,y\), holds if and only if does not hold.

Assume first that and both holds. Then is an odd cycle contradicting Lemma 13.

Conversely, assume that adding the edge  would break the property \(\mathcal {L}(G)\subseteq \mathtt {Parity}_{[0,2d]}\). This means that there is an elementary cycle of the form \(u(x,k+1,y)v\) which is odd. Let \(\ell \) be the maximal priority in \(vu\). If \(\ell \geqslant k+1\), then  \(\ell \) is odd, and thus \(\ell \sqsubseteq k\), and we obtain by Lemma 15. Otherwise, \(\ell \leqslant k\), and again \(\ell \sqsubseteq k\). Once more holds by Lemma 15.□

A \([0,2d]\)-graph \(G\) is a \(\mathtt {Parity}_{[0,2d]}\)-maximal graph if and only if all the following properties hold:

First direction. Assume first that \(G\) is a \(\mathtt {Parity}_{[0,2d]}\)-maximal graph.

(1) Let \(k=0,2,\ldots ,2d\); is transitive by Lemma 16. Furthermore, by Lemma 17, for all vertices \(x\), and thus by Lemma 15, since \(0\sqsubseteq k\), . Hence is also reflexive and hence a preorder. Consider now another vertex \(y\). By Lemma 18, either  or . But by Lemma 15, implies  . Hence either  or . Thus  is a total preorder.

(2) For \(k=0,2,\ldots ,2d-2\), since \(k\sqsubseteq k+2\), by Lemma 15, .

(3) is the maximal relation by Lemma 15.

(4) For \(k=0,2,\ldots ,2d-2\) and \(x,y\), we know that holds if and only if does not. This shows .

Second direction. Assume now that \(G\) satisfies the conditions (1)-(4). Let us first show that \(\mathcal {L}(G)\subseteq \mathtt {Parity}_{[0,2d]}\). For the sake of contradiction, consider an elementary cycle that would be odd. It can be written as \(u(x,k,y)v\) with a maximal odd priority \(k\). Note first that for all \(\ell \leqslant k\): indeed, by (2), this is true if \(\ell \) is even, and by (1) and (4), for all \(j\) odd. Also  is the strict version of the preorder  . Hence, the path \(u(x,k,y)v\) has to strictly advance with respect to the preorder : it cannot be a cycle.

Assume now that an edge \((x,k,y)\) is not present in \(G\). If \(k\) is even, since \((x,k,y)\) is not present, by (4) this means that \((y,k+1,x)\) is present. Hence, adding the edge \((x,k,y)\) would create the odd cycle \((x,k,y)(y,k+1,x)\). If \(k\) is odd, since \((x,k,y)\) is not present, by (4) this means that \((y,k-1,x)\) is present. Hence, adding the edge \((x,k,y)\) would create the odd cycle \((x,k,y)(y,k-1,x)\). Hence \(G\) is \(\mathtt {Parity}_{[0,2d]}\)-maximal.□

Given a morphism \(\alpha \) from a \(\mathtt {Parity}_{[0,2d]}\)-maximal graph \(H\) to a \(\mathtt {Parity}_{[0,2d]}\)-maximal graph \(G\), then if and only if , for all vertices \(x,y\) of \(H\) and integers \(k\) in \([0,2d]\). Furthermore, if \(\alpha \) is surjective, then every map \(\beta \) from \(G\) to \(H\), such that \(\alpha \circ \beta \) is the identity on \(G\) is an injective morphism.

First part. From left to right, this is the definition of a morphism. The other direction is by (4) of Lemma 19: if  and \(k\) is odd, then does not hold by (4), thus does not hold by morphism, thus holds by (4) again. The case of \(k\) even is similar (using \(k+1\) this time).

For the second part, since \(\alpha \circ \beta \) is the identity, \(\beta \) has to be injective. It is a morphism by the first part.□

Let \(G\) be a \(\mathtt {Parity}_{[0,2d]}\)-maximal graph. The \(d\)-tree is constructed as follows:

Let \(q\) be the quotient map from vertices of \(G\) to leaves of \(\mathtt {Tree}(G)\) that maps each vertex to its -equivalence class. It has the following property for all vertices \(x,y\) of \(G\):The identity maps the vertices of \(\mathtt {Graph}(t)\) to the leaves of \(t\), and has the property that for all vertices \(x,y\):

¹⁰ For all \(\mathtt {Parity}_{[0,2d]}\)-maximal graphs \(G,H\), all \(d\)-trees \(t\), and all positive integers \(n\),

Let \(q\) be the quotient from Lemma 20. It can be seen as a surjective map from vertices of \(\mathtt {Graph}(\mathtt {Tree}(G))\) to \(G\). By Lemma 20 it is a morphism. By Corollary 3, \(\mathtt {Graph}(\mathtt {Tree}(G))\) is also an induced subgraph of \(G\).

The leaves of \(\mathtt {Tree}(\mathtt {Graph}(t))\) are the singletons consisting of leaves of \(t\). Hence, there is a bijective map from leaves of \(\mathtt {Tree}(\mathtt {Graph}(t))\) to leaves of \(t\) that sends\(\{\ell \}\) to \(\ell \). By Lemma 20, this is a morphism, and by Corollary 3 an isomorphism.

For the third item, assume first that there is a morphism from \(H\) to \(\mathtt {Graph}(t)\). By the first point, there is an injective morphism from \(\mathtt {Graph}(\mathtt {Tree}(H))\) to \(H\). By composition, we obtain a morphism from \(\mathtt {Graph}(\mathtt {Tree}(H))\) to \(\mathtt {Graph}(t)\). By Lemma 20, it is also a tree embedding from \(\mathtt {Tree}(H)\) to \(t\). Conversely, assume that there exists an embedding from \(\mathtt {Tree}(H)\) to \(t\). It can be raised by Lemma 20 to a morphism from \(\mathtt {Graph}(\mathtt {Tree}(H))\) to \(\mathtt {Graph}(t)\). By the first point, there is a morphism from \(H\) to \(\mathtt {Graph}(\mathtt {Tree}(H))\). By composition, we get a morphism from \(H\) to \(\mathtt {Graph}(t)\).

The two last items are obvious from the one just before.□