Udi Boker
email: udiboker@gmail.com

Denis Kuperberg
email: denis.kuperberg@ens-lyon.fr

Karoliina Lehtinen
email: k.lehtinen@liverpool.ac.uk

Michał Skrzypczak
email: mskrzypczak@mimuw.edu.pl

On the Succinctness of Alternating Parity Good-for-Games Automata (Full Version * )

Keywords: 2012 ACM Subject Classification Theory of computation → Logic and verification Good for games, history-determinism, alternation

We study alternating parity good-for-games (GFG) automata, i.e., alternating parity automata where both conjunctive and disjunctive choices can be resolved in an online manner, without knowledge of the suffix of the input word still to be read.

We show that they can be exponentially more succinct than both their nondeterministic and universal counterparts. Furthermore, we present a single exponential determinisation procedure and an Exptime upper bound to the problem of recognising whether an alternating automaton is GFG.

We also study the complexity of deciding "half-GFGness", a property specific to alternating automata that only requires nondeterministic choices to be resolved in an online manner. We show that this problem is PSpace-hard already for alternating automata on finite words.

Introduction

Good-for-games (GFG) automata were first introduced in [START_REF] Henzinger | Solving games without determinization[END_REF] as a tool for solving the synthesis problem. The equivalent notion of history-determinism was introduced independently in [START_REF] Colcombet | The theory of stabilisation monoids and regular cost functions[END_REF] in the context of regular cost functions. Intuitively, a nondeterministic automaton is GFG if nondeterminism can be resolved on the fly, only with knowledge of the input word read so far. GFG automata can be seen as an intermediate formalism between deterministic and nondeterministic ones, with advantages from both worlds. Indeed, like deterministic automata, GFG automata enjoy good compositional properties-useful for solving games and composing automata and trees-and easy inclusion checks [START_REF] Boker | Nondeterminism in the presence of a diverse or unknown future[END_REF]. Like nondeterministic automata, they can be exponentially more succinct than deterministic automata [START_REF] Kuperberg | On determinisation of good-for-games automata[END_REF].

In recent years, much effort has gone into understanding various properties of nondeterministic GFG automata, for instance their relationship with deterministic automata [START_REF] Boker | Nondeterminism in the presence of a diverse or unknown future[END_REF][START_REF] Kuperberg | On determinisation of good-for-games automata[END_REF][START_REF] Boker | How deterministic are good-for-games automata[END_REF][START_REF] Kuperberg | Computing the width of non-deterministic automata[END_REF], Many questions about GFG alternating automata were left open, in particular whether there exists a doubly exponential succinctness gap between alternating GFG and deterministic automata, and the complexity of deciding whether an alternating parity automaton is GFG.

Succinctness of alternating GFG automata. We show that there is a single exponential gap between alternating parity GFG automata and deterministic ones, thereby answering a question left open in [START_REF] Boker | Good for games automata: From nondeterminism to alternation[END_REF]. This is in contrast to general alternating automata, for which determinisation incurs a double-exponential size increase. However, we also show that alternating GFG automata can present exponential succinctness compared to both nondeterministic and universal GFG automata. This means that alternating GFG automata can be used to reduce the complexity of solving some games with complex acceptance conditions.

Recognising GFG automata. We give an Exptime upper bound to the problem of deciding whether an alternating parity automaton is GFG, matching the known upper bound for recognising nondeterministic parity GFG automata.

We also study the complexity of deciding "half-GFGness", i.e., whether the nondeterminism (or universality) of an automaton is GFG. This property guarantees that composition with games preserves the winner for one of the players. We show that already on finite words, this problem is PSpace-hard, and it is in Exptime for alternating Büchi automata. This shows that a PTime algorithm for deciding GFGness must exploit the subtle interplay between nondeterminism and universality, and cannot be reduced to checking independently whether each of them is GFG.

shows that GFGness of alternating parity automata is in Exptime, using the determinisation of the previous section. Throughout the paper, we provide high-level proof sketches, with detailed technical developments in the appendix.

Preliminaries

Words and automata. An alphabet Σ is a finite nonempty set of letters. A finite (resp. infinite) word u = u 0 . . . u k ∈ Σ * (resp. w = w 0 w 1 . . . ∈ Σ ω ) is a finite (resp. infinite) sequence of letters from Σ. A language is a set of words, and the empty word is written . We denote a set {i, i + 1, . . . , j} of integers by [i, j].

An alternating word automaton is a tuple A = (Σ, Q, ι, δ, α), where: Σ is an alphabet; Q is a finite nonempty set of states; ι ∈ Q is an initial state; δ : Q × Σ → B + (Q) is a transition function where B + (Q) is the set of positive Boolean formulas (transition conditions) over Q; and α, on which we elaborate below, is either an acceptance condition or a transition labelling on top of which an acceptance condition is defined. For a state q ∈ Q, we denote by A q the automaton that is derived from A by setting its initial state ι to q.

An automaton A is nondeterministic (resp. universal) if all its transition conditions are disjunctions (resp. conjunctions), and it is deterministic if all its transition conditions are just states. We represent the transition function of nondeterministic and universal automata as δ : Q × Σ → 2 Q , and of a deterministic automaton as δ : Q × Σ → Q. A transition of an automaton is a triple (q, a, q ) ∈ Q×Σ×Q, sometimes also written q a -→ q . We denote by δ ⊆ B + (Q) the set of all subformulas of formulas in the image of δ, i.e., all the Boolean formulas that "appear" somewhere in the transition function of A.

Acceptance conditions. There are various acceptance (winning) conditions, defined with respect to the set of transitions1 that a path of A visits infinitely often. (Notice that a transition condition allows for many possible transitions.) We later formally define acceptance of a word w by A in terms of games, and consider a path of A on a word w as a play in that game. For nondeterministic automata, a "run" coincides with a "path". Some of the acceptance conditions are defined on top of a labelling of the transitions rather than directly on the transitions. In particular, in the parity condition, we have α : Q × Σ × Q → Γ, where Γ ⊆ N is a finite set of priorities and a path is accepting if and only if the highest priority seen infinitely often on it is even.

The Büchi and coBüchi conditions are special cases of the parity condition with Γ = {1, 2} and Γ = {0, 1}, respectively. When speaking of Büchi and coBüchi automata, we often refer to α as the set of "accepting transitions", namely the transitions that are mapped to 2 in the Büchi case and to 0 in the coBüchi case. The weak condition is a special case of both the Büchi and coBüchi conditions, in which every path eventually remains in the same priority.

The Rabin and Streett conditions are more involved, yet defined directly on the set T of transitions. A Rabin condition is a set

{(B 1 , G 1 ), (B 2 , G 2 ), . . . , (B k , G k )}, with B i , G i ⊆ T ,
and a path ρ is accepting iff for some i ∈ [1, k], we have that the set inf(ρ) of transitions that are visited infinitely often in ρ satisfies (inf(ρ)

∩ B i = ∅ and inf(ρ) ∩ G i = ∅). A Streett condition is dual: a set {(B 1 , G 1 ), (B 2 , G 2 ), . . . , (B k , G k )}, with B i , G i ⊆ Q, whereby a path ρ is accepting iff for all i ∈ [1, k], we have (inf(ρ) ∩ B i = ∅ or inf(ρ) ∩ G i = ∅).
Sizes and types of automata. The size of A is the maximum of the alphabet size, the number of states, the transition function length, which is the sum of the transition condition lengths over all states and letters, and the acceptance condition's index, which is 1 for weak, Büchi and coBüchi, |Γ| for parity, and k for Rabin and Street.

We sometimes abbreviate automata types by three-letter acronyms in {D, N, U, A} × {F, W, B, C, P, R, S} × {A,W}. The first letter stands for the transition mode, the second for the acceptance condition, and the third indicates that the automaton runs on finite or infinite words. For example, DPW stands for a deterministic parity automaton on infinite words.

Games and strategies. Some of our technical proofs use standard concepts of an arena, a game, a winning strategy, etc. For the sake of completeness, we provide precise mathematical definitions of these objects in Appendix A. Here we will just overview the involved concepts.

First, we work with two-player games of perfect information, where the players are Eve and Adam. These games are played on graphs (called arenas). Most of the considered games are of infinite duration and their winning condition is expressed in terms of the infinite sequences of edges taken during the play. We invoke results of determinacy (one of the players has a winning strategy), as well as of positional determinacy (one of the players has a strategy that depends only on the last position of the play).

R a A R a × A v v a Q = {q 0 , q 1 , q 2 }
δ(q 0 , a) = (q 0 ∧q 1 ) ∨ (q 1 ∧q 2 ) δ(q 1 , a) = q 1 ∧ q 2 δ(q 2 , a) = q 1 ∨ q 2 α(q 0 , a, q 0 ) = 3 α(q 0 , a, q 1 ) = 2 α(q 0 , a, q 2 ) = 6 α(q 1 , a, q 1 ) = 4 α(q 1 , a, q 2 ) = 5

α(q 2 , a, q 1 ) = 3 α(q 2 , a, q 2 ) = 5 v, q 0 v , q 0 v, q 1 v , q 1 v, q 2 v , q 2 v , q 0 , a, (q 0 ∧ q 1 )∨ (q 1 ∧ q 2 ) v , q 0 , a, q 0 ∧ q 1 v , q 0 , a, q 1 ∧ q 2 v , q 1 , a, q 1 ∧ q 2 v , q 2 , a, q 1 ∨ q 2 v , q 0 , a, q 0 v , q 0 , a, q 1 v , q 0 , a, q 2 v , q 1 , a, q 1 v , q 1 , a, q 2 v , q 2 , a, q 1 v , q 2 , a, q 2 ( a , 3 ) ( a , 2 ) (a , 6 ) (a , 4) ( a , 5 ) ( a , 3 ) (a , 5 )
Figure 1 A one-step arena over a letter a ∈ Σ, obtained as a product of a simple arena Ra with the alternating parity automaton A. In this example v is controlled by Eve and v by Adam. The transitions with no label are labelled by . Diamond-shaped positions belong to Eve and square-shaped positions belong to Adam.

q 0 q 0 q 1 q 1 q 2 q 2 q 0 q 0 q 1 q 1 q 2 q 2 q 0 q 0 q 1 q 1 q 2 q 2 q 0 q 0 q 1 q 1 q 2 q 2 Figure 2
The four possible boxes corresponding to Eve's choices in the one-step arena of Figure 1. (All edges should be labelled with a, which we omit for better readability.)

Model-checking games. To represent the semantics of an alternating automaton A, we treat the Boolean formulas that appear in the transition conditions of A as games. More precisely, given a letter a ∈ Σ we represent the transition conditions q → δ(q, a) ∈ B + (Q) as the one-step arena over a (see Figure 1). A play over this arena begins in a state q ∈ Q; then the players go down the formula δ(q, a) with Eve resolving disjunctions and Adam resolving conjunctions; and finally they reach an atom q ∈ Q and the play stops. This means that a play over the one-step arena over a results in a transition of the form q a -→ q . The language L(A) of an alternating automaton A over an alphabet Σ is defined via the model-checking game, defined for an automaton A and a word w = a 0 a 1 a 2 • • • ∈ Σ ω . A configuration of this game is a state q of A and a position i ∈ ω of w, starting at (ι, 0). In the ith round, starting at configuration (q i , i), the players play on the one-step arena from q i over a i , resulting in a transition q i ai -→ q i+1 . The next configuration is (q i+1 , i+1). The acceptance condition of A becomes the winning condition of this game. A accepts w if Eve has a winning strategy in this game.

For technical convenience, we define (in Appendix A) the model-checking game in terms of a synchronised product of the word w (treated as an infinite graph) and the automaton A. Synchronised products turn out to be useful in the analysis of various games presented in this paper and will be used throughout the technical versions of the proofs, in the appendix.

Definition 1. Given an alternating automaton A, we denote by A the dual automaton: it has the same alphabet, set of states, and initial state. Its transition conditions δ A (q, a) are obtained from those of A by replacing each disjunction ∨ with conjunction ∧ and vice versa. Its acceptance condition is the dual of A s condition. (In parity automata, all priorities are increased by 1.) A recognises the complement L(A) c of L(A).

Boxes. Another technical concept that we use is that of boxes (see Figure 2), which describe Eve's local strategies for resolving disjunctions within a transition condition. Consider an alternating automaton A and a letter a ∈ Σ. Moreover, fix a strategy σ of Eve that resolves disjunctions in all the transition conditions δ(q, a) for q ∈ Q. Now, the box of A, a, and σ is a subset of Q × Σ × Q and contains a triple (q, a, q ) iff σ resolves disjunctions of δ(q, a) in such a way that Adam (resolving conjunctions) can reach the atom q . In other words, this box contains (q, a, q ) if there is a play consistent with σ on δ(q, a) that reaches the atom q . We use β to denote single boxes and by B A,a we denote the set of all boxes of A and a, while B A denotes the union a∈Σ B A,a . We give a more formal definition based on synchronised products in the Appendix, see page 15.

Definition 2. Given a sequence of boxes π = b 0 , b 1 , . . . of an automaton A and a path ρ = (q 0 , a 0 , q 1 ), (q 1 , a 1 , q 2 ), . . ., we say that ρ is a path of π if for every i we have (q i , a i , q i+1 ) ∈ b i . The sequence π is said to be universally accepting if every path in π is accepting in A. Intuitively, a sequence of boxes π as above represents a particular positional strategy σ of Eve in the model-checking game over the word w = a 0 a 1 a 2 . . . In that case, a path of π corresponds to a possible play of this game consistent with σ, and the sequence is universally accepting if and only if the strategy is winning.

Good-For-Games Alternating Automata

Good-for-games (GFG) nondeterministic automata are automata in which the nondeterministic choices can be resolved without looking at the future of the word. For example, consider an automaton that consists of a nondeterministic choice between a component that accepts words in which a occurs infinitely often and a component that accepts words in which a occurs finitely often. This automaton accepts all words but is not GFG since the nondeterministic choice of component cannot be resolved without knowing the whole word.

To extend this definition to alternating automata, we must look both at its nondeterminism and universality and require that both can be resolved without knowledge of the future. The following letter games capture this intuition. Definition 3 (Letter games [START_REF] Boker | Good for games automata: From nondeterminism to alternation[END_REF]). Given an alternating automaton A, Eve's letter game proceeds at each turn from a state q of A, starting from the initial state of A, as follows:

Adam chooses a letter a, Adam and Eve play on the one-step arena over a from q to a new state q , where Eve resolves disjunctions and Adam conjunctions. A play of the letter game thus generates a word w and a path ρ of A on w. Eve wins this play if either w / ∈ L(A) or ρ is accepting in A.

Adam's letter game is similar, except that Eve chooses letters and Adam wins if either w ∈ L(A) or the path ρ is rejecting.

A more formal definition is given in Appendix B.

Definition 4 (GFG automata [5]). An automaton A is ∃-GFG if Eve wins her letter game; it is ∀-GFG if Adam wins his letter game. Finally,

A is GFG if it is both ∃-GFG and ∀-GFG.
As shown in [START_REF] Boker | Good for games automata: From nondeterminism to alternation[END_REF]Theorem 8], an automaton A is GFG if and only if it is indeed "good for playing games", in the sense that its product with every game whose winning condition is L(A) preserves the winner of the game.

Example 5. The automaton in Figure 3 accepts the language L of words in which a occurs finitely often and c occurs infinitely often. Here Eve loses her letter game: Adam can play c until Eve takes the transition to the second state, and then play a followed by c ω . Conversely, Eve wins Adam's letter game: her strategy is to play b, take the transition to the second state an keep playing b until Adam takes the transition into the third state, after which she plays c once and then b ω . This automaton is neither ∃-GFG nor ∀-GFG, and taking its product with games with L as winning condition does not preserve the winner of the game.

In contrast, the automaton in Figure 4 is ∀-GFG but not ∃-GFG. Indeed, Adam's winning strategy in his letter game is to resolve the conjunction from the middle state by always moving to the right-hand state when Eve plays b. This forces Eve to choose between playing c infinitely many times (in which case, the word is in the language) or letting Adam build a rejecting run. Taking its product with one-player games with winning condition L preserves the winner whenever Eve is the player controlling all positions. However, this is not the case for one-player games where Adam is the sole player.

Alternating GFG vs. Nondeterministic and Universal Ones

We show in this section that alternating GFG automata can be more succinct than both nondeterministic and universal GFG automata. Lemma 6. There is a family (C n ) n∈N of alternating GFG {0, 1, 2}-parity automata of size linear in n over a fixed alphabet, such that every nondeterministic GFG parity automaton and universal GFG parity automaton for L(C n ) is of size 2 Ω(n) .

Proof. From [START_REF] Kuperberg | On determinisation of good-for-games automata[END_REF], there is a family (A n ) n∈N of GFG-NCWs with n states over a fixed alphabet Σ, such that every DPW for L n = L(A n ) is of size 2 Ω(n) . For every n ∈ N, let B n be the dual of A n , so B n is a UBW accepting L n . We build an APW C n over Σ of size linear in n, by setting its initial state to move to the initial state of A n when reading the letter a ∈ Σ and to the initial state of B n when reading the letter b ∈ Σ. The acceptance condition of C n is a parity condition with priorities {0, 1, 2}: accepting transitions of A n are assigned priority 0, and accepting transitions of B n priority 2. Other transitions have priority 1.

The automaton C n is represented below:

Observe that L(C n ) = aL n ∪bL n , and that C n is GFG: its initial state has only deterministic transitions, and over the A n and B n components, the strategy to resolve the nondeterminism and universality, respectively, follows the strategy to resolve the nondeterminism of A n , which is guaranteed due to A n 's GFGness.

Consider a GFG UPW E n for L(C n ), and let q be a state to which E n moves when reading a, according to some strategy that witnesses E n 's GFGness. Then E q n is a GFG UPW for L n . Its dual is therefore a GFG NPW E n for L n .

Since A n is a GFG NPW for L n , by [START_REF] Boker | Nondeterminism in the presence of a diverse or unknown future[END_REF]Theorem 4] we obtain a DPW for L n of size |A n ||E n |. By choice of L n , this DPW must be of size 2 Ω(n) , and since A n is of size n, it follows that E n , and hence E n , must be of size 2 Ω(n) . By a symmetric argument, every GFG NPW for L(C n ) must also be of size 2 Ω(n) .

Informally, the language L n above describes a set of threads, of which at least one eventually satisfies a safety property. Then, the above construction can be understood as describing a property of reactive systems where, depending on the input, the system guarantees either that there is a thread that eventually satisfies a safety property, or that all threads satisfy a liveness (Büchi) property. The GFG alternating automaton can then be used to solve in polynomial time games with such languages as winning condition, for example in the context of synthesis: the product of the game arena and the alternating automaton for L n is a parity game with 3 priorities with the same winner as the original game. In contrast, a DPW, GFG NPW and GFG UPW for the same language would all be exponentially larger.

Deciding Half-GFGness

In order to decide GFGness, it is enough to be able to decide the ∃-GFG property on the automaton and its dual. A natural first approach is therefore to study the complexity of deciding whether an APW is ∃-GFG. Yet, we will show that already on finite words, this problem is PSpace-hard, while we conjecture that deciding GFGness is in PTime.

Lemma 7.

Deciding whether an AFA is ∃-GFG is PSpace-hard.

Proof. We reduce from NFA universality: starting from an NFA A, we build an AFA B based on the dual of A, with an additional non-GFG choice to be resolved by Eve. This AFA B is ∃-GFG if and only if L(B) = ∅, which happens if and only if L(A) = Σ * . We crucially use the fact that B is not necessarily ∀-GFG.

Let A be an NFA over an alphabet Σ = {a, b} and Ā its dual. We want to check whether L(A) = Σ * . We build an AFA B, as depicted below, by first making Eve guess the second letter. If her guess is wrong, the automaton proceeds to a rejecting sink state ⊥. Otherwise, it proceeds to the initial state of Ā. The size of B is linear in the size of A.

If L( Ā) = ∅, then L(B) = ∅, so B is trivially ∃-GFG.
However, if there is some u ∈ L( Ā), then Adam has a winning strategy in Eve's letter game on B. This strategy consists of playing a, then playing the letter that brings Eve to ⊥, and finally playing u. The resulting word is in L(B) = Σ 2 L(A), so this witnesses that B is not ∃-GFG. We obtain that

L(A) = Σ * ⇔ L( Ā) = ∅ ⇔ B is ∃-GFG, which is the wanted reduction.
For Büchi automata, and so in particular for finite words, we can give an Exptime algorithm for this problem.

Lemma 8. Deciding whether an ABW is ∃-GFG is in Exptime.

Proof. It is shown in [START_REF] Boker | Good for games automata: From nondeterminism to alternation[END_REF]Lemma 23] that removing alternation from an ABW A using the breakpoint construction [START_REF] Miyano | Alternating finite automata on ω-words[END_REF] yields an NBW B such that if A is ∃-GFG then B is GFG. Moreover, the converse also holds: if B is GFG then A is ∃-GFG, since playing Eve's letter game in B is more difficult for Eve than playing it in A. This means that starting from an ABW A, we can build an exponential size NBW B via breakpoint construction, and test whether B is GFG via the algorithm from [START_REF] Bagnol | Büchi good-for-games automata are efficiently recognizable[END_REF], in time polynomial with respect to B. Overall, this yields an Exptime algorithm deciding whether A is ∃-GFG.

Determinisation of Alternating GFG Parity Automata

In this section we provide a procedure that, given an alternating GFG parity automaton, produces an equivalent deterministic parity automaton with single-exponentially many states.

To do so, we first provide an alternation-removal procedure that preserves GFG status. Then, we apply this procedure to both the input automaton and its complement and use the GFG strategies in these two automata to determinise the input automaton. Our proofs, in Appendix C, rely on some analysis of when GFG strategies can use the history of the word, rather than the full history of the play (which also includes the choices of how to resolve the nondeterminism and universality), and on the memoryless determinacy of parity games.

Our method for going from alternating to nondeterministic automata is similar to that of Dax and Klaedtke [START_REF] Dax | Alternation elimination by complementation[END_REF]: they take a nondeterministic automaton that recognises the universally-accepting words in (B A ) ω and add nondeterminism that upon reading a letter a ∈ Σ chooses a box in B A over a. Yet in our approach, in order to guarantee that the outcome preserves GFGness, the intermediate automaton is deterministic.

Alternation Removal in GFG Parity Automata

Theorem 9. Consider an alternating parity automaton A with n states and index k. There exists a nondeterministic parity automaton box(A) with 2 O(nk log nk) states that is equivalent to A such that if A is GFG then box(A) is also GFG.

In Section 5, where we discuss decision procedures, we will show that box(A) is GFG exactly when A is ∃-GFG. For now, the rest of this section is devoted to the proof of Theorem 9, of which a detailed version can be found in Appendix C.2.

Lemma 10. Consider an alternating parity automaton

A with n states and index k. Then there exists a deterministic parity automaton B with 2 O(nk log nk) states over the alphabet B A that recognises the set of universally-accepting words for A. If A is a Büchi automaton, then B can also be taken as Büchi, and in general the parity index of the automaton B is linear in the number of transitions of A.

Proof sketch. We first construct a nondeterministic parity (resp. coBüchi) automaton over the alphabet B A that recognises the complement of the set of universally-accepting words for A. This automaton is easy to build: it guesses a path that is not accepting, and has the dual acceptance condition to A. We then obtain the automaton B by determinising and complementing this automaton.

We now build the automaton box(A) of Theorem 9. It is the same as the automaton B of Lemma 10, except that the alphabet is Σ and the transition function is defined as follows: For every state p of B and a ∈ Σ, we have δ box(A) (p, a) := β∈B (A,a) δ B (p, β).

In other words, the automaton box(A) reads a letter a, nondeterministically guesses a box β ∈ B A,a , and follows the transition of B over β. Thus, the runs of box(A) over a word w = w 0 w 1 w 2 • • • ∈ Σ ω are in bijection with sequences of boxes (β i ) i∈N such that β i ∈ B A,wi for all i ∈ N.

Fix an infinite word w ∈ Σ ω . Our aim is to prove that w ∈ L(A) ⇔ w ∈ L(box(A)).

Lemma 11. There exists a bijection between positional strategies of Eve in the acceptance game of A over w and runs of box(A) over w. Moreover, a strategy is winning if and only if the corresponding run is accepting. Thus L(A) = L(box(A)).

Remark 12. The above alternation-removal procedure also extends to alternating Rabin automata but fails for alternating Streett automata A: since Streett games are not positionally determined for Eve, the acceptance game of A over a word w is not positionally determined for Eve.

Lemma 13. For an alternating ∃-GFG parity automaton A, the automaton box(A) is GFG.

Intuitively, this is because the construction of box(A) preserves the nondeterminism of A.

Single-Exponential Determinisation

The aim of this section is to prove the following determinisation theorem; see Appendix C.3 for a detailed proof. Theorem 14. If A is an alternating parity GFG automaton then there exists a deterministic parity automaton D that recognises the same language and has size at most exponential in the size of A. Moreover, the parity index of D is the same as that of A.

Remark 15. Theorem 9 and [3, Theorem 4], which uses an NRW-GFG and its complement NRW-GFG to obtain a DRW, together give an exponential deterministic parity automaton for L(A). However, the index of A might not be preserved. On the other hand, from [5, Theorem 19] we know that there exists a deterministic parity automaton equivalent to A with the same index, but it might have more than exponentially many states. Here we are able to guarantee both the preservation of the index and an exponential upper bound on the size of the deterministic automaton.

Observe that Theorem 9 can be applied both to A and its dual. Therefore, we can fix a pair of nondeterministic GFG parity automata box(A) and box( Ā) that recognise L(A) and L(A) c respectively and are both of size exponential in A. We use the automata A, box(A), and box( Ā) to construct two auxiliary games G(A) and G (A) .

The game G(A) proceeds from a configuration consisting of a pair (p, q) of states from box( Ā) and A respectively, starting from their initial states, as follows:

Adam chooses a letter a ∈ Σ; Eve chooses a transition p a -→ p in box( Ā); Eve and Adam play on the one-step arena over a from q to a new state q .

A play in G(A) consists of a run ρ in box( Ā) and a path ρ in A. It is winning for Eve if either ρ is accepting in box( Ā) (in which case w / ∈ L(A)), or ρ is accepting in A.

If A is ∃-GFG and box( Ā) is GFG, Eve has a winning strategy in G(A) consisting of building a run in box( Ā) using her GFG strategy in box( Ā) and a path in A using her ∃-GFG strategy in A. This guarantees that if w ∈ L(A) then the path in A is accepting, and otherwise the run in box( Ā) is accepting.

We then argue that as the winning condition of G(A) is a Rabin condition, Eve also has a winning strategy that is positional in A, that is, which only depends on the history of the word and the current position. (Interestingly, the question of whether Eve can resolve the nondeterminism in a class of alternating GFG automata with only the knowledge of the word read so far does not tightly correspond to whether the acceptance condition of this class is memoryless. For example, it does hold for the generalised-Büchi condition, though it is not memoryless.) See Appendix C for details.

Remark 16. There is some magic here: both the GFG strategies of Eve in A and in box( Ā) may require exponential memory, yet, when she needs to satisfy the disjunction of the two conditions, no more memory is needed. In a sense, the states of A provide the memory for box( Ā) and the states of box( Ā) provide the memory for A.

The game G (A) is similar, except that Adam is given control of box(A) and Eve is in charge of letters. This time Adam wins a play, consisting of a run of box(A) and a path in A, if either the path of A is rejecting or the run of box(A) is accepting.

Accordingly, if A is GFG, then he can win by using the ∃-GFG strategy in box(A) and the ∀-GFG strategy in A. Then if w ∈ L(A), the run in box(A) is accepting, and otherwise the path of A is rejecting. As before, he also has a positional winning strategy in G (A).

We are now ready to build the deterministic automaton from a GFG APW A, using positional winning strategies σ and τ for Eve and Adam in G(A) and G (A), respectively.

Let D be the automaton with states of the form (q, p 1 , p 2 ), with q a state of A, p 1 a state of box(A) and p 2 a state of box( Ā). A transition of D over a moves to (q , p 1 , p 2 ) such that moving from (q, p 1 ) to (q , p 1 ) is consistent with τ ; and moving from (q, p 2 ) to (q , p 2 ) is consistent with σ. The acceptance condition of D is inherited from A.

Lemma 17. For a GFG APW A and D built as above, L(A) = L(D).

Remark 18. To extend this construction to an alternating GFG Rabin automaton A, we would need to remove alternations from both A and its dual while preserving GFGness. However, the dual is a Streett automaton, for which we cannot invoke positional determinacy.

Deciding GFGness of Alternating Automata

We use the development of the last section to show that deciding whether an APW is GFG is in Exptime. This matches the best known upper bound for the same problem on NPW.

The main result of this section is the following theorem; its proof is in Appendix D.1.

Theorem 19. There exists an Exptime algorithm that takes as input an alternating parity automaton A and decides whether A is GFG.

The idea is to construct the (exponential size) NPWs box(A) and box( Ā) for L(A) and L(A) c respectively, which are GFG if and only if A is ∃-GFG and ∀-GFG respectively. Then, it remains to check whether both are indeed GFG. Since we don't have a polynomial procedure to check this, instead, we will build a game which Eve wins if and only if both are indeed GFG, and which we can solve in exponential time with respect to the size of A.

First, we observe the following reciprocal of Lemma 13.

Lemma 20. If box(A) is GFG then

A is ∃-GFG.
Proof. Assume that box(A) is GFG and consider a strategy witnessing this. Such a strategy can be easily turned into a function σ : Σ + → B A that, given a word w ∈ L(A) produces a universally accepting word of boxes of A. Now, due to the definition of a box, each such box defines a positional strategy of Eve in the respective one-step game. This allows us to construct a winning strategy of Eve in the letter game over A.

Thus, A is GFG if and only if both box(A) and box( Ā) are GFG. To decide this, we consider a game G where Adam plays letters and Eve produces runs of the automata box(A) and box( Ā) in parallel. The winning condition of G requires that at least one of the constructed runs must be accepting. Now, each sequence of letters given by Adam belongs either to the language of box(A) or to box( Ā) and therefore, a winning strategy of Eve in G must comprise of two strategies witnessing GFGness of both box(A) and box( Ā). Dually, if both box(A) and box( Ā) are GFG then Eve wins G by playing the two strategies in parallel.

It remains to show that G is solvable in Exptime. Its winning condition is a disjunction of parity conditions, with index linear in the number of transitions of A. This winning condition is recognised by a deterministic parity automaton of exponential size with polynomial index. To solve G , we take its product with this deterministic automaton that recognises its winning condition, and solve the resulting parity game with an algorithm that is polynomial in the size of the game whenever, like here, the number of priorities is logarithmic in the size of the game, for instance [START_REF] Cristian S Calude | Deciding parity games in quasipolynomial time[END_REF]. Details of this construction and its complexity are in Appendix D.1.

Conclusions

The results obtained in this work shed new light on where alternating GFG automata resemble nondeterministic ones, and where they differ. Overall, our results show that allowing GFG alternations add succinctness without significantly increasing the complexity of determinisation nor decision procedures.

In particular, we show that alternating parity GFG automata can be exponentially more succinct than any equivalent nondeterministic GFG automata, yet this succinctness does not become double exponential when compared to deterministic automata, answering a question from [START_REF] Boker | Good for games automata: From nondeterminism to alternation[END_REF]. Some further succinctness problems are left open here, such as the possibility of a doubly exponential gap between alternating GFG automata of stronger acceptance conditions and deterministic ones, as well as between ∃-GFG parity automata and deterministic ones.

We also show that the interplay between the two players can be used to decide whether an automaton is GFG without deciding ∃-GFG and ∀-GFG separately, yielding an Exptime algorithm. This matches the current algorithms for deciding GFGness on non-deterministic automata. Bagnol and Kuperberg conjectured that GFGness is PTime decidable for nondeterministic parity automata of fixed index [START_REF] Bagnol | Büchi good-for-games automata are efficiently recognizable[END_REF]; we extend this conjecture to alternating automata.

It then becomes interesting to ask how to build an alternating automaton GFG. Indeed, Henzinger and Piterman [START_REF] Henzinger | Solving games without determinization[END_REF] proposed a transformation of nondeterministic automata into GFG automata, which, despite in some cases leading to a deterministic automaton, is, conceptually, a much simpler procedure than determinisation. Indeed, in many examples of non-GFG automata, adding transitions suffices to obtain a GFG one. We leave finding such a procedure for alternating automata as future work.

Along a play, the memory starts with m 0 , and is updated along every transition according to upd. The general notion of strategy corresponds to M = (V • X) * , and positional strategies correspond to M being a singleton. A player has a finite-memory winning strategy if there exists a winning strategy using a finite memory set M . Proposition 21. Let G and G be two Σ-games with the same winning condition, such that the unfoldings of G and G are isomorphic. Then Eve has a winning strategy in G if and only if she has a winning strategy in G . Proposition 22 ([13]). Rabin games are positionally determined for Eve. (If Eve has a winning strategy then she has a positional winning strategy.)

Definition 23 (Synchronised product). The synchronised product R × A of a (partial) Σ-arena R = (V, X, V E , V A
) and an alternating automaton A = (Σ, Q, ι, δ, α) with a set of transitions T and labelling α : T → Γ is a (partial) Σ×Γ-arena defined as follows. Its set of positions is

(V × Q) ∪ (V × Q × Σ × δ)
, and its transitions are defined by: (v, q), , (v , q, a, δ(q, a))

for (v, q) ∈ V × Q and v, a, v ∈ X; (v, q), , (v , q) for (v, q) ∈ V × Q and v, , v ∈ X; (v, q, a, b), , (v, q, a, b i ) for (v, q, a, b) ∈ V × Q × Σ × δ with b = b 1 ∨b 2 or b = b 1
∧b 2 and i = 1, 2; (v, q, a, q ), a, α(q, a, q ) , (v, q ) for (v, q, a, q ) ∈ V × Q × Σ × δ with q ∈ Q. The positions belonging to Eve are of the form (v, q) where v ∈ V E and of the form (v, q, a, b 1 ∨b 2 ). The remaining ones belong to Adam. If R has an initial position v ι then the initial position of the product is (v ι , ι).

We implicitly assume that the arena only contains vertices that are reachable from V × Q. (They need not be reachable from an initial position of R and an initial state of A, but from some position of R and state of A.)

We will sometimes consider longer products, like (R × A 1 ) × A 2 , where R is a Σ-arena and both automata A 1 and A 2 are over the alphabet Σ. Assume that A 1 and A 2 have transitions labelled in sets Γ 1 and Γ 2 respectively. Notice that in that case the arena R × A 1 is formally a Σ × Γ 1 -arena. Thus, to make the above formula precise, we treat the automaton A 2 as an automaton over the alphabet Σ × Γ 1 and assume that it ignores the second component of the letters read.

One-step arenas. For a letter a ∈ Σ, we denote by R a a partial Σ-arena consisting of two vertices v and v (it does not matter which of the players controls them), and one transition (v, a, v ). Then, for an automaton A = (Σ, Q, ι, δ, α), the product R a × A is a partial arena, in which the players should resolve their choices in the formulas δ(q, a) for all the possible states q ∈ Q. We call it the one-step arena of A over a. Such an arena contains one position of the form (v, q) for each state q ∈ Q; a set of non-terminal positions of the form (v , q, a, ψ) for some q ∈ Q and ψ ∈ δ; and one terminal position of the form (v , q) for each state q ∈ Q. (See Figure 1.) Boxes. In the later exposition, we will be interested in the combinatorial structure of possible strategies of Eve over one-step arenas R a × A. For a positional strategy σ of Eve in a game of the form R a × A, we define the box of A, a, and σ, denoted by β(A, a, σ), as the relation that is a subset of Q × Σ × Q and contains a triple (q, a, q ) iff there exists a play in R a × A that is consistent with σ, starting in (v, q) and ending in (v , q ). We further define for every a ∈ Σ, the set B (A,a) = {β(A, a, σ) | σ is a positional strategy of Eve}. Finally, let

B A := a∈Σ B (A,a) . Notice that |B A | ≤ 2 |Q×Σ×Q| .
When speaking of an arbitrary box, we mean any non-empty relation β ⊆ Q × Σ × Q where all the letters a appearing on the middle component are equal.

Figure 2 represents B (A,a) for the automaton A of Figure 1: Since there are two binary-choice positions of Eve in the corresponding one-step arena, there are four distinct positional strategies of Eve, which give the four possible boxes. They correspond to Eve choosing respectively LL, LR, RL, RR, where L stands for a left choice and R for a right choice in each of her two binary-choice positions.

Proposition 24. Consider a letter a and an automaton A with states Q and transition function δ. Then there is a bijection between B (A,a) and the positional strategies of Eve in the one-step arena of A and a.

Acceptance of a word by an automaton. We define the acceptance directly in terms of the model-checking (acceptance/membership) game, which happens to be exactly the product of the automaton with a path-like arena describing the input word. More precisely, given a word w ∈ Σ ω , the model-checking game is defined as the product R w × A, where the arena R w consists of an infinite path ω, of which all positions belong to Eve (although it does not matter); the transitions are of the form i, w i , i+1 ; the initial position is 0; and the winning condition is based on the winning condition of A (the Σ-component of the labels is ignored). We say that A accepts w if Eve has a winning strategy in the model-checking game R w × A. The language of an automaton A, denoted by L(A), is the set of words that it accepts (recognises).

Notice that for each i ∈ N, the sub-arena of R w × A with positions in

{i} × Q ∪ {i+1} × Q×Σ×B + (Q) ∪ {i+1} × Q
is isomorphic to the one-step arena of A over w i .

B Appendix of Section 3

Definition 25 (A formalisation of Definition 3). Let R A,Σ be the Σ-arena consisting of a single position v that belongs to Adam and the set of transitions X of the form (v, a, v) for each letter a ∈ Σ (see Figure 5). The arena R E,Σ is the same except that v belongs to Eve. Notice that the products R A,Σ × A and R E,Σ × A are both labelled by Σ × Γ, where Σ is the alphabet of A and Γ is A's labelling, on top of which its acceptance condition is defined. Thus, the winning condition of games defined on these arenas can depend on a sequence of labels of the form (a i , γ i ) i∈N . Then, Eve's letter game is played over R A,Σ × A, where Eve wins if:

(a i ) i∈N / ∈ L(A) or the sequence (γ i ) i∈N satisfies the acceptance condition of A.
Dually, Adam's letter game is played over R E,Σ × A, where Adam wins if:

(a i ) i∈N ∈ L(A) or the sequence (γ i ) i∈N violates the acceptance condition of A.

C Appendix of Section 4

This section provides the technical details of the determinisation procedure in Section 4. We start with some technical analysis of the types of histories needed to win letter games.

C.1 Good for Games Automata: Required Histories

We begin by considering an expanded letter game. This will allow us to use a form of positional determinacy in letter games.

R A,Σ R * A,Σ

Figure 5

The arenas R A,Σ and R * A,Σ , allowing Adam to choose an arbitrary sequence of letters. We define Eve's letter game for an automaton A over the product of R A,Σ × A, and her expanded letter game over R * A,Σ × A; She wins a play if the word generated by Adam is not in L(A) or the path generated by her (resolving A's nondeterminism) and by Adam (resolving A's universality) satisfies A's acceptance condition.

Expanded letter games. The definition of the letter games (Definition 3) has the important advantage of being defined over a finite-arena. Yet, as a result, these games generally do not allow for positional determinacy.

We provide below an expanded variant of the letter game that will have same unfolding as the original one, while being defined over an infinite arena. This will allow Eve to have positional determinacy in these games for Rabin automata.

Let R * A,Σ be the Σ-arena with the set of positions V = Σ * , all belonging to Adam, and the set of transitions X of the form w, a, w • a for each word w ∈ Σ * and letter a ∈ Σ (see Figure 5). The initial position of this arena is . The arena R * E,Σ is the same, except that all the positions belong to Eve. We define Eve's expanded letter game over R * A,Σ × A and Adam's expanded letter game over R * E,Σ × A with the same winning conditions as in their (non expanded) variants. The following follows directly from Proposition 21.

Proposition 26. For every automaton A, the expanded letter games for A have the same winners as the (standard) letter games for A.

History Requirement. Although R *

A,Σ and R * E,Σ are trees, the arenas of the expanded letter games are directed acyclic graphs as there can exist two distinct paths from the initial position to a given position (w, q). Thus, a priori, a winning strategy of a player of such a game might need some history of a play. However, as expressed by the following theorem, it is not the case. Theorem 27. If A is a Rabin (or parity) automaton then Eve's expanded letter game is positionally determined for Eve.

Proof. We will show that the winning condition of this game can be represented as a Rabin condition and invoke Proposition 22. Let D be a deterministic parity automaton recognising the complement of the language L(A), for a Rabin automaton A over the alphabet Σ. Let Ω : Q D → N be the priority assignment of D (without loss of generality we can assume that the states of D bear priorities).

Consider the arena R * A,Σ that is derived from the arena R * A,Σ by adding to transitions priorities according to the deterministic of runs of D , that is, by changing the labelling of every transition w, a, w • a to w, (Ω D (q), a), w • a , where a ∈ Σ and q is the state of D reached after reading the word w from the initial state of D .

Consider the product R * A,Σ × A, in which for A s transitions we ignore these additional labels. The labels of that product are now of the form ( , a, γ), where ∈ N is a priority of D , a ∈ Σ, and γ ∈ Γ is a label of A. Notice that when one forgets about the first coordinate of the label, the game is equal to R * A,Σ × A. Moreover, given a sequence of labels ( i , a i , γ i ) i∈N , by the choice of D , we know that (a i ) i∈N / ∈ L(A) if and only if the sequence ( i ) i∈N satisfies the parity condition.

Define the game G over R * A,Σ × A, in which Eve wins a play labelled by ( i , a i , γ i ) i∈N if ( i ) i∈N satisfies the parity condition of D or (γ i ) i∈N satisfies the Rabin condition of A.

Notice that both disjuncts above can be written as Rabin conditions and therefore G is positionally determined for Eve. Moreover, the choice of D guarantees that the new winning condition is equivalent to Eve's condition in her expanded letter game on A-the same plays are winning for Eve in G and her expanded letter game on A. Since the structure of the game is also preserved, it means that Eve's expanded letter game on A is positionally determined for Eve.

Remark 28. Dually, Adam's expanded letter game for a Streett automaton is positionally determined for Adam.

As a consequence of Theorem 27, for alternating ∃-GFG Rabin automata, a strategy for Eve to resolve the nondeterminism may ignore the history of the play, and only consider the history of the word read, as is the case for nondeterministic GFG automata.

We will now argue that Eve's positional strategy σ in the expanded letter game on an alternating automaton A can be represented as a function σ : Σ + → B A that assigns to each word wa a box β wa ∈ B (A,a) . Indeed, let (w • a) ∈ Σ + and let V wa be the set of positions of R * A,Σ × A of the form (w, q), (w • a, q, a, b), or (w • a, q) for q ∈ Q and b ∈ B + (Q). Observe that the partial arena of R * A,Σ × A restricted to V wa is isomorphic to the one-step arena R a × A. Thus, σ provides a positional strategy over this arena, which by Proposition 24 can be encoded as a box β wa . More formally, let β wa contain (q, a, q ), if there is a play consistent with σ that visits both the positions (w, q) and then (wa, q ). Then, in the next lemma we show that if σ is also winning, then the sequences of boxes β wa only has accepting paths. Definition 29. Consider an automaton A with states Q and initial state ι, and an infinite word u = β 0 , β 1 , . . . ∈ (B A ) ω . We say that a sequence of transitions ρ = (q i , a i , q i+1 ) i∈N is a path of u if q 0 = ι and for every i ∈ N, we have (q i , a i q i+1 ) ∈ β i . The word u is universally accepting for A if each of its paths satisfies the acceptance condition of A.

Lemma 30. Given an alternating ∃-GFG Rabin automaton A, there is a positional strategy σ in her expanded letter game on A such that for every word w ∈ L(A) the sequence of boxes u = β 0 , β 1 , . . . ∈ (B A ) ω defined as β i = σ(w i+1 ) is universally accepting for A.

Proof. Consider words w and u as above. Let ρ = (q i , a i , q i+1 ) i∈N be a path of u. Since the strategy σ is positional, the definition of σ(w i+1 ) implies that there exists a single play of

q 0 q 1 q 2 q 3 q 4 q 5 ∧ ∨ t 1 t 2 t 4 t 5
Acceptance condition: (Finitely often t 1 or Infinitely often t 4 ) and (Finitely often t 2 or Infinitely often t 5 )

Figure 6 A GFG ASW over a singleton alphabet, for which Eve's ∃-GFG strategy cannot only remember the prefix of the word read so far, but also some history about the visited states.

the expanded letter game that visits all the positions of the form (w i , q i ) for i ∈ N . Since w ∈ L(A), the winning condition of the expanded letter game guarantees that the path ρ must be accepting.

Observe that the above arguments do not hold for alternating GFG Streett automata: Since Streett games are not positionally determined for Eve, Eve's expanded letter game for a Streett automaton is not positionally determined for Eve (an analogous of Theorem 27 does not hold). Furthermore, we provide in Figure 6 an example of an alternating GFG Streett automaton, in which Eve cannot resolve her nondeterminism only according to the history of the word read. Proof. Consider the ASW depicted in Figure 6. It is ∃-GFG, as witnessed by the strategy that chooses the transition t 4 in q 3 if the last visited state was q 1 and t 5 otherwise. Yet, there is no strategy that only remembers the word read so far, as this only gives the length of the word, and cannot help in determining whether the path visited q 1 or q 2 .

C.2 Alternation Removal in GFG Parity Automata

This section presents the proof of the following theorem: Theorem 9. Consider an alternating parity automaton A with n states and index k. There exists a nondeterministic parity automaton box(A) with 2 O(nk log nk) states that is equivalent to A such that if A is GFG then box(A) is also GFG. Lemma 10. Consider an alternating parity automaton A with n states and index k. Then there exists a deterministic parity automaton B with 2 O(nk log nk) states over the alphabet B A that recognises the set of universally-accepting words for A. If A is a Büchi automaton, then B can also be taken as Büchi, and in general the parity index of the automaton B is linear in the number of transitions of A.

Proof. Notice that it is easy to construct a nondeterministic parity automaton S over the alphabet B A that recognises the complement of the set of universally-accepting words for A-it is enough to guess a path that is not accepting, and have the acceptance condition that is the dual of A's condition. If A is a Büchi automaton, then S is a coBüchi one. Formally, for an alternating parity (resp. Büchi) automaton A = (Σ, Q, ι, δ, α), we define the nondeterministic parity (resp. coBüchi) automaton S = (B A , Q, ι, δ S , α), where α is the dual of α and δ S is defined as follows. For every states q, q ∈ Q and box β ∈ B A , we have q ∈ δ S (q, β) iff q a -→ q ∈ β for some a. Now, one can translate S to an equivalent deterministic parity automaton B with 2 O(nk log nk) states [START_REF] Piterman | From nondeterministic Büchi and Streett automata to deterministic parity automata[END_REF] and then complement the acceptance condition of B , getting the required automaton B.

Since nondeterministic coBüchi automata can be determinised into deterministic coBüchi automata, if A is Büchi, so is B. In general, the parity index of the automaton B is linear in the number of transitions of A.

We now proceed to the construction of the automaton box(A) of Theorem 9. It is the same as the automaton B of Lemma 10, except that the alphabet is Σ and the transition function is defined as follows: For every state p of box(A) and a ∈ Σ, we have

δ box(A) (p, a) := ∪ β∈B (A,a) δ B (p, β).
In other words, the automaton box(A) reads a letter a, nondeterministically guesses a box β ∈ B A,a , and follows the transition of B over β. Thus, the runs of box(A) over a word w ∈ Σ ω are in bijection between sequences of boxes (β i ) i∈N such that β i ∈ B A,wi for i ∈ N .

Fix an infinite word w ∈ Σ ω . Our aim is to prove that w ∈ L(A) ⇔ w ∈ L(box(A)).

Lemma 11. There exists a bijection between positional strategies of Eve in the acceptance game of A over w and runs of box(A) over w. Moreover, a strategy is winning if and only if the corresponding run is accepting. Thus L(A) = L(box(A)).

Proof. Consider a run of box(A) over w, and observe that it corresponds to a sequence of boxes β 0 , . . .. Notice that each box β i corresponds to Eve's choices in A over w i , and therefore provides a positional strategy for Eve in the one-step arena R wi × A. The sequence of these choices provides a positional strategy for Eve in R w × A.

Dually, given a positional strategy for Eve in R w × A, one can extract a sequence of strategies for Eve in the one-step arenas R wi × A, and each of them corresponds to a box β i . Proposition 24 shows that each path in β 0 , . . . corresponds to a play consistent with the constructed strategy and vice versa: each play gives rise to a path. Now, a run is accepting if and only if the sequence of boxes is universally accepting, which means exactly that all the plays consistent with the corresponding strategy are winning.

We now show that the automaton box(A) is also GFG. Lemma 13. For an alternating ∃-GFG parity automaton A, the automaton box(A) is GFG.

Proof. Let σ be a positional winning strategy for Eve in her expanded letter game for A (over the arena R * A,Σ × A). The proof is based on the construction of the function σ : Σ + → B A , see the paragraph before Definition 29.

Consider the following way of resolving the nondeterminism of box(A): after reading w ∈ Σ * , when the next letter a ∈ Σ is provided, the automaton moves to the state δ B (p, β wa ) where β wa = σ (wa). Consider an infinite word w ∈ L(A) and let β 0 , . . . be the sequence of boxes used to construct the run of box(A) over w. Lemma 30 implies that this sequence is universally accepting and therefore, the constructed run of B must also be accepting.

C.3 Single-Exponential Determinisation of Alternating Parity GFG Automata

The aim of this section is to prove the following determinisation theorem.

Theorem 14. If

A is an alternating parity GFG automaton then there exists a deterministic parity automaton D that recognises the same language and has size at most exponential in the size of A. Moreover, the parity index of D is the same as that of A.

First consider the synchronised product R A,Σ × box( Ā), which is a game with labels of the form Σ × Γ box( Ā) , where Γ box( Ā) is the parity condition of box( Ā). Now, we can treat the automaton A as an automaton over the alphabet Σ × Γ box( Ā) that just ignores the second component of the given letter. Thus, we can define a game G(A) = R A,Σ × box( Ā) × A.

Notice that G(A) is naturally divided into rounds, between two consecutive positions of the form (v, p, q), where v is the unique position of R A,Σ , p is a state of box( Ā), and q is a state of A. Such a round, starting in (v, p, q), consists of first Adam choosing a letter a; then Eve resolving nondeterminism of box( Ā) from p over a; and then both players playing the game corresponding to the transition condition δ(q, a) of A.

Let the winning condition of G(A) say that either the sequence of transitions of box( Ā) is accepting or the sequence of transitions of A is accepting. Since A is ∃-GFG and box( Ā) is GFG, we know that Eve has a winning strategy in G(A): she just plays her GFG strategies in both automata and is guaranteed to win whether the word produced by Adam is in L(A) or L(box( Ā)).

As the winning condition of G(A) is a disjunction of two Rabin conditions, Eve has a positional winning strategy. Fix such a strategy σ. Now do the same with A and box(A) for Adam: define G (A) as R E,Σ × box(A) × A, where box(A) is the automaton box(A) where the transitions are turned from nondeterministic to universal, i.e, we replace ∨ with ∧.

Again, in a round of G (A) from a position (v, p, q): Eve plays a letter a; Adam resolves nondeterminism of box(A) (i.e., the universality in its dual); then they both resolve the choices in A. Let Adam win G if either the play of A is rejecting or the run of box(A) is accepting. Again we can ensure that Adam has a winning strategy in G (A), because both automata are GFG: he uses the GFG strategy of box(A) and the ∀-GFG strategy over A. If the word given by Eve belongs to L(A) then Adam wins by producing an accepting run of box(A), otherwise he wins by refuting an accepting run of A. Let τ be his positional winning strategy in that game.

We are now ready to build the deterministic automaton from a GFG APW A, using positional winning strategies σ and τ for Eve and Adam in G (A) and G(A), respectively.

Let D be the automaton with states of the form (q, p 1 , p 2 ), with q a state of A, p a state of box(A) and p a state of box( Ā). A transition of D over a moves to (q , p 1 , p 2 ) such that ((q, p 1 ), (q , p 1 )) is consistent with τ and ((q, p 2 ), (q , p 2 )) is consistent with σ. In other words, when reading a letter a in such a state, the following computations are performed: 1. We simulate the choices made by σ in G (A) upon obtaining a from Adam. This way we know how to resolve nondeterminism of box( Ā) and what to do with disjunctions inside A. 2. We simulate the choices made by τ in G(A) upon obtaining a from Eve. This way we know how to resolve nondeterminism in box(A) and what to do with conjunctions of A.

3.

In the end we proceed to a new state of A and resolved nondeterminism of both box(A) and box( Ā).

The acceptance condition of D is inherited from A.

Lemma 17. For a GFG APW A and D built as above, L(A) = L(D).

Proof. Take a word w ∈ Σ ω . First assume that w ∈ L(A). Eve cannot win a play of the game G with the letters played in R A,Σ coming from w using by the first disjunct of her

Figure 3

 3 Figure 3 Alternating weak automaton accepting words over {a, b, c} in which a occurs finitely often and c occurs infinitely often. Omitted transitions lead to a rejecting sink.

Figure 4

 4 Figure[START_REF] Boker | How deterministic are good-for-games automata[END_REF] Alternating coBüchi ∀-GFG automaton accepting words over {a, b, c} in which a occurs finitely often and c occurs infinitely often.

Proposition 31 .

 31 Consider an ∃-GFG alternating Streett automaton A with transition conditions in DNF. Then Eve might not have a strategy σ : Σ + → B A satisfying Lemma 30.

Acceptance is defined in the literature with respect to either states or transitions; for technical reasons we prefer to work with acceptance on transitions.

Bader Abu Radi and Orna Kupferman. Minimizing GFG transition-based automata. In Proceedings of ICALP, pages 100:1-100:16,

Funding Udi Boker: Israel Science Foundation grant 1373/16 Karoliina Lehtinen: This project has received funding from the European Union's Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 892704. * This is the full version of the paper of the same name published at FSTTCS 2020

Appendix

A Appendix of Section 2

In this section of the appendix we provide the remaining technical definitions from Section 2 that are used in the proofs.

Games. A Σ-arena is a directed (finite or infinite) graph with nodes (positions) split into E-labelled positions of Eve and A-labelled positions of Adam, where the edges (transitions) are labelled by elements of Σ { }. The role of is to mark edges that have no influence on the winner of a play, e.g., edges allowing players to resolve some Boolean formula.

We represent such an arena as R = (V, X, V E , V A ), where V is its set of positions;

Notice that the definition allows more than one transition between a pair of positions (such transitions needs to have distinct labels). We will require that each infinite path contains infinitely many Σ-labelled transitions. An arena might be rooted at an initial position v ι ∈ V . We say that a position v is terminal if there is no outgoing transition from v (i.e. no element of X of the form (v, a, v )). If we don't say that an arena is partial then it is assumed that there are no terminal positions.

If R is a (partial) Σ-arena and V ⊆ V is a set of positions, then R V is the sub-arena of R defined as the restriction of R to the positions in V , namely for P ∈ {E, A}, the P -positions of R V are V P := V P ∩ V , and its transitions are

there exists a bijection i : V → V that preserves the membership in V P /V P , for P ∈ {E, A}, and sets of transitions X/X .

A partial play in R is a path in R, i.e., an element

where for every i we have e i = (v i , a i , v i+1 ). Such a partial play is said to begin in v 0 . A partial play is a play if either it is infinite or the last position v i is terminal.

A game is a Σ-arena together with a winning condition W ⊆ Σ ω . An infinite play π is said to be winning for Eve in the game if the sequence of Σ-labels (a i ) i∈N of the transitions along π form a word in W . Else π is winning for Adam. Games with some class X of winning conditions (e.g., the parity condition) are called X games (e.g., parity games).

A strategy for Eve (resp. Adam) is a function τ : V • X • V * → X that maps a history v 0 e 0 v 1 . . . e i-1 v i , i.e. a finite prefix of a play in R, to a transition e i whenever v i belongs to V E (resp. to V A ). A partial play v 0 e 0 v 1 e 1 . . . agrees with a strategy τ for Eve (Adam) if whenever

A strategy for Eve (Adam) is winning from a position v ∈ V if all plays beginning in v that agree with it are winning for Eve (Adam). We say that a player wins the game from a position v ∈ V if they have a winning strategy from v. If the game is rooted at v ι , we say that a player wins the game if they win from v ι . A strategy is positional if its value depends only on the last position, i.e., τ (v 0 e 0 • • • e i-1 v i ) depends only on v i . In that case the strategy of a player P can be represented as a function τ : V P → X.

We also define the notion of strategy with memory M for player P . This is a tuple (σ, M, m 0 , upd) where M is a set of memory states; m 0 is an initial memory state; upd : M × X → M is an update function, and σ : M × V P → X is a strategy deciding which move should be played, depending only on the current memory state and on the current position. winning condition, since L(box( Ā)) = L( Ā). Thus, all the plays over w consistent with her winning strategy σ in G must guarantee that the constructed path of A is accepting. Thus, the run of the automaton D over w is accepting. Now assume that w / ∈ L(A). Dually, no play of the game G with the letters coming from w can produce an accepting run of box(A) over w. Thus, the strategy τ guarantees that the sequence of visited states of A is rejecting. Thus, the run of D over w must be rejecting.

D

Appendix of Section 5

D.1 Proof of Theorem 19

Our aim is to provide an Exptime algorithm for deciding if a given alternating parity automaton is GFG.

Recall the construction of the two nondeterministic parity automata box(A) and box( Ā) for L(A) and L(A) c respectively, as defined in Section 4.2. We will use these automata to design a game characterising the fact that A is both ∃-GFG and ∀-GFG, i.e, A is just GFG.

Recall that the automata box(A) and box( Ā) have exponential number of states in the number of states of A. However, due to Lemma 10 their parity index is linear in the number of transitions of A. Consider the game G = R A,Σ × box(A) × box( Ā), i.e, the game where Adam plays a letter and Eve replies with two boxes, one of A and the other of A. Let the winning condition of that game for Eve say that either of the runs of box(A) or box( Ā) must be accepting.

Lemma 32. Eve has a winning strategy in G if and only if A is GFG.

Proof. Clearly if A is GFG then both box(A) and box( Ā) are GFG as nondeterministic automata. Therefore, one can use strategies witnessing their GFGness to construct a single strategy for Eve in G . This strategy must be winning, because each word proposed by Adam either belongs to L(box(A)) = L(A) or to L(box( Ā)) = L(A) c . Now assume that Eve has a winning strategy in G . This strategy consists of two components: one is a strategy in R A,Σ × box(A) and the other in R A,Σ × box( Ā). By the fact that the languages of box(A) and box( Ā) are disjoint, the above components are in fact winning strategies in the letter games for box(A) and box( Ā) respectively. Thus, by Lemma 20 we know that A is both ∃-GFG and ∀-GFG.

What remains is to show how to solve the game G in Exptime. Let n be the size of the automaton A. Our aim is to turn it into a parity game of size exponential in n but with a number of priorities polynomial in n. Then, by invoking for instance [START_REF] Cristian S Calude | Deciding parity games in quasipolynomial time[END_REF], we know that such a game can be solved in Exptime.

Lemma 33. Let Γ = {0, . . . , N } be a set of priorities. Then, there exists a deterministic parity automaton of size exponential in N , with a number of priorities polynomial in N that recognises the language L of words w ∈ (Γ × Γ) ω that satisfy the parity condition on at least one coordinate.

Proof. It is a rather standard construction. One possibility is to design a nondeterministic Büchi automaton for L with N 2 states. Then, the standard determinisation procedure [START_REF] Piterman | From nondeterministic Büchi and Streett automata to deterministic parity automata[END_REF] applied to this automaton gives a deterministic parity automaton as in the statement. Therefore, we conclude the proof of Theorem 19 by taking a product of the game G with the automaton from Lemma 33 and then solving the resulting parity game.