Register Games
Karoliina Lehtinen Udi Boker

=1





1626
LastPage
Feb. 28, 2019May 19, 2020

 =1


[description]leftmargin=10.95003pt



 

shapes,shapes.geometric,arrows,fit,calc,positioning,automata




countitems
nextitemizecount




AutoMultiColItemize
>32


>3



Register Games]Register Games*

*The article extends <cit.> and parts of <cit.>.
K. Lehtinen]Karoliina Lehtinen	
University of Liverpool, United Kingdom	
k.lehtinen@liverpool.ac.uk

U. Boker]Udi Boker	
Interdisciplinary Center (IDC) Herzliya, Israel	
udiboker@idc.ac.il  
Research supported by the Israel Science Foundation grant 1373/16 and the EPSRC grant EP/P020909/1
(Solving Parity Games in Theory and Practice)	








 
 
 
 
 
 
 
 
 
 
 
 
 
 


 
 
 


 





 
 

 


 
































 
 








  




 





















The complexity of parity games is a long standing open problem that saw a major breakthrough in 2017 when two quasi-polynomial algorithms were published. 

This article presents a third, independent approach to solving parity games in quasi-polynomial time, based on the notion of register game, a parameterised variant of a parity game.

The analysis of register games leads to a quasi-polynomial algorithm for parity games, a polynomial algorithm for restricted classes of parity games and a novel measure of complexity, the register index, which aims to capture the combined complexity of the priority assignement and the underlying game graph.

 We further present a translation of alternating parity word automata into alternating weak automata with only a quasi-polynomial increase in size, based on register games—this improves on the previous exponential translation. 



We also use register games to investigate the parity index hierarchy: while for words the index hierarchy of alternating parity automata collapses to the weak level, and for trees it is strict, for structures between trees and words, it collapses logarithmically, in the sense that any parity tree automaton of size n is equivalent, on these particular classes of structures, to an automaton with a number of priorities logarithmic in n.


[
    [
    December 30, 2023
=====================






§ INTRODUCTION


A play in a parity game consists of a player, whom we shall call Eve, and her opponent, Adam, moving a token along the edges of a graph labelled with integer priorities, forever, thus forming an infinite path. Eve's objective is to force the highest priority that occurs infinitely often to be even, while Adam tries to stop her.


These games arise at the intersection of logic, games, and automata theory. In particular, they are the acceptance games for alternating parity automata, both on trees and on ω-words.
The complexity of solving parity games—that is, of deciding which player has a winning strategy—still is, despite extended efforts, an open problem: it is in UP∩coUP <cit.> yet it is not known to admit a polynomial algorithm. After over twenty-five years of incremental improvements, Calude, Jain, Khoussainov, Li, and Stephan published the first quasi-polynomial solution <cit.>. Only a little later in the same year, Jurdziński and Lazić presented an independent progress-measure based algorithm that achieves the same complexity <cit.>.
This article presents a third, independent approach to solving parity games in quasi-polynomial time. The automata-theoretic method also solves the more general problem of translating alternating parity word automata into alternating weak automata with quasi-polynomial increase in state space, and offers some new insights into the descriptive complexity of parity games—that is, the complexity of formalisms that can recognise winning regions in parity games—and the parity index problem.



  §.§.§ Register Games
 Our first contribution is to present register games, a parameterised variant of parity games, that we then use to analyse the complexity of parity games and parity automata, both on infinite words and infinite trees.
A register game consists of a normal parity game, augmented with a fixed number of registers that keep partial record of the history of the game. Although the register game is harder for Eve than the parity game on the same arena, if she can win the parity game, then she can also win the register game as long as she has a large enough number of registers. Exactly how many registers she needs depends on the parity game arena. We call this the register-index of the parity game: it is a measure of complexity which takes into account both the priority assignment of the parity game and the structure of the underlying graph.


Two key properties of register games then enable us to derive complexity results for finite  parity games as well as for parity automata on both words and restricted classes of trees. First, register games are automata-definable: there is, for every integer k, an alternating parity tree automaton that accepts infinite parity games of fixed maximal priority in which Eve wins the k register game; furthermore, for any alternating parity automaton , we can define a family of parameterised automata _k that use the k-register game as their acceptance game instead of standard parity games.
Second, the register-index is bounded logarithmically in the number of disjoint cycles of a parity game arena. 



  §.§.§ A quasi-polynomial algorithm for parity games
 For finite arenas, where the number of disjoint cycles is bounded by the number of positions, solving parity games reduces to solving the register game with a number of registers logarithmic in the size of the game. This results in a quasi-polynomial parity game algorithm with running time in 2^O((log n)^3), as well as a parameterised polynomial algorithm that solves classes of parity games with bounded register-index.




  §.§.§ Word automata transformations
 The complexity of solving parity games is intimately related to the complexity of turning alternating parity word automata (APW) into alternating weak word automata (AWW). Indeed, solving parity games amounts to checking the emptiness of an APW on the trivial singleton alphabet. Since the emptiness of AWW on the singleton alphabet can be checked in linear time <cit.>, a translation from APW to AWW immediately yields an algorithm for solving parity games of which the time complexity matches the size-increase and time-complexity of the automata translation.
 Note, however, that the automata-translation question is more general, since automata need not be defined over a one-letter alphabet, and even a binary alphabet can add substantial complexity.
 
Nevertheless, until 2017, the best known algorithms for the two problems were roughly the same: exponential in the number of priorities. A competitive tool for solving parity games is even based on the translation from parity to weak automata <cit.>.
In 2017, however, the advent of quasi-polynomial algorithms created a gap between the complexity of solving parity games, and the automata translation.

 
In this article, we show that the analysis of parity games that are infinite, or at least of unbounded size, allows us to generalise the quasi-polynomial time complexity of solving parity games to the blow-up incurred when turning alternating parity word automata into alternating weak automata[Recently a translation based on universal trees and infinite progress measures has further improved this upper bound to n^O(logd/log n)<cit.>.].





  §.§.§ The index hierarchy
While the translation of alternating parity automata into weak is always possible for word automata <cit.>, this is not the case for tree automata. Indeed, while alternating weak automata suffice to capture all ω-regular word languages, no fixed number of priorities suffices to capture all regular tree languages—this follows from the equivalence between alternating parity automata and the modal μ-calculus <cit.>, and the strictness of the modal μ-calculus alternation hierarchy <cit.>. We say that the parity index hierarchy is strict on trees, but collapses to the weak level over words. 

We study automata on structures that are, in some sense, between words and trees and show, using register games, a logarithmic collapse of the index hierarchy: for every alternating parity automaton  with n states, there is an alternating parity automaton ' with only O(log n) priorities that is equivalent to  over these structures.



  §.§.§ Of other quasi-polynomial automata
 Separating automata have been proposed as a way to understand the underlying combinatorial structure of the different quasi-polynomial algorithms <cit.>. We conclude with a discussion on what it would take for other quasi-polynomial algorithms for parity games, when seen as separating automata, to be extended into translations of alternating parity automata into weak automata.

 



This article is based on Lehtinen's quasi-polynomial algorithm for parity games <cit.>, which introduced the notion of register games, and Boker and Lehtinen's extension of this technique into a translation of alternating parity word automata into weak automata <cit.>. Here the definition of register games is simplified, generalised to infinite parity games, and presented from an automata-theoretic, rather than modal μ-calculus, perspective.












§ PARITY GAMES

 
[Parity games]
A parity game is an infinite-duration two-player zero-sum path-forming game, played between Eve and her opponent Adam on a potentially infinite game graph =(,_ e,_ a,,) called the arena. The positions  of the arena are partitioned into those belonging to , _ e, and those belonging to , _ a. The priority assignment : → maps every position in V

to a priority in a finite co-domain ={,+1..,} where ∈{0,1}. The edge-relation E⊆× defines the successors of each position. Without loss of generality we assume all positions to have at least one successor. On finite parity games of size n, we can assume ≤ n.

A play is an infinite sequence of positions =_0_1... such that (_i,_i+1)∈ E for all i≥ 0. 




A play  is winning for Eve if the highest priority that occurs infinitely often along  is even; otherwise it is winning for Adam.

A (positional) strategy  for a player ∈{,} in a parity game  maps every position  belonging to  in   to one of its successors.


 A play is said to agree with a strategy  for  if _i+1=(_i) whenever _i belongs to .
A strategy  for player  is said to be winning  for  from a position  if all plays starting at  that agree with  are winning for . We call the positions from which has a winning strategy 's winning region in , written ; 's winning region is written .

 We write , for the parity game  with a designated initial position . A winning strategy in , is a strategy that is winning from .



In all positions in a parity game, one of the players has a positional winning strategy.



It will sometimes be convenient, for clarity and aesthetics,  to assign priorities to edges, with Ω:E→ I. A parity game with edge priorities can be converted into one with vertex priorities by introducing intermediate, priority-carrying nodes onto edges and giving a low priority to other vertices. Conversely, a vertex-labelled parity game can be converted into an edge-labelled one by assigning the priority of a vertex to its outgoing edges.



§ REGISTER GAMES


This section describes the key technical development of this article: register games. These are parameterised variations of parity games, also played on a parity game arena. 
 Crucially, the winning condition of a k-register game is a parity condition that ranges over priorities 
 [0..2k+1]
 rather than the priorities of the arena.
 The larger the parameter k, the easier the k-register game becomes for Eve who, on arenas in which she has a winning parity game strategy, is guaranteed to also have a winning  k-register game strategy, for some large enough k. Note that the mechanics of register games have been simplified, compared to their first appearance in <cit.>; see Remark <ref>.
 


 §.§ Definitions and Observations

Informally, the k-register game 
 consists of a normal parity game, augmented with a 
 tuple (r_0,...,r_k)
 of registers that keeps a partial record of the history of the game. During a turn, several things happen: the player whose turn it is in the parity game moves onto a successor position of their choice, which has some priority p and Eve chooses an index i, 
 0≤ i≤k; 
 then, the registers get updated according to both i and p, and an output between 0 and 2k+1 is produced, also according to i and p.
 
 The update wipes out the contents of registers with index lower than i: for j< i, r_j is set to 0. Meanwhile r_i is set to p and r_j for j>i to max(r_j,p). In other words, each register r_j keeps track of the highest priority seen since Eve last chose i with i≥ j.
 The output is 2i if max(r_i,p) is even, and 2i+1 otherwise.
 

 Then, in the limit, Eve wins a play if the largest output that occurs infinitely often is even.


 Since the winning condition of the register game is a parity condition, we can formally define the k-register game on a parity game arena  as a parity game on an arena k, of which the positions are positions of  paired with vectors in 
 ^k+1
  that represent the contents of the registers. An additional binary variable t indicates whether the next move consists of Eve's choice of register (t=0), or a move in the underlying parity game (t=1).
 
[Register game]
Let  be a parity game  (^,^_ e,^_ a,^,^) and let  be the co-domain of ^:^→. For a fixed parameter k∈N, the arena of the k-register game k on  in which controls the registers, consists of k=(,_ e,_ a,,) as follows. 

While  carries its priorities on its vertices, for the sake of clarity, k carries them on its edges, : → [0..2k+1].

 


  *  is a set of positions (,,t)∈^×^k+1×{0,1},

  * _ a consists of (,,1) such that ∈ V^G_ a,

  * _ e consists of ∖_ a,


  *  is the disjoint union of sets of edges _𝑚𝑜𝑣𝑒 and E_i for all i∈ [0..k] where:

_𝑚𝑜𝑣𝑒 consists of edges ((,, 1),(,,0)) such that (,)∈^.


For each i∈ [0.. k], _i consists of edges ((,, 0),(,',1)) such that:


  * r'_j=max(r_j,^()) for j>i,

  * r'_j=^() for j=i, and

  * r'_j=0 for j< i.


  * Ω assigns priorities from [0..2k+1] to edges as follows:


  * Edges of E_𝑚𝑜𝑣𝑒 have priority 0;

  * ((p,, 0),(p,',1))∈ E_i has priority 2i if max(r_i,p) is even, and priority 2i+1 otherwise.






  §.§.§ Terminology
 Given a play in k, we call the underlying play its projection onto the first element of each visited position. At a position (,r̅,t), we write that: a priority ∈ occurs  if ^()=; a register i∈ [0.. k] contains a priority ∈ if r_i=; Eve chooses register i and outputs j∈ [0.. 2k+1] if the play follows an edge in _i of priority j. 


 A strategy for in  induces a strategy for in kG. A strategy for in  paired with a register-choosing strategy in kG induces a strategy for in kG.
 Observe that as the winning condition depends on the outputs that occur infinitely often, and that registers up to the largest one chosen infinitely often renew their contents infinitely often, if a player has a winning strategy in k from (, , t), then they have a winning strategy from all (,  ,). We will then simply say that they have a winning strategy from .


The k-register game arena k where controls the registers is similar to k except that positions (,,0) are in _ a, edges in _𝑚𝑜𝑣𝑒 have priority 0, and edges ((,, 0),(,',1)) of _i have priority 2i+2 if r_i is even, and  2i+1 otherwise. The k-register game with (resp., ) in control of registers on an arena  is the parity game on the arena k (resp., k).
Unless specified, the k-register game on  refers to  k.


For fixed k, k is a parity game on an arena of size polynomial in the size of  and of priority domain [0..2k+1]: it can be solved in polynomial time in the size of  using any solver exponential in the number of priorities (e.g. a progress measure algorithm <cit.>).


 
 We now establish two important facts about register games: if has a winning strategy from a position  in a parity game , then he has a winning strategy from all positions (,,t) in k for any k. However, if has a winning strategy in  from , then she also has a winning strategy from all (,,t) in k as long as k is large enough.
 
 
 
 If has a winning strategy in the parity game  starting at , then he also has a winning strategy in k starting at 
 
 for all k.
 
 
 
Assume has a strategy  in  that is winning from . On any play  starting at 

that agrees with , the highest priority  seen infinitely often is odd. Let i be the highest register chosen infinitely often by during . Then, eventually—that is, after the last occurrence of anything higher than  and after no longer chooses registers higher than i—whenever  is seen, r_i is set to  and remains at  until Eve again chooses i. Then, since  is odd, this outputs 2i+1. Since  occurs infinitely often and i is picked infinitely often, 2i+1 is output infinitely often. It is also the highest value output infinitely often because i is the highest index picked infinitely often. Since 2i+1 is odd,  is winning for . The strategy  is therefore winning for in k from  position .
 

 
 If has a winning strategy in the parity game  with parity co-domain  at a position _ι, then she also has a winning strategy in k from 
_ι 
 
 for k≥ i where 2i is the largest even priority in .
 
 
 
 Given a strategy  in the parity game  that is winning for from _ι, let ' be the following strategy for in k where k≥ i and 2i is the largest even priority in : at positions (,,1) the strategy ' follows , that is if  belongs to , then '(,,1)=(,,0) where ()=; at positions (,,0) where ^()=2i or 2i+1 for some i, the strategy ' chooses register i.
 
 We now argue that ' is winning for in k from _ι. Since ' follows  in the underlying game, the highest priority  that occurs on any play beginning at _ι that agrees with ' is even, say =2i for some i. The highest register chosen infinitely often is therefore i. Since eventually nothing higher than  occurs anymore, r_i will eventually remain  in perpetuity, and therefore, eventually, every time chooses i, this outputs 2i; since this is the highest register chosen infinitely often, nothing higher is output infinitely often. Hence wins every play that agrees with ' from _ι. 
 
 




The number of registers that needs to win the register game on a parity game in which she has a winning strategy depends on the complexity of her winning strategy. We define this as the register index of a parity game and consider it as a measure of complexity for parity games, comparable to measures such as entanglement <cit.>.


 [Register-index]
A parity game   has register-index k at ∈ if k is the smallest integer such that wins k from ,

and at ∈ if k is the smallest integer such that wins k from 
. A parity game  has register index k if k is the minimal integer such that it has register index up to k at all positions.

 




The register game defined here differs slightly from the one defined in <cit.> and used in <cit.>. Here, for a more elegant presentation, Eve chooses a register at every turn, but has an additional 0-indexed register she can default to. This avoids having  an additional priority that encodes that Eve must reset infinitely often. Furthermore, and perhaps  more significantly, the register update mechanism is simplified: instead of values shifting between registers, all registers below the chosen one get reset to 0 while the chosen register updates to the current priority.
This new game mechanism simplifies Eve's strategies and in particular the proof of Theorem <ref>.
 Finally, we do not restrict register games to finite arenas, but consider them on potentially infinite ones.




 §.§ Examples
 In this section we explore which features of parity games affect the register index, and which do not.
Since the register-index depends on a player's winning regions, the examples presented in this section are all on one-player games: all positions belong to . They can  be embedded into two-player games of arbitrary complexity; however, for the register-index, only the game induced by the simplest winning strategy matters.

We begin by looking at register games with a small number of registers, starting with 0-register games.
We observe that wins the 0-register game if she has a strategy σ such that plays that agree with σ see finitely many odd priorities, such as the game depicted in Figure <ref>. Indeed, if follows such a strategy, then eventually all outputs in the 0-register games are 0.


Among well-known parity games with register-index 0 are the example games for which strategy improvement and divide-and-conquer algorithms exhibit worst-case complexity <cit.>.



While parity games with register-index 0 must be quite simple, register-index 1 already captures games with more complexity. Example <ref> for instance dicusses games with high entanglement, high tree-width, and a large number of priorities that have register-index 1. Known examples of families of parity games of register-index 1 are those that exhibit worst-case complexity for Zielonka's recursive algorithm and the quasi-polynomial progress measure algorithms <cit.>. In these games every odd priority is immediately followed by a larger even priority, so still has an easy 1-register game strategy consisting of choosing register 1 whenever an even priority occurs, and register 0 otherwise. 



Figure <ref> shows an edge-labelled arena in which wins the parity game but loses the 0-register game.
In the 0-register game, 's strategy is to loop at the current position once (this clears the register), then move to the other position and repeat; has no choice but to produce outputs 1 and 0 infinitely often.

can win the 1-register game by choosing register 1 after seeing 2, and register 0 after seeing 1 or 0.

Figure <ref> illustrates a slightly more complicated family of parity games, which has linear entanglement, tree-width and number of priorities, yet constant register-index 1. It consists of arenas with vertices v_0...v_n with priority edges (v_j,v_i) of priority 2i for j≤ i and 2j-1 for j>i.
's strategy is to choose register 1 whenever she sees an even priority and register 0 otherwise. Since odd priorities only occur after a larger even priority, with this strategy register 1 permanently contains even priorities. Then every occurrence of an even priority leads to output 2, while odd priorities lead to output 1.




We have seen some parity games of low register-index. Building parity games of high register-index is more involved and requires, as we shall see, exponentially many positions.


For all n, there exists a parity game of register-index at least n.



Let H_0 be the game arena consisting of a single node, belonging to , with a self-loop of priority 0. This unique node is also the initial node of H_0.

Then, for all n>0, the arena H_n consists of two distinct copies of H_n-1 with initial positions v_0 and v_1
respectively, with an edge (v_0,v_1) of priority 2n-1 and an edge (v_1,v_0) of priority 2n. The position v_0 is also the initial position of H_n. See Figure <ref>.

 wins these parity games H_n because all cycles are dominated by an even priority. We will show that for n>0, has a winning strategy in the n-1-register game n-1H_n. 

We reason inductively, and show that for each H_n, n>0, that i) from the initial position in mH_n for m≥ n-1, with a register configuration in which register contents are bounded by 2n-1, can force the game to output 2n-1 or a higher odd priority, before returning to the initial position, and ii) loses in n-1H_n.



  Base case has a winning strategy in 0H_1: His strategy is to loop once in the current position to see 0—this sets the register content to 0; he then moves to the other position and repeats. This causes both 0 and 1 to be output infinitely often.

If uses this strategy in mH_1 for m≥ 0, starting from a register configuration in which register contents are bounded by 1, although he can't win, he can force the game to output 1 or a higher odd priority before returning to the initial position.



  Inductive step Assume i) and ii) for H_n.

i) Consider the following strategy for in mH_n+1 for m≥ n. He first moves from v, the initial position of H_n+1 onto the initial position v' of the second component of H_n+1, via the odd priority 2n+1.
Then, he plays in H_n, which only contains priorities smaller than 2n+1, with a strategy that is winning in n-1H_n. To counter this strategy, has to eventually choose a register of index n or higher, after which returns to the initial position. This is his strategy τ_n. Observe that if at the initial position all register contents are bounded by 2n+1, then will either lose in the second H_n component, or choose a register of index n or higher when it contains the odd priority 2n+1, outputting 2n+1 or a higher odd priority.

ii) We now show that he also has a winning strategy in nH_n+1. He begins by playing τ_n until 2n+1 is output and the play is back at the initial position. Note that some registers now might contain 2n+2,
so he can not yet repeat τ_n. Instead, he  plays a strategy that is winning in n-1H_n in
the first H_n component of H_n+1. Again, will lose unless she chooses register n. After she has chosen the register n, all the registers hold values smaller than 2n+1. can then return to the initial position, and again use τ_n to force output 2n+1. Thus by alternating between using τ_n to force the maximal odd output, and clearing the registers of higher priorities in order to be able to use τ_n+1 again, forces 2n+1 to be output infinitely often. 

Hence H_n has register-index at least n.







 §.§ The register-index as a measure of complexity

Given the elusiveness of a polynomial algorithm for parity games, there is a rich line of research in algorithms that are polynomial for restricted classes of parity games. The size of the priority co-domain is perhaps the simplest way of measuring the complexity of parity games: many parity game algorithms are exponential in the number of priorities, and therefore polynomial on parity games with a fixed number of priorities.
There are also many graph-theoretic restrictions, such as bounded tree-width, bounded clique-width and bounded entanglement, that allow for polynomial algorithms. These two classes of restrictions are orthogonal in the sense that the size of the priority assignment is agnostic to the underlying graph and vice-versa.

In contrast, the register-index can be seen as a measure of complexity that takes into account both the complexity of the priority assignment and the structure of the underlying parity game graph. Since for bounded k the register game over a game  is just a parity game of polynomial size in ||, solving parity games of bounded register-index is polynomial. Since we may not know the register-index in advance, by solving both k and k up to fixed k, we obtain a parameterised polynomial algorithm which solves games of register-index up to k, and does not return an answer for other arenas.

From the analysis in the previous sections, this algorithm seems likely to be effective on many—perhaps most—reasonable parity games. In particular, parameter 1 suffices to solve various parity games that are hard for existing algorithms, including other quasi-polynomial algorithms; furthermore, the register-index is independent of measures such as tree-width and entanglement. In this sense, this algorithm is complementary to existing ones. In any case, as we shall see in the next section, a logarithmic parameter suffices to solve all finite parity games, making this algorithm quasi-polynomial.




§ REGISTER GAMES AND FINITE PARITY GAMES


So far we have defined both parity and register games on potentially infinite arenas.

In this section we consider the special case of finite arenas, which is of particular interest for verification and synthesis.

We show that for finite parity games, the register-index is logarithmically bounded in the number of disjoint cycles, and by extension in the size of the game.
We deduce a quasi-polynomial algorithm for solving finite parity games.




 §.§ Logarithmic bound on the register index of finite parity games

This section presents the key technical result, from which the various results in the sequel follow: the register-index is logarithmic in the number of disjoint cycles in a finite parity game.


For a finite directed graph G, we call  the maximal number of vertex-disjoint cycles in G; the of a parity game is that of the underlying directed graph.

In order to build strategies from subgame strategies, we define the notion of a defensive strategy. Indeed, an arbitrary winning strategy in a subgame may output a finite number of large odd priorities; this is problematic when this strategy is used in a subgame that a play can enter infinitely often. Defensive strategies avoid high odd priorities from the start.


[Defensive register-index]
For a subgame  with priorities bounded by p, in which has a winning strategy, a winning strategy  for in k is defensive if, from positions (,,0) where r_k≥ p and r_k is even, a play that agrees with  never outputs 2k+1.
 has defensive register-index k if k is the minimal integer such that has a defensive winning strategy in k from all positions.






The register-index k of a finite parity game of z is at most 1+log z.



From the definition of register-index,
it suffices to consider the single-player parity games  induced by any winning strategy for in her winning region.
Observe that in the register games on , all positions with multiple successors belong to and 's strategy consists of just choosing a register after each move in the underlying game.

We show by induction on the number of positions n in  that the defensive register-index of  is bounded by 1+ log z; the theorem follows. The base case, n=1, is trivial.
For the inductive step where  has at least two positions, let G' be the game induced by positions of  of priority up to p-2, where p is the even supremum of priorities that appear in . Then, let G_1,…,G_j be the maximal strongly connected subgames of G'. Let k_1,…,k_j be their respective defensive register-indices, and m the maximal among these.  
If there are no such subgames, then p is the maximal priority in all cycles; then Eve wins defensively in 1 by choosing register 1 when p occurs and register 0 otherwise. Since no priority higher than p occurs, r_1 always contains either p or the initial value of r_1; this strategy is therefore winning and defensive.



  Case of a unique i for which k_i=m and m>0
We show that the defensive register-index of  is no more than m. Since the of _i is no larger than z, and from the inductive hypothesis m≤ 1+log z, this suffices. 

Eve's strategy in the m-register game on G is as follows:  within a subgame G_j she uses the bottom  k_j registers to simulate her defensive winning strategy in the k_j-register game on G_j; elsewhere, she chooses register m whenever p occurs and register 0 otherwise.

Assume that this strategy is played from a register-configuration where the top register contains an even priority greater or equal to the largest priority in . First observe that after choosing register m upon seeing p, r_m is set to p. Furthermore, this strategy encounters p between any two entrances into _i, and outside of _i chooses register 0≠ m whenever p does not occur; therefore plays that agree with this strategy always enter G_i with either p or the larger even initial r_m-value in register m. Thus, since the strategy within _i is defensive, it never outputs 2m+1 in _i. Similarly, when p occurs max(r_m,p) is always even: r_m is either its initial value, p, or a smaller priority from _i.  Plays that agree with this strategy either eventually stay within a subgame G_j where follows a winning strategy, or change subgames infinitely often. In the latter case, p is seen infinitely often, thus producing 2m as output infinitely often. This strategy is therefore both defensive and winning for .

Note that if this strategy is played from a register-configuration in which the top register is not an even priority greater or equal to the highest priority in , then a play might output 2k_m+1 once, but the values output infinitely often will still be the same as above, so the strategy is still winning.



  Case of i,j where i≠ j and k_i=k_j=m 
We show that the defensive register-index of  is at most m+1. This suffices, since by the induction hypothesis, each of _i and _j has at least 2^m-1; then  has at least 2^m as G_i and G_j are disjoint. 
's strategy in the m+1-register game on  is as follows:  in a subgame G_i, she uses registers up to k_i to simulate a winning strategy in the k_i-register game on G_i; elsewhere, she chooses register m+1 when p is seen, and register 0 otherwise. This strategy is winning as a play either eventually stays within a subgame where is following a winning strategy, or it enters some subgame infinitely often. In this case, it  must see p infinitely often; then 2(m+1) is the highest value output infinitely often since after the first occurrence of p register m+1 permanently contains p. Furthermore, if the initial content of register m+1 is an even priority larger than any occurring in , then every time chooses register m+1, the output is even; the strategy is therefore defensive.


  Case of m=0 

Eve can win the 1-register game on G, using a strategy as above: within a subgame _i, she uses her strategy in the 0-register game, and chooses register 1 whenever p is seen. This strategy is winning since a play either remains in a subgame and follows a winning strategy, or sees p infinitely often and therefore outputs 2 infinitely often, but does not output 3 infinitely often. If initially r_1 contains an even priority greater or equal to the maximal priority in , this strategy never outputs 3 and is therefore defensive.








The logarithmic bound was shown in <cit.> with respect to the size of a finite parity game directly; in <cit.> it was strengthened to a logarithmic bound with respect to the maximal number of disjoint strongly connected components. Here we opt for the number of vertex-disjoint cycles, which is equivalent but more intuitive.








 §.§ A quasi-polynomial algorithm for parity games


The quasi-polynomial solvability of parity games then follows: 
to solve a parity game  of size n, one can always solve 1+log n instead. 



Parity games are solvable in quasi-polynomial time.


Let n be the number of positions in a parity game  with d distinct priorities and m edges. The game k has 𝒪(nd^k+1) positions, priorities up to 2k+1 and 𝒪((m+nk)d^k) edges. Since k is presented with its priorities on its edges, for the complexity analysis we take the size of k to be O(knd^k), to account for an additional vertex for each of the O(knd^k) edges of significant priority—that is, those in E_r for some r∈[0..k].

From Theorem <ref>, the register-index of a parity game of size n is at most 1+log n. Therefore solving parity games G reduces to solving k where k=1+log n.
The k game can then be solved with an algorithm exponential in the number of priorities of one's choice, say the small progress measure algorithm <cit.>, to obtain a quasi-polynomial algorithm that runs in time 2^𝒪((log n)^3).


Without further optimisations, the complexity of this algorithm is not competitive with respect to existing quasi-polynomial algorithms; its space-complexity, due to building 1+log n, is also quasi-polynomial. We refer the reader to Parys's <cit.> and to Daviaud, Jurdziński and Thejaswini's <cit.> recent work that shows how to bring both the space and time complexity down to match other quasi-polynomial algorithms.
 Furthermore, as discussed in Section <ref>, many games have low register-index, including those that exhibit worst-case complexity for other algorithms; on such games this approach is expected to work well. Section <ref> discusses further ideas to adapt this approach for practical usage.


One of the principal appeals of this technique for analysing parity games comes undoubtedly from the logic and automata-theoretic perspective.
In the sequel, we turn our attention to infinite parity games, or at least parity games of unbounded size, which we use to build automata transformations based on register games.



§ REGISTER GAMES AND PARITY AUTOMATA



Parity automata are closely related to parity games. On one hand, the language of parity games (represented as infinite trees) with a fixed number of priorities in which Eve has a winning strategy is recognised by an alternating parity tree automaton. On the other hand, the acceptance game for alternating parity automata—both on trees and on words—is an infinite parity game.

In this section we first establish that register games are, like parity games, automata-definable: the winning regions of k-register games on arenas with d priorities are recognised by an alternating parity tree automaton of size O(d^k).
We then use register games on infinite and unbounded arenas to define a quasi-polynomial translation from alternating parity word automata into alternating weak word automata.



We finish with a discussion of how these techniques generalise to restricted classes of tree automata, on which we observe a partial collapse of the parity index hierarchy.


We begin this section by fixing notations and definitions for ω-word and tree automata with parity acceptance conditions.






 §.§ Automata on Words, Trees and Games




  §.§.§ Words, trees, games and graphs

A word over Σ is a (possibly infinite) sequence w=w_0 w_1⋯ of letters in Σ. We write (w) for the set of suffixes of w (which includes w itself).
We consider a tree to be an infinite directed rooted tree in the graph-theoretic sense; in particular, the children of a node are not ordered. A Σ-tree t (resp. Σ-graph) is a tree (resp. graph) together with a mapping of each of its nodes to a letter in Σ. We write (t) for the set of Σ-subtrees of t (which includes t itself). A Σ-graph with an initial vertex unfolds into an infinite Σ-tree; a regular Σ-tree can be finitely represented by a Σ-graph (i.e., Kripke structures).

We will use a game alphabet ^d={A_i,E_i|i∈ [0..d]} to represent parity games with priorities up to d. A ^d-tree, or graph, is interpreted as the infinite or finite parity game on the arena consisting of the tree, or graph respectively, where positions labelled E_i belong to , positions labelled A_i belong to , and positions labelled E_i or A_i have priority i.



  §.§.§ Automata



Several different definitions of alternating tree automata exist. One variable is the branching type of the input trees: fixed or arbitrary, with or without an order on the successors. In the context of parity games, it is most natural to operate in a setting with arbitrary branching without an order on the successor nodes—that is, an automaton can not distinguish between the left and right branch of a binary tree, unless this is encoded in the labelling. Another difference in automata definitions is how flexible the transition condition is with respect to ϵ-transitions and the combination of path quantifiers (,) and boolean connectives (,). Usually, all of these definitions give the same expressiveness (<cit.> and <cit.>), except for the case of very restricted automata, in which they do not <cit.>. In our definition of alternating automata, there are no epsilon transitions and path quantifiers are applied directly on states.

An alternating parity tree automaton is a tuple Σ,Q, ι, δ, Ω where Σ is a finite alphabet, Q is a finite set of states, ι∈ Q is an initial state, δ:Q×Σ→({,}× Q) is a transition function, (X) is the set of positive boolean formulas over X, and Ω:Q→ I is a priority assignment that assigns priorities from I=[0..i] or I=[1..i], for some i∈, to states. 
Intuitively, given a state and a letter, the transition function returns a positive boolean formula that defines which states the
automaton can transition to, and whether it considers the next state at a non-deterministically chosen child (), or at all of the children (). Positive boolean formulas over {,}× Q are called transition conditions. The transition graph of  is the graph (Q,E) where (q,q')∈ E if q' appears in δ(q,α) for some α∈Σ.




















Büchi and co-Büchi automata are  special cases of parity automata in which I={1,2} and I={0,1} respectively.
An automaton is weak if every strongly connected component in the transition graph consists of states with either only odd priorities or only even priorities.
Observe that a weak automaton can be seen as either a Büchi or co-Büchi automaton by using priorities 1 and 2, or 1 and 0, respectively.


The size of an automaton is the maximum of the alphabet size, the number of states, the number of subformulas in the transition function, and the acceptance condition's index, that is |I|. Observe that in alternating automata, the difference between the size of an automaton and the number of states in it can stem from a transition function that has exponentially many subformulas.
 


How exactly nondeterminism in tree automata is defined also varies in the literature. In general, it only concerns the boolean connectives of the transition condition and not the path quantifiers. We consider an alternating automaton to be nondeterministic (resp. universal) if its transition conditions only use the  (resp. ) connective, in addition to the path quantifiers  and .

A word automaton is simply a tree automaton that operates on unary trees, that is, ω-words. For word automata, the path quantifiers  and  are equivalent as there is always exactly one successor. 

We will also mention deterministic word automata, in which the transition condition has no boolean connectives, and safety automata, in which the only rejecting state is a rejecting sink.

The class of an automaton is determined by its transition mode (deterministic, nondeterministic, or alternating), its acceptance condition, and whether it runs on words or trees.
We often abbreviate automata classes by  acronyms in {D, N, A}×{W, B, C, P}×{W, T}. The first letter stands for the transition mode; the second for the acceptance-condition (weak, Büchi, co-Büchi, and parity); and the third indicates whether the automaton runs on Words or on Trees. For example, AWW stands for an alternating weak automaton on words.



We define the semantics of automata directly in terms of their acceptance games.

[Acceptance game]
Given a Σ-tree t and an APT =Σ,Q,ι,δ,Ω, the acceptance game t is the following parity game:


  * The set of positions is (t) × (Q ∪({, }× Q)).

  * For a∈Σ, a Σ-tree u whose root is labeled a, transition conditions b and b', and state q∈ Q, there is an edge from:




  * (u,q) to (u, δ(q,a))

  * (u,b∨ b') to (u,b) and (u, b')

  * (u, b∧ b') to (u,b) and (u, b')

  * (u, q) to (u',q), for every child u' of u.

  * (u, q) to (u',q), for every child u' of u.






  * Positions ( q,u) and (b∧ b',u) belong to Adam; other positions belong to Eve.

  * A position (u,b) is of priority Ω(b) if b is a state q, 


and 0 otherwise.

Observe that the  acceptance games of regular, i.e., finitely representable, trees are finite since these trees only have finitely many distinct subtrees. For a Kripke structure S, we write S for the acceptance game t where t is the tree represented by S, and observe that it is finite.



We say that an APT  with initial state ι accepts a tree t if and only if Eve has a winning strategy in the acceptance game t from (t,ι). A tree automaton accepts or rejects a graph according to whether it accepts or rejects its infinite tree unfolding. The set of trees accepted by  is called the language of , denoted by L(). Two automata are equivalent if they recognise the same language.

As a word is a special case of a tree, Definition <ref> and other results that will be shown on acceptance games apply also to word automata. In the word setting, the presentation of the acceptance game can be simplified: q and q are equivalent, and may thus be written q, and Q ∪(Q) is equal to (Q).




 §.§ Automata for Register Games

We define for every APT  and positive integer k, the parameterised version _k, which is an APT that will be shown to accept a tree t if and only if Eve wins the k-register game on t starting from (t,ι). The idea is to emulate the k-register game by keeping track of register configurations with a tuple ∈ I^k+1 that is updated according to which priorities are seen and Eve's register choices, which are represented as nondeterministic choices in _k. The outputs are captured by the priorities of the states of _k. Here we note a slight subtlety: In the k-register game on t, Eve chooses registers not only at positions (u,q) where q is a state of , but also at positions (u,b) where b is a boolean formula. In _k only states can have priorities (i.e., there can only be one priority per move in t) so we aggregate the outputs from these choices between two states by taking the largest output into the priority of the next state—this is the third element p∈ [0..2k+1] of the states of _k.


Given an APT =Σ,Q,ι,δ,Ω with Ω:Q→ I and a positive integer k, we define an APT _k=Σ,Q',ι',δ',Ω' as follows:


  * Q' = Q× I^k+1× [0..2k+1]

  * ι' = (ι,(0,..,0),0)

  * Ω': For every q∈ Q, ∈ I^k+1, and p∈[0..2k+1], we have Ω'(q,,p)=p.


  * δ': For every q∈ Q, ∈ I^k+1, p∈[0..2k+1], and a∈Σ, we have δ'((q,,p),a) = ⋁_i∈ [0..k](δ(q,a),_i(,Ω(q)),max(r_i,Ω(q))) where for transition conditions b,b':


  * _i(,p)= ' where r_j'=max(r_j,p) for j>i, r_i=p and r_j=0 for j<i;

  * ( q',,p)=⋁_i∈ [0.. k] (q', _i(,0),m) where m=2i if max(r_i,p) is even; 2i+1 otherwise;

  * ( q',,p)=⋁_i∈ [0.. k] (q', _i(,0),m)
where m=2i if max(r_i,p) is even; 2i+1 otherwise;

  * (b ∧ b',,p)=⋁_i∈ [0..k](b, _i(,0),max(r_i,p))∧(b', _i(,0),max(r_i,p))

  * (b ∨ b',,p)=⋁_i∈ [0..k](b, _i(,0),max(r_i,p))∨(b', _i(,0),max(r_i,p))









Given an APT  and a positive integer k, the parameterised APT _k accepts a tree t if and only if Eve wins the k-register game on t from (t,ι).


Recall that _k accepts a tree t if and only if Eve wins the parity game t_k from the initial position, which consists of _k's initial state and t's root. Thus, we should show that Eve wins t_k from the initial position if and only if she wins the k-register game on t from the initial position. The intuition for the equivalence between the games is that t_k encodes the k-register game on t by having the register-configuration in the state space, Eve's register choices as new disjunctions, and the highest output between two states as priorities.

Positions of t_k are in 

    (t)×((Q× I^k × [1..2k+1]) ∪({, }× Q× I^k × [1..2k+1]))

while positions of the k-register game on t  are in
(t)×(Q ∪({, }× Q)) ×   I^k.

t_k begins at (t,(ι,(0,..,0),0)) while the k-register game on t begins at (t,ι,(0,..,0)).

Now, observe that in the k-register game on t at position (u,q,), for a state q∈ Q and a Σ-tree u whose root is labeled a, Eve has to choose a register i∈ [0.. k] before the parity game proceeds to (u,δ(q,a)) with register configuration ', which is exactly _i(,Ω(q)). Similarly in t_k, from (u,q,x̅,p) Eve chooses i∈ [0..k] before proceeding with the transition condition δ(q,a) with register configuration _i(,Ω(q)). In the register game on t, this produces an output 2i if max(r_i,Ω(q)) is even; 2i+1 otherwise. In t_k the value max(r_i,Ω(q)) is kept in the state of the successor position.

When the games proceed, in both the register game on t and in the parity game on tA_k, the decision falls to if δ(q,a) is a conjunction or prefixed by  and to otherwise. Then, between each subformula of the transition condition, Eve again has a choice of register in both games. In the register game on t, this produces an output 2i if max(r_i,0) (that is r_i) is even; 2i+1 otherwise. The largest output between two positions in Q×(t) of t is recorded via the third element of the automata-component of t_k, which determines the priority of the successor state.







Then a winning strategy for Eve in one game translates into a winning strategy for Eve in the other game by mapping 's choices of registers in the register game on t to her choices in t_k at disjunctions over [0..k] in the transition condition of  and vice versa, and mapping her choices in the underlying parity game t to the remaining choices in t_k, and vice-versa.



The μ calculus-minded reader can get an idea of the equivalent modal μ-calculus formula from <cit.> where the definability of register games was presented from a logic-perspective, rather than in terms of automata. The following proof in particular uses the automata-equivalent of the canonical modal μ-calculus formulas that witness the strictness of the alternation hierarchy <cit.>.










There is a parity automaton of size d^O(log n) that, over ^d-graphs of size n and priorities up to d, recognises the parity games in which Eve has a winning strategy.



Let ^d be the alternating parity automaton on ^d-trees that, over parity game graphs with priorities up to d, recognises parity games with priorities up to d in which has a winning strategy. This is simply an automaton with states 0,1… d where the priority of a state i is i and the transition condition is δ(q,E_i)= i and δ(q,A_i)= i. 
The acceptance game t^d for any ^d-tree t is identical to t once we collapse positions with a unique successor. It follows that t and t^d have identical register-index. Then, from Theorem <ref> and Lemma <ref>, over ^d-graphs of size up to n and priorities up to d, ^d_log n+1 recognises the same language as ^d, which recognises the games in which Eve has a winning strategy.



This corollary casts the quasi-polynomial complexity of parity games in terms of their descriptive complexity—that is,  in terms of the complexity of the logical formalisms able to capture their winning regions. Note that here we only consider the complexity of recognising parity games with a bounded number of priorities (here bounded by the size of the game) in which has a winning strategy; for parity games with an unbounded number of priorities, this task is beyond the expressivity of parity automata and the μ calculus <cit.>.



Observe that the register-index is bisimulation-invariant.
Indeed, 
 we can build an automaton that accepts exactly parity games with priorities up to d that have register-index at most k.
Since alternating parity automata, like formulas of the modal μ-calculus, are bisimulation invariant, so is the register-index.  




 §.§ Register Games and Word Automata


We turn our attention to automata over ω-words. On words, deterministic parity automata, non-deterministic Büchi automata and alternating weak automata all are expressive enough to capture all ω-regular languages <cit.>. 
However, our understanding of the trade-offs in conciseness between different acceptance conditions is incomplete.  For instance, an ABW can be turned into an AWW with quadratic size blow-up <cit.>, but the current corresponding lower bound is at Ω(nlog n). Until recently the best translation from APW into AWW was exponential <cit.>; here we improve it to quasi-polynomial; the lower bound remains at Ω(nlog n).

 

In this section we use register games to define a quasi-polynomial translation from APW to AWW. It is based on observing that the acceptance parity games of an automaton on an ultimately periodic word have a register-index that depends solely on the automaton and is at most logarithmic in its size. Given that equivalence over ultimately periodic words implies equivalence over all words <cit.>, this will suffice to turn APW  into equivalent APW with a logarithmic number of priorities and of quasi-polynomial size; from there, Kupferman and Vardi's classic translation into weak automata <cit.> produces a weak automaton which is also of only quasi-polynomial size.


We begin by showing that the of t, for a tree t that represents the computations of a finite Kripke structure with minimum feedback vertex set size at most d in each of its (maximal) strongly connected components (SCC), is linear in d||. Then, since the register index is logarithmic in the , it is not the number of states in a Kripke structure that influences the register index of the acceptance game, but rather its minimum feedback vertex set. 
 For Kripke structures representing ultimately periodic words, this measure is 1. While a weaker lemma based directly on the single cycle of a Kripke structure representing an ultimately periodic word w would suffice, the next section will use this stronger lemma.



Given a directed graph G, a feedback vertex set is a set of vertices that contains at least one vertex of every cycle in G.
Let the fvs-size of G be the size of a minimum feedback vertex set of G.






Given a Kripke structure S with fvs-size up to d in each of its SCCs and an APT  with n states, the parity game S has register index at most 1+log dn.



We first note that the register index of a parity game is the maximal one among its SCCs.
We show that the dc-size of any SCC in S is at most dn. Then, by Lemma <ref>, its register index is at most 1+log dn.

First note that every SCC of S results from a single SCC of S and a single SCC of . It is therefore enough to assume that both S and  consist of a single SCC.

We consider the graph H that is derived from S by ignoring the intermediate positions (v,b), where b is a boolean formula between positions of the form (v,q), for a state q. That is, let H be the graph consisting of just the vertices (v,q) of S, where q is a state. The edges of H connect positions (v,q) and (v',q') if (v',q')  is reachable from (v,q) in S directly, that is, with a path which does not visit yet another position (v”,q”) where q” is a state.

Observe that SA has no larger than that of the graph H: a set of disjoint cycles in SA induces a set of disjoint cycles in H.

Let F be a feedback vertex set of S, having up to d vertices. Since every cycle C in H corresponds to some cycle of S, it must contain a vertex (v,q), such that q is a state of  and v∈ F. Hence, for every v∈ F, there are up to n vertex-disjoint cycles in H that have a vertex of the form (v,q). Therefore, there are up to |F|n ≤ dn disjoint cycles in H, and therefore in S.


In particular, given an ultimately periodic word and an APW  with n states, since the fvs-size of a lasso Kripke structure representing a word is 1, the parity game w has register-index at most 1+log n.











Then  is equivalent to its 1+log n parameterised version. On can then obtain an equivalent weak automaton of quasi-polynomial size by applying Kupferman and Vardi's transformation <cit.> to _1+log n instead of .



Every APW  is equivalent to its parameterised version _k, for k=1+log ||.


As two ω-regular languages are equivalent if they agree on all ultimately periodic words <cit.>, it suffices to argue that  and _k agree on ultimately periodic words.

From Lemma <ref>, _k accepts an ultimately periodic word w if and only if if Eve wins the k-register game on S_w where S_w is a finite Kripke structure representing w. Since S_w is a lasso, and it has fvs-size 1. From Lemma <ref>, Eve wins the k-register game on S_w exactly when Eve wins the parity game on S_w, that is, when  accepts w.




There is a translation of alternating parity word automata into alternating weak word automata incurring at most a quasi-polynomial size increase. In particular, every APW  of size (resp. number of states) n is equivalent to an AWW of size (resp. number of states) 2^O((log n)^3).


From Lemma <ref>, an APW  with n states and d priorities is equivalent to its parameterised APW _k for k=1+log n, having n · d^k · (2k+1) states and 2k+1 priorities. The automaton _k can then be turned into a weak automaton using standard techniques <cit.> with a O(m^d') blow-up, where m is the number of states and d' the number of priorities, which yields an AWW with 2^O((log n)^3) many states, since m is here O(kn^k+1), which is in 2^O((log n)^2) and d'=2k+1 is O(log n).

If the size of  is dominated by the size e of its transition function, namely when e>n, observe that the parameter k, the number of states in _k, and the number of priorities in _k do not depend on e, while the size of _k's transition function is  O(k^2ed^k) is in 2^O((log e)^2). Since the translation in <cit.> does not blow up the transition-function size more than it blows up the number of states, we end up with an AWW of size in  2^O((log e)^3).





 §.§ Register Games and Tree automata

While the parity hierarchy collapses for alternating word automata, that is, AWWs suffice to recognise all word languages recognised by APWs, it is strict for alternating tree automata <cit.>: For every positive integer n, there is an APT  with O(n) states and O(n) priorities, such that there is no APT equivalent to  with less than n priorities. Hence the weak condition does not suffice to capture all tree-languages captures by parity automata, so a general translation from APT to AWT does not exist. However, even for APT that are equivalent to an AWT, such a translation is at least exponential <cit.>, in contradistinction to the quasipolynomial translation of APW to AWW.






A natural question is then to consider the index hierarchy of alternating automata on entities that are “between” words and trees—that is, infinite trees generated by Kripke structures that are more complex than lassos, but more restrictive than trees. Examples of such classes are “flat Kripke structures” <cit.>, in which every SCC has a single cycle, “weak Kripke structures” <cit.>, in which SCCs cannot have two vertex-disjoint cycles and Kripke structures with finite Cantor–Bendixson rank <cit.>.


We show that the parity hierarchy collapses logarithmically for alternating automata on the classes of Kripke structures with bounded fvs-size in each of its SCCs. That is, for every APT  with n states, there is an APT A' with O(log n) priorities, such that  and ' are equivalent with respect to trees generated by Kripke structures of which the SCCs have bounded fvs-size. Kripke structures of which the SCCs have bounded fvs-size subsume Kripke structures that are flat, weak or of finite Cantor–Bendixson rank.































Every APT  with n states is equivalent to an APT ' with 1+log dn priorities with respect to Kripke structures with fvs-size of up to d in each of their SCCs.


Let k=1+log dn.
Setting ' to be the k-parameterised version _k of  fits the bill. Indeed:
 accepts a Kripke structure S iff Eve wins S. 
By Lemma <ref>, for every Kripke structure S with fvs-size of up to d in each of its SCCs, the register index of S is at most k.
Hence, Eve wins S iff she wins the k-register game on S, and by Lemma <ref>, this happens iff A_k accepts S.





Every APT with n states is equivalent to an APT with O(log n) priorities with respect to Kripke structures whose SCCs are bounded in one of the following measures: minimum feedback vertex set, minimum feedback edge set, maximal number of vertex-disjoint cycles, and maximal number of edge-disjoint cycles.


Observe that the minimum feedback vertex set is always smaller than or equal to the minimum feedback edge set, and likewise the maximal number of vertex-disjoint cycles is smaller than or equal to the maximal number of edge-disjoint cycles. Hence, it is enough to consider the vertex-version of these measures.

The result with respect to the minimum feedback vertex set follows directly from Theorem <ref>. 
The result with respect to the maximal number of disjoint cycles follows from Theorem <ref> and the Erdős-Pósa Theorem <cit.>, which states that the maximal number of disjoint cycles is logarithmically bounded in the minimum feedback vertex set.



It may be the case that this collapse of the index-hierarchy on these structures goes further, all the way to weak, as on words, combining techniques from Kupferman and Vardi <cit.> and Daviaud, Jurdziński and Lehtinen <cit.> for example, or to priorities {1,2,3} as for trees with a countable number of infinite branches <cit.>. We leave this as an open problem, as well as the related question of what is the simplest class of trees on which the hierarchy is strict.




§ OTHER QUASI-POLYNOMIAL AUTOMATA


In this section we discuss the relationship between our approach and the notion of separating automata for solving parity games.
Czerwiński et al. <cit.> have argued that the existing quasi-polynomial parity game algorithms can all be seen as separating automata. We consider the converse question: we make explicit how separating automata imply a tree automaton that recognises the winning regions of parity games of bounded size and propose a criterion delineating when a separating automaton also implies a translation of alternating parity automata into weak automata.











 §.§ From separating automata to tree automata

Bojańczyk and Czerwiński consider automata that separate plays that agree with winning strategies for each player in parity games of size up to n with up to d priorities <cit.>.
Finding a deterministic safety automaton of size f(n,d) that separates these word languages suffices to solve parity games in time polynomial in f(n,d).
If the separation condition is strengthened to a separation between the language of plays that agree with a positional winning strategy for in some parity game of size n with d priorities and the language of plays that do not satisfy the parity condition, then a quasi-polynomial lower bound applies <cit.>.

From a deterministic separating word automaton,  one can build a tree automaton that recognises parity game arenas of size up to n in which Eve has a winning strategy:


Let  be a DPW over the alphabet [0..] that:


  * Accepts words that agree with a positional winning strategy for in some parity game of size up to n with up to  priorities, and

  * Rejects words that agree with a positional winning strategy for in some parity game of size up to n with up to  priorities.


Then, there is an APT ' of the same size and acceptance condition as  that recognises parity game arenas of size up to n with up to p priorities in which Eve has a winning strategy.



While  operates on an alphabet of priorities, ' operates on the richer game alphabet ^ that also encodes the ownership of nodes.
' has the same state-space, initial state and priority assignment as . The only difference is the transition function of ' which is simply δ'(q,E_i)=δ(q,i) and  δ'(q,A_i)=δ(q,i). In other words,
 ' gives the decision of which branch to choose to the player who owns the current position, but otherwise operates exactly as . Whichever player has a winning strategy in a parity game   of size n with up to d priorities encoded as a -graph can copy their positional winning strategy in the acceptance game '; since  separates the plays resulting from such strategies, ' will accepts if and only if has a winning strategy in .


 
Proposition <ref> extends to good for games word automata <cit.>. These are (not necessarily deterministic) automata  over an alphabet Σ for which, given any Σ-labelled arena —that is, a graph of which the positions are partitioned between two players and labelled with Σ—wins the synchronised product of  and  if and only if she has a strategy σ in  such that every path that agrees with σ forms a word accepted by . 
Good-for-games parity automata, like deterministic automata, can be turned into APTs in the way outlined in Proposition <ref>. 

However, the register automaton that recognises whether Eve wins the k-register game over an arena of size n with up to d priorities, although separating plays that agree with a winning positional strategy for Eve from plays that are winning for Adam, is neither deterministic nor good for games. First, observe that for k>0, it is indeed trivially a separating automaton for words with up to d priorities since all words have register index 1. It is not good for games (of register index larger than k). It is only “good for small games" in the sense that when interpreted on games, it is only guaranteed to operates correctly on parity games of size up to 2^k-1.





 §.§ From tree automata to automata transformations



As we have seen in Section <ref>, register games are also suited for handling the  parity games of unbounded size that stem from word automata, thus allowing for a quasi-polynomial translation from alternating parity word automata to alternating weak automata. The same generalisation is not immediate for  Calude et al.'s and Jurdziński and Lazić's algorithms; in particular, a safety-automata based approach, as the one proposed by Czerwiński et al. <cit.> is unlikely to suffice since safety automata are not as expressive as parity automata. This raises the following question: when does an automaton that recognises the winning regions of parity games of bounded size imply a translation from alternating parity word automata into weak automata? 

We propose infinite directed acyclic graphs (dags) of bounded width as a key ingredient. The acceptance games for word automata take this shape, which make them an interesting stepping stone between words and trees. We shall see that tree automata with an acceptance condition X (e.g. Büchi or weak) that recognise infinite parity game dags of bounded width (rather than of bounded size) in which Eve has a winning strategy can be used to turn alternating parity word automata into word automata with the same acceptance condition X. The translation is easy: it consists of the synchronised composition of the two automata.


The technical details of the synchronised composition are cumbersome, but the idea is straight-forward: the synchronised composition of  and  is an automaton that accepts a tree  if and only if  accepts the acceptance game of  and  when viewed as a -tree.



[Synchronised Composition]
Let =(Σ^A,Q^A,ι^A,δ^A,Ω^A) be an APT with priorities up to d. Let =(^d,Q^B,ι^B,δ^B,Ω^B) be an APT over the game alphabet ^d.


The synchronised product  is defined as:




  * State space Q^A× Q^B;

  * Alphabet Σ^A;

  * Ω(q_A,q_B)=Ω^B(q_B).

  * Transition relation: δ((q_A,q_B),α)=f^α(q_A,δ^B(q_B,label(q_A)) where:






  * f^α(q_A, p) =  f^α(δ^A(q_A,α),p)

  * f^α(q_A, p) =  f^α(δ^A(q_A,α),p)


  * f^α(b∧ b', p)= f^α(b,p) ∨ f^α(b',p)

  * f^α(b∨ b', p)= f^α(b,p) ∨ f^α(b',p)

  * f^α( q, p)=  (q,p)

  * f^α( q, p)=  (q,p)

  * f^α(b∧ b', p)= f^α(b,p) ∧ f^α(b',p)

  * f^α(b∨ b', p)= f^α(b,p) ∧ f^α(b',p)

  * f^α( q, p)=  (q,p)

  * f^α( q, p)=  (q,p)

  * f^α(b,c∨ c')=f^α(b,c)∨ f^α(b,c')

  * f^α(b,c∧ c')=f^α(b,c) ∧ f^α(b,c')


  * f^α(b,p)=f^α(b,δ^B(p,(b))) where p∈ Q^B and

  * label(b∧ b')=label( q)=A_0

  * label(b ∨ b')=label( q)=E_0

  * label(q)=E_Ω^(q)
  


Observe that  has the acceptance condition of . Indeed, the product construction preserves the priorities and the non-reachability of states of : if q_B' is not reachable from q_B, then (q_A,q_B') is not reachable from any (q_A',q_B'). Then, if  is weak, then  is weak. 





 accepts a Σ^A-tree t if and only if  accepts the acceptance game t seen as a ^d-tree for d the maximal priority in . 


We show that t and t have the same winner.
The transition relation is designed so that 
 tAB is identical to t. More precisely, we identify positions ((t,q_A),q_B) and ((t,b_A),b_B)  in tAB with (t,(q_A,q_b)) and (t,f^α(b_A,b_B)) in t, respectively, where α is the label of t. We now show that this mapping preserves successors, position ownership and priorities; the preservation of winner follows.


  Preservation of successors We observe:



  * ((t,q_A), q_B) has successor ((t,q_A),δ^B(q_B,E_Ω(q_A)))


  * (t,(q_A,q_B)) has successor (t,f^α(q_A,δ^B(q_B,E_Ω(q_A))))


  * ((t, b∧ b'),  p)) has successors ((t,b),p) and ((t,b'),p)

  * (t,f^α(b∧ b', p)) has successors (t,f^α(b,p)) and ((t,f^α(b',p)))


  * ((t,  q),  p)) has successors ((t',q),p) for all children t' of t.

  * (t,f( q,  p)) has successors (t',(q,p)) for all children t' of t.


  * Similarly for other combinations of modalities and boolean operators.





  Preservation of ownership Eve owns position ((t,b_a),b_B) in tAB whenever b_A is a disjunction or a -formula, and positions with a unique successor. Similarly, Eve owns (t,f^α(b_a,b_B)) in t whenever b_B is a disjunction or -formula, and positions with a unique successor.


  Preservation of priorities The priority of both ((t,q_A),q_B) and (t,(q_A,q_B)) is  Ω^B(p) and the priority of other positions is 0.


Then, since t and t must have the same winner,  accepts a tree t if and only if  accepts .





Then, if for a class  of trees, for all ∈,  accepts (,) if and only if  accepts , then  is equivalent to  over . In other words, to turn an automaton  into a simpler automaton that is equivalent on a particular class of structures, it suffices to find an automaton  with a simple acceptance condition that accepts only the winning acceptance games of  over that class of structures. In particular, to turn a parity word automaton into a Büchi or weak automaton, it suffices to study Büchi or weak automata that recognise the winner in acceptance games over words.


An infinite dag is of bounded width m if its vertices can be partitioned into sets L_0, L_1, L_2, … no larger than n 
such that every edge goes from some layer L_i to the next
layer L_i+1.


An alternating parity automaton _(m,)  that over regular parity game dags of bounded width m with up to  priorities recognises those in which Eve has a winning strategy induces a translation from alternating parity word automata to alternating automata with the number of priorities of _(m,) and with state and size blow-up linear in |B_(m,)|.



The acceptance game of a ultimately periodic word w and an APW  with up to  priorities is a regular parity game dag of width || with up to  priorities; hence _(||,) recognises the winning regions of the acceptance games of  over ultimately periodic words. The automaton _(||,) is, from Lemma <ref>, equivalent to  on ultimately periodic words and therefore over all words. The synchronised product _(||,) is therefore equivalent to  and has the acceptance condition of _(||,). The blow-up is linear in _(||,)



The register index approach is an instantiation of this method: indeed, the key measure we use to bound the register index, , is also bounded in finite structures that can be unfolded into a dag of bounded width.
From these observations, it seems that reasoning about parity games of arbitrary size but with a bounded number of disjoint cycles, or infinite parity games of bounded width, rather than only finite parity games, is a key distinction between algorithms for solving finite parity games and translations from one type of automata into another. Indeed, this strategy was recently used by Daviaud, Jurdziński and Lehtinen to provide an alternative quasi-polynomial APW to AWW translation, based on universal trees, with size increase in n^O(logd/log n) <cit.>.





§ CONCLUSIONS
 

We have presented an automata-theoretic take on solving parity games in quasi-polynomial time based on the notion of register games. This perspective enabled us to go beyond finite parity games, and provide a quasi-polynomial translation of alternating parity automata into weak automata.



  §.§.§ Solving parity games in practice
 This article has focused on the automata-theoretic aspect of register games, rather than how they can be used to solve parity games in practice. We would therefore forgive the reader for questioning the practicality of this quasi-polynomial algorithm, which, among its less flattering features, has quasi-polynomial space complexity.

Recent work by Parys <cit.>, as well as by Daviaud, Jurdziński and Thejaswini <cit.>,  show that the register-game approach can be optimised to have  both time and space-complexity in line with the state-of-the-art.
Furthermore, there is much unexplored potential both for improving the practical viability of this algorithm, and for using the insights of this analysis to improve existing solvers.

Indeed, we have seen that building parity games with truly complex winning strategies—in the sense of requiring more than a small constant number of register in the register game—is subtle business: see the construction in Lemma <ref>. We therefore conjecture that the parameterised version of this algorithm, which solves parity games of register index 1, is a plausible candidate for solving most reasonable parity games in polynomial time, and perhaps also in practice. Increasing the parameter to 2 or 3 could ensure it only fails for purpose-built counter-examples.
The insight that even complex-looking parity games tend to have low register index could be useful in itself, for optimising existing solvers, which are not necessarily quasi-polynomial, but still more effective in practice.

Finally, the register index approach seems suited for a symbolic implementation: given a symbolically represented parity game, the k-register game can also be represented symbolically without significant blow-up. This would bypass the space-complexity of the algorithm for parity games that benefit from concise symbolic representations.



  §.§.§ Further open problems
 We have, throughout this article, pointed to some problems that remain open. The most obvious, of course, is the complexity of solving parity games. Another fundamental question is the conciseness gap between alternating parity and alternating weak word automata: a quasi-polynomial upper bound and a quasi-linear lower bound. One of the difficulties for closing this gap is the lack of techniques on one hand to prove lower bounds for alternating automata, and on the other to use alternations effectively to describe the winning regions of parity games.

We also mentioned the parity index problem, which is connected to the automata-theoretic concerns that this article touches upon. The question of where exactly, when moving from words to trees, the index hierarchy becomes strict, is particularly interesting.


alpha




