Simon Iosti

Denis Kuperberg

Eventually Safe Languages

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Synthesis is one of the most classical applications of automata theory. It asks, given a specification, whether there exists a reactive system complying with it. We also want to automatically build such a system when it exists. The specification is typically given in a logic such as Linear Temporal Logic (LTL). The problem was solved positively by Büchi and Landweber [START_REF] Büchi | Solving sequential conditions by finite-state strategies[END_REF] for the case of ω-regular specifications. The usual approach to this problem consists in building a deterministic automaton from the specification, and then solving a game based on this automaton. Henzinger and Piterman [START_REF] Henzinger | Solving games without determinization[END_REF] have proposed a model of Good-For-Games (GFG) automata as a weakening of determinism that is still sound for solving the synthesis problem. An automaton is GFG if there exists a strategy that resolves the non-deterministic choices, by taking into account only the prefix of the input ω-word read so far. The strategy must guarantee to build an accepting run whenever the input word is in the language of the automaton. In [START_REF] Kuperberg | On determinisation of good-for-games automata[END_REF], the question of succinctness of GFG automata compared to deterministic ones is answered. A family (L n ) of languages is exhibited, such that for each n there is a GFG coBüchi automaton of size n for L n , but any deterministic Streett automaton for L n must have size exponential in n. Therefore, GFG automata offer a promising alternative to deterministic ones for synthesis, and this work is part of an effort to systematically study their applicability in this context.

However, one of the potential issues with the use of GFG automata for synthesis lies in the fact that the most usual specification formalism for synthesis is LTL. It is therefore natural to ask whether GFG automata can be useful in this context. We show that the languages L n witnessing succinctness of GFG automata are not LTL-definable. Moreover, a close look at the structure of GFG coBüchi automata, as studied in [START_REF] Kuperberg | On determinisation of good-for-games automata[END_REF], suggests that the ability to permute states is an essential feature of non-trivial GFG automata. It is therefore plausible that GFG automata are no longer succinct (compared to deterministic ones) for LTL-definable languages, where such permutations are forbidden [START_REF] Diekert | First-order definable languages[END_REF].

We answer this question here, by building a family (K n ) of LTL-definable languages presenting the same succinctness gap as the family (L n ) between GFG and deterministic automata. Although this shows that GFG automata are still succinct for LTL-definable languages, the issue of practicability is still unclear, due to the fact that the LTL formulas representing K n have exponential size. Moreover, we show that there are simple µ-calculus formulas of linear size for the same languages. Interestingly, a by-product of this work is the exhibition of the family K n as a candidate witness for an exponential gap succinctness of linear µ-calculus compared to LTL, a problem that is open to our knowledge. This suggests that µ-calculus is more suited than LTL for describing specifications that are recognized by small GFG automata. We therefore aim at proposing a framework based on µ-calculus for building succinct GFG automata.

This leads us to a second issue standing in the way of bringing GFG automata to practical applications. Due to their semantic definition, building GFG automata is a hard problem and requires an understanding of their syntactical shape. A first way to achieve this has been given in [START_REF] Kuperberg | Width of non-deterministic automata[END_REF], building GFG automata in an incremental way from non-deterministic ones. The algorithm tries bigger and bigger automata until a GFG one is reached, the worst case being when a full determinization construction is needed. The only knowledge about GFG automata that is used in this construction is in the subroutine used to test whether an automaton is GFG. We propose here an alternative approach, building automata that are GFG by construction, using the understanding acquired in [START_REF] Kuperberg | On determinisation of good-for-games automata[END_REF] about the structure of GFG coBüchi automata.

Considering restricted classes of specifications is a classical way to try to tackle the difficulty of the synthesis problem. The classes of safety and liveness properties [START_REF] Alpern | Defining liveness[END_REF] have gathered particular interest [START_REF] Prasad | Safety, liveness and fairness in temporal logic[END_REF][START_REF] Zhu | A Symbolic Approach to Safety LTL Synthesis[END_REF], as they simplify algorithms while expressing typical requirements on reactive systems. We introduce a class of properties called "eventually safe" and noted ESafe, for which we give a specification language E νTL and an algorithm systematically producing GFG automata from this language. The class ESafe can be seen as a natural compromise between safety and liveness, and is defined as the class of languages of the form Σ * L safe where L safe is a suffix-closed safety language. Equivalently, the class ESafe is the class of prefix-independent coBüchi languages. As an example, the following specification can be formalized in ESafe: "after being started, the system must eventually start interacting with external agents, and must answer their requests within a fixed finite time".

Both families (L n ) and (K n ) are expressible in the logic E νTL in a very natural way and with formulas of size linear in n. This approach is orthogonal to the one from [START_REF] Kuperberg | Width of non-deterministic automata[END_REF] that we outlined above. Here, we restrict the class of inputs to the class ESafe that is natural for verification purposes, and for which GFG automata are well-suited. We show that unfortunately, translating a formula of E νTL to a GFG automaton is still doubly exponential in the worst case. This is not surprising, as it was shown in [START_REF] Boker | How deterministic are Good-For-Games automata[END_REF] that this is already the case for translating LTL (or linear µ-calculus ) formulas for "bounded" languages, i.e. languages that are both safe and co-safe, to GFG automata. However we believe that this model is worth exploring, in order to understand the power and possible limitations of GFG automata for synthesis. Moreover, recent works such as [START_REF] Esparza | One theorem to rule them all: A unified translation of LTL into ω-automata[END_REF][START_REF] Kretínský | Rabinizer 4: From LTL to your favourite deterministic automaton[END_REF] rely on a modular treatment of specifications, and can call subroutines to build automata for restricted fragments of LTL. This is particularly suitable to embed GFG automata for well-behaved fragments, and the present work brings a clearer understanding of the possibilities and theoretical limitations of this approach. Let us give another example of application of the E νTL formalism, in the spirit of this modular approach. Properties required of systems are often subject to fairness assumptions. This is expressed by specifications of the form ψ ⇒ ϕ for some fairness assumption ψ, that typically consists in liveness properties. This can be treated by building a GFG automaton for ¬ψ, in addition to the automaton for ϕ. In this context, E νTL would for example allow to model the fairness assumption that a finite set of agents (that can be dynamically renamed) will all be activated infinitely many times, as the complement of such a language is similar to the language L n discussed in this work.

Outline of the paper

We start by recalling definitions on logical formalisms and automata in Section 2. In Section 3, we recall the definition of the (L n ) language family from [START_REF] Kuperberg | On determinisation of good-for-games automata[END_REF], and show that it is not LTL-definable. In Section 4, we define the (K n ) family, show that it also witnesses succinctness of GFG automata compared to deterministic ones, and give a family of LTL formulas of exponential size for the languages (K n ). In Section 5, we define the safety fragment S νTL of linear µ-calculus, show that it is equivalent to safety languages, and build the logic E νTL based on its syntax by using an alternative semantic. We show that both families of languages (K n ) and (L n ) have linear-size representations in E νTL, and give a generic algorithm to translate an E νTL formula to a GFG coBüchi automaton. We also exhibit an E νTL formula witnessing that the translation to GFG coBüchi automata is doubly exponential in the worst case. Detailed proofs can be found in Appendix.

Definitions

We will use Σ to denote an arbitrary finite alphabet. The empty word is denoted

ε. If i ≤ j, the set {i, i + 1, i + 2, . . . , j} is denoted [i, j].
The set of finite words on Σ is denoted Σ * , and the set of infinite words Σ ω . We note Σ ∞ = Σ * ∪ Σ ω . If X ⊆ Σ ω , we note pref (X) the set of finite prefixes of words in X, and suff (X) the set of infinite suffixes of words in

X. A set X ⊆ Σ ω is prefix-independent if for all u, v ∈ Σ * and w ∈ Σ ω , we have uw ∈ X ⇔ vw ∈ X. A set X ⊆ Σ ω is suffix-closed if suff (X) = X.

Logic

We define here the linear temporal logic (LTL) and the linear µ-calculus.

The syntax of LTL is defined with the following grammar, where a ranges over Σ:

ϕ := a | ϕ ∨ ϕ | ¬ϕ | ϕ | ϕUϕ
The semantic ϕ ⊆ Σ ω of a formula ϕ of LTL is defined recursively on the formula:

-a = {aw | w ∈ Σ ω }, -ϕ ∨ ψ = ϕ ∪ ψ , -¬ϕ = Σ ω \ ϕ , - ϕ = {aw ∈ Σ ω | a ∈ Σ, w ∈ ϕ }, -ϕUψ = {a 0 a 1 • • • ∈ Σ ω | ∃i ∈ N, ∀j < i, a j a j+1 • • • ∈ ϕ , and a i a i+1 • • • ∈ ψ }.
Let a be an arbitrary letter in Σ and ϕ, ψ be LTL formulas. We will use the syntactic sugar ϕ∧ψ, , ⊥, Fϕ, Gϕ and ϕWUψ as shorthands for ¬((¬ϕ)∨(¬ψ)), a ∨ ¬a, ¬ , Uϕ, ¬F¬ϕ and Gϕ ∨ ϕUψ respectively.

The linear µ-calculus has the following syntax, where a ranges over Σ, and X over a countable set V of variables:

ϕ := a | X | ϕ ∨ ϕ | ¬ϕ | ϕ | µX.ϕ | νX.ϕ
Its semantic ϕ µ,val relative to a valuation val : V → 2 Σ ω of the variables is defined similarly to the semantic of LTL for their common symbols (using the µ-calculus semantic instead of the LTL semantic), with the following additional rules for the new symbols, where gfp and lfp denote the greatest fixed point and the least fixed point operators respectively, and val [X → S] is the valuation val except for val (X) = S:

-X µ,val = val (X); -µX.ϕ µ,val = lfp(S → ϕ µ,val[X→S] ); -νX.ϕ µ,val = gfp(S → ϕ µ,val[X→S] ).
The semantic ϕ µ of a closed formula ϕ is ϕ µ,∅ where ∅ is the empty valuation.

The DAG-size of a formula is a measure of the size of the formula using the directed acyclic graph (DAG) representing the formula instead of the syntactic tree. We define formally the DAG-size |ϕ| dag of a formula ϕ as the size of the set sub(ϕ) of subformulas of ϕ. This representation of a formula as a DAG is usually the one used in algorithms taking as input LTL or µ-calculus formulas (e.g. the translation from a LTL formula to a Büchi automaton), and is therefore a more sensible measure of the size of a formula than the size of its syntactic tree.

Automata

A non-deterministic automaton A is a tuple (Q, Σ, q 0 , ∆, F ) where Q is the set of states, Σ is a finite alphabet, q 0 ∈ Q is the initial state, ∆ : Q × Σ → 2 Q is the transition function, and F ⊆ Q is the set of accepting states. If for all (p, a) ∈ Q × Σ there is at most one q ∈ Q such that q ∈ ∆(p, a), we say that A is deterministic.

If u = a 1 . . . a n is a finite word of Σ * , a run of A on u is a sequence q 0 q 1 . . . q n such that for all i ∈ [1, n], we have q i ∈ ∆(q i-1 , a i ). The run is said to be accepting if q n ∈ F . If u = a 1 a 2 . . . is an infinite word of Σ ω , a run of A on u is a sequence q 0 q 1 q 2 . . . such that for all i > 0, we have q i ∈ ∆(q i-1 , a i ). A run is said to be Büchi accepting if it contains infinitely many accepting states, and coBüchi accepting if it contains finitely many non-accepting states. Automata on infinite words will be called Büchi and coBüchi automata, to specify their acceptance condition.

We will note NFA (resp. DFA) for a non-deterministic (resp. deterministic) automaton on finite words, and NCW (resp. DCW) for a non-deterministic (resp. deterministic) coBüchi automaton. An automaton A is a safety automaton if F = Q, and every run is accepting.

Non-deterministic automata can be generalized to alternating automata, where the transition function associates to each pair (p, a) ∈ Q × Σ a positive boolean combination of states instead of a disjunction. We refer the reader to [START_REF] Fellah | Constructions for alternating finite automata[END_REF] for formal definitions and basic constructions on alternating automata.

We also mention the Rabin condition on infinite words: it consists of a list of pairs (E i , F i ) ∈ 2 Q × 2 Q and an infinite run is accepting if there is i such that some states from E i are seen infinitely often and all states from F i are seen finitely often. Its dual, the negation of a Rabin condition, is called a Streett condition. They both generalize the parity condition.

The language of an automaton A, noted L(A), is the set of words on which the automaton A has an accepting run. Two automata are equivalent if they recognise the same language. For a property P of automata (e.g. safety, or coBüchi), a language is said to be P if it is the language of a P automaton.

An automaton A is determinisable by pruning (DBP) if an equivalent deterministic automaton can be obtained from A by removing some transitions.

An automaton A is Good-For-Games (GFG) if there exists a function σ : Σ * → Q (called GFG strategy) that resolves the non-determinism of A depending only on the prefix of the input word read so far: over every word u = a 1 a 2 a 3 . . . (finite or infinite depending on the type of automaton considered), the sequence of states σ(ε)σ(a 1 )σ(a 1 a 2 )σ(a 1 a 2 a 3 ) . . . is a run of A on u, and it is accepting whenever u ∈ L(A). For instance every DBP automaton is GFG. See [START_REF] Boker | Nondeterminism in the presence of a diverse or unknown future[END_REF] for more introductory material and examples on GFG automata. Lemma 1. GFG automata are closed under the standard union and intersection constructions using cartesian products.

The original family L n

We start by recalling the family of languages L n from [START_REF] Kuperberg | On determinisation of good-for-games automata[END_REF], witnessing an exponential blow-up in the state space for determinisation of GFG automata.

The language L n is defined on alphabet Σ = {ι, σ, π, }. Each letter represents a permutation of the set [0, 2n-1]: ι is the identity, σ is the cycle (0 1 2 . . . 2n-1), π is the transposition (0 1), and is the identity on [1, 2n -1] and is undefined on 0.

An infinite word w ∈ Σ ω describes an infinite graph noted Graph(w) with vertices [0, 2n -1] × N, where letter w(i) representing a permutation α induces edges from vertice (k, i) to (α(k), i + 1) for each k ∈ [0, 2n -1] where α is defined. An example is given below for n = 2. The language L n is then defined as

L n = {w ∈ Σ ω | Graph(w) contains an infinite path}
The infinite path required in the definition of L n needs not start at time 0. Notice that L n is suffix-closed and prefix-independent.

Theorem 2. [15]

There is a GFG-NCW with 2n + 1 states for L n , but any deterministic Streett3 automaton for L n has at least 2 n 2n + 1 states.

However, this example does not settle the blowup problem for languages represented by LTL formulas. Indeed, for any n ≥ 1, the language L n is not LTL-definable: Lemma 3. For all n ≥ 1, there is no LTL formula for the language L n .

Proof. We use the characterization of LTL-definable languages as aperiodic languages [START_REF] Diekert | First-order definable languages[END_REF]. Let M be the syntactic monoid of L n , and h : Σ * → M be the corresponding syntactic morphism. Assume there is u, v ∈ Σ * such that for infinitely many k ∈ N, (u k v) ω ∈ L n and (u k+1 v) ω / ∈ L n . Then we have h(u) k = h(u) k+1 for infinitely many k, so the syntactic monoid of L n cannot be aperiodic, and therefore L n is not LTL-definable. Hence it suffices to find such u, v to prove that L n is not LTL-definable. We can take here u = σ and v = . Indeed, if k is a multiple of 2n, we have

(σ k ) ω ∈ L n and (σ k+1 ) ω / ∈ L n .
Moreover, it is shown in [START_REF] Kuperberg | On determinisation of good-for-games automata[END_REF] that in some sense, the languages L n essentially constitute the canonical example for coBüchi GFG automata. Indeed, in order to show that deciding whether a NCW is GFG can be done in polynomial time, it is shown that GFG-NCW are very close to the following structure: the automaton deterministically follows a safe path, and when a coBüchi state is encountered, the automaton jumps to another such safe path ; in particular, the safe paths can in some sense be "permuted", and a bad choice of path for the automaton can eventually be corrected by jumping to the right path later, provided the GFG strategy has enough memory to remember how paths were permuted. It is thus plausible that the reason exponential memory is needed in GFG-NCW is the presence of arbitrary permutations, and that this could not happen for LTLdefinable languages, where permutations of states are forbidden in the run-DAG of the corresponding automaton [START_REF] Diekert | First-order definable languages[END_REF].

We show in the next section that this is not the case: this exponential blowup result still holds for LTL-definable languages. This gives hope for the use of GFG automata in the context of LTL synthesis.

A family of LTL-definable languages K n with succinct GFG representations

We will define for every n ≥ 1 a LTL-language K n . We show that for all n ≥ 1 there is a GFG-NCW of size 2n + 1 recognizing K n , but there is no deterministic Streett automaton recognizing K n of size less than 2 n 2n+1 .

Definition of the language K n

The language K n is defined on alphabet Σ = {ι, a 0 , a 1 , . . . a 2n-2 , b 0 , b 1 . . . b 2n-2 }.

As in L n , each letter x ∈ L is mapped to a bipartite graph G(x) describing a partial function [0, 2n-1] → [0, 2n-1]. A word w = x 1 x 2 . . . is in K n if and only if the DAG Graph(w) with vertices [0, 2n -1] × N obtained by concatenating all the slices G(x 1 )G(x 2 ) . . . contains an infinite path, not necessarily starting in [0, 2n -1] × {0}, so we define K n = {w ∈ Σ ω | Graph(w) contains an infinite path}.

The graph G(ι) will represent the identity function. For all i ∈ [0, 2n -2], the graph G(a i ) maps i to i + 1, is undefined on i + 1, and leaves [0, 2n -1] \ {i, i + 1} unchanged. For all i ∈ [0, 2n -2], the graph G(b i ) maps i + 1 to i, is undefined on i, and leaves [0, 2n -1] \ {i, i + 1} unchanged. An example of Graph(w) for n = 2 is given below.

Aperiodicity of K n and succinctness of GFG automaton

Theorem 4. There is a GFG coBüchi automaton of size 2n + 1 for K n , but any deterministic Streett automaton for K n has at least 2 n 2n + 1 states.

Proof. (Scheme) The same proof scheme as the one from [START_REF] Kuperberg | On determinisation of good-for-games automata[END_REF] showing the exponential blowup for the family L n can be used here. We need to adapt it to account for the specificities of K n , namely modify the construction to avoid crossings of paths.

Lemma 5. K n is LTL-definable, via a formula of DAG-size at least exponential in n.

Proof. (Scheme) LTL definability is shown via the aperiodicity of K n [START_REF] Diekert | First-order definable languages[END_REF]. We also provide an explicit formula, defined by induction on n, where each induction steps doubles the depth of the formula. Details can be found in Appendix B Conjecture 6. There is no LTL formula for K n with DAG-size polynomial in n.

In the next section, we define a specification logic more suited to this setting.

5 A modal logic for eventually safe properties

The safety logic S νTL

We recall here the formalism S νTL, a fragment of linear µ-calculus designed to express safety properties. This fragment has been studied in several works, usually in the branching time setting ; see for example [START_REF] Wilke | Alternating tree automata, parity games, and modal µ-calculus[END_REF], from which we extract (in Theorem 7 below) part of the characterization of S νTL as the safety fragment of the µ-calculus. A similar characterization for LTL is sketched in the conclusions of [START_REF] Prasad | Safety, liveness and fairness in temporal logic[END_REF]. Formulas of S νTL are given by the following syntax, where a stands for letters of Σ.

ϕ

:= a | ¬a | ϕ ∨ ϕ | ϕ ∧ ϕ | ϕ | X | νX.ϕ
If ϕ is a formula of S νTL, we will note ϕ its semantic as a linear µ-calculus formula.

Theorem 7. A language is definable in S νTL if and only if it is a safety language.

Proof. (Scheme) For the left to right implication, we follow a more general construction that has been proposed in [START_REF] Wilke | Alternating tree automata, parity games, and modal µ-calculus[END_REF], for branching µ-calculus. In our case, the states of the constructed alternating safety automaton are subformulas of the input S νTL formula ψ, and the transition function describes the subformulas that should be true after reading a letter, using alternation to encode the disjunctions and conjunctions. Since alternating safety automata are equivalent to safety languages through standard powerset constructions we are done. For the right to left implication, we build a S νTL formula from a non-deterministic safety automaton by encoding into the formula the transition function; loops in the automaton are encoded using the operator νX.

The logic E νTL for eventually safe properties

We introduce here a second semantic • E for S νTL formulas, called the eventual semantic, in the following way:

ϕ E := {uw ∈ Σ ω | w ∈ suff ( ϕ )}.
That is to say, ϕ E denotes infinite words that have a suffix that is also a suffix of ϕ . This logic can be seen as a way to specify what we mean by a safe behaviour, letting the semantic automatically generate the language of eventually safe behaviours. Notice that since GFG automata are closed under union and intersection by Lemma 1, the technique introduced in this paper can be combined with others in order to treat more advanced specifications.

We call E νTL the logic S νTL equipped with the eventual semantic.

Lemma 8. A language is definable in E νTL if and only if it is of the form Σ * L safe , where L safe is a suffix-closed safety language.

Proof. If L is defined in E νTL via the formula ϕ, then L = Σ * suff ( ϕ ), which is of the wanted form. Conversely, if L = Σ * L safe with L safe a suffix-closed safety language, then by Theorem 7 there is a formula ϕ of S νTL such that ϕ = L safe , and we obtain L = ϕ E .

Let us call ESafe the class of such languages. Notice that E νTL uses a syntax for safety properties, but with our semantics, the languages defined by E νTL are actually liveness properties [START_REF] Alpern | Defining liveness[END_REF]: if L ∈ ESafe, any finite word can be extended to a word in L.

Properties of the class ESafe

The following theorem states that the class ESafe captures exactly prefixindependent coBüchi languages, and that it is equivalent to represent a language from ESafe directly with a NCW, or via its suffix-closed safety language L safe .

Theorem 9. ESafe is equal to the class of prefix-independent coBüchi languages. Moreover, if L = Σ * L safe is accepted by a NCW C, we can build a non-deterministic safety automaton A safe from C recognizing L safe with the same number of states. Conversely, if we have a non-deterministic safety automaton for L safe , we can build a NCW C for L with one more state.

Lemma 10. Given a regular language L, it is decidable whether it is in ESafe. If L is given by a DCW, the problem is in NL, whereas it is PSPACE-complete if L is given by a NCW.

The complexity of deciding whether an arbitrary regular language (given by various models of automata and LTL formulas) is coBüchi-recognizable, and obtaining an equivalent DCW or NCW automaton, is studied in [START_REF] Boker | Co-Büching Them All[END_REF]. This completes the picture for the problem of deciding whether an arbitrary language can be represented using E νTL.

A succinct E νTL formula for the language K n

The formula we aim to build will describe the safety languages of words for which the path starting in (0, 0) is infinite. It recognizes K n via the eventually safe semantic. We use the weak until operator WU as syntactic sugar, defined as ϕWUψ := νX.ψ ∨ (ϕ ∧ X).

The pure LTL formula for K n given in Section B.2 has a DAG-size at least exponential in n. The formulas we will define here will instead be linear in n. Let N = 2n -1. We reuse the subalphabets (α i ) 0≤i≤N defined in Section B.2. We define inductively the formulas ψ i for i from N to 0, each one containing X i-1 as a free variable, except for ψ 0 which is closed:

ψ N = νX N .((α N ∧ X N ) ∨ (b N -1 ∧ X N -1 )) For 0 < i < N : ψ i = νX i .((α i ∧ X i ) ∨ (a i ∧ ψ i+1 ) ∨ (b i-1 ∧ X i-1 )) ψ 0 = νX 0 .((α 0 ∧ X 0 ) ∨ (a 0 ∧ ψ 1 ))
We finally define Φ := ψ 0 .

Lemma 11. The formula Φ has size linear in n, and

Φ E = K n .
We note that a similar formula can be explicited for the original family of languages (L n ) witnessing exponential succinctness of GFG automata. This formula allows to encode the examples of specifications on interacting agents given in the introduction. Details can be found in Appendix D.2

From E νTL to GFG coBüchi automata

In this section, we describe a general algorithm for translating any E νTL formula to an equivalent GFG-NCW. Recall that since GFG automata are sound for synthesis [START_REF] Henzinger | Solving games without determinization[END_REF], this translation can be used as a blackbox for solving synthesis of ESafe properties, specified via the logic E νTL. As explained before, this translation can also be used in a modular way, and combined with other deterministic or GFG automata as shown in Lemma 1. We now describe the algorithm, taking as input an E νTL formula ψ. We can view ψ as a S νTL formula and build an alternating safety automaton A alt recognizing ψ as described in the proof of Theorem 7.

We use a powerset construction to obtain an equivalent non-deterministic safety automaton A nd . Determinizing A nd to a deterministic safety automaton A det through another powerset construction is standard. Since A det can be equivalently seen as a safety DFA, it can be minimized into a safety deterministic automaton A min = (Q, Σ, q 0 , ∆) using standard techniques. Minimization techniques can also be applied on the intermediate automaton A nd , for instance using bisimulation equivalence [START_REF] Paige | Three partition refinement algorithms[END_REF]. Here we omitted the accepting states of A min , since all runs are accepting. We assume that all states of A min are reachable from q 0 .

We will now build a GFG coBüchi automaton C = (Q , Σ, q 0 , ∆, F ) for ψ E , based on A min . We take Q = Q ∪ {⊥}, F = Q, and

∆ = ∆ ∪ {(p, a, ⊥) | ∀q ∈ Q, (p, a, q) / ∈ ∆} ∪ {⊥} × Σ × Q
The following theorem states that the algorithm is correct.

Theorem 12. C is a GFG-NCW for ψ E .

Proof. (Scheme) C will deterministically follow paths made of safe transitions, and will go to ⊥ when the path it is currently following is cut. The only nondeterminism to resolve is: where to jump from ⊥ ? It suffices to jump to the path that has been uncut for the longest time. Details can be found in Appendix D.3.

Remark 13. An alternative construction where strongly connected components of A nd are determinized separately is also possible and allows more optimizations, we discuss this in Appendix D.4. This can yield smaller GFG automata in cases where the size of the biggest strongly connected component of A nd is small in front of its total size, or if some components cover the safe languages of others.

The complexity of this algorithm is doubly exponential in terms of number of states. The following theorem shows that this cannot be avoided. Theorem 14. The translation of E νTL formulas to GFG-NCW is doubly exponential.

Proof. This result for general LTL formulas has been proven in [START_REF] Boker | How deterministic are Good-For-Games automata[END_REF] using a language family (L n ) defined in [START_REF] Kupferman | From linear time to branching time[END_REF], itself adapted from a language of finite words given in [6]. However, the particular structure of the class ESafe prevents us from using the results of [START_REF] Boker | How deterministic are Good-For-Games automata[END_REF][START_REF] Kupferman | From linear time to branching time[END_REF]6] as blackboxes. The language L n as defined by the LTL formula from [START_REF] Kupferman | From linear time to branching time[END_REF] is F n ω where F n is the language defined by

F n = {{0, 1, #} * • # • w • # • {0, 1, #} * • $ • w | w ∈ {0, 1} n }.
We will use similar ideas here, while taking care of the special semantic of E νTL.

Let Σ = {0, 1, #, $, }. We change the formula from [START_REF] Kupferman | From linear time to branching time[END_REF] so that we iterate the closure of F n , with as separator. Intuitively, the S νTL formula ϕ n states that any word on {0, 1} * immediately following a $ has length n, is followed by a , and is identical to a word that occurred between the last and the $ following it. Let Θ = 0 ∨ 1 and Θ = Θ ∨ , we define the following formulas:

ϕ word (X) = Θ ∧ (Θ∧ n • • • (Θ ∧ ( ∧ X)) • • • ) ϕ i,x = ( i x ∧ (Θ WU($ ∧ i x))) for 1 ≤ i ≤ n and x ∈ {0, 1} ϕ match = 1≤i≤n (ϕ i,0 ∨ ϕ i,1 ) ϕ n = νX.Θ WU[# ∧ ϕ match ∧ (Θ WU($ ∧ ϕ word (X)))]
The formula ϕ word (X) checks for {0, 1} n X, where X is a free variable. The formula ϕ i,x checks that i th letter is x and that it is again the case after the next $. The formula ϕ match enforces that the current word u ∈ {0, 1} n must be matched by a $u at the next $. Finally, ϕ n ensures that before the next $, we encounter some u where u is further matched by $u , after which we reiterate the constraint. Notice that |ϕ n | is quadratic in n, and

ϕ n E ∩ (Σ * ) ω = Σ * (F n ) ω .
Let us assume that we have a GFG-NCW automaton C for ϕ n E . We show that C must have at least 2 2 n -1 states. Let Q be the set of states of C and σ : Σ * → Q be the GFG strategy of C. Let us assume that |Q| < 2 2 n -1 . We call the type of a finite run of C the pair (c, q), where c is a bit specifying whether a rejecting state has been seen, and q is the last state of the run. The number of possible types is 2|Q| < 2 2 n . To any set of words X = {u 1 , u 2 , . . . , u k } ⊆ {0, 1} n , we associate a word w X = #u 1 #u 2 # . . . #u k , where the u i 's are lexicographically sorted. Since there are 2 2 n such sets, there must be X 1 = Y 1 ⊆ {0, 1} n such that σ(w X1 ) and σ(w Y1 ) have same type. Without loss of generality let

w 1 ∈ X 1 \ Y 1 , we have w X1 $w 1 ∈ F n but w Y1 $w 1 / ∈ F n .
Again, there are X 2 , Y 2 , q 2 , w 2 such that σ(w X1 $w 1 w X2 ) and σ(w Y1 $w 1 w Y2 ) have same type on the suffix starting with $w 1 , and w 2 ∈ X 2 \Y 2 . By iterating this construction, we build two infinite words

v = w X1 $w 1 w X2 $w 2 . . . and v = w Y1 $w 1 w Y2 $w 2 . . . such that σ accepts v if and only if σ accepts v , but we have v ∈ ϕ n E while v / ∈ ϕ n E .
We obtain a contradiction with the fact that C recognizes ϕ n E with GFG strategy σ.

However, our algorithm can perform well in practice, as witnessed by the languages K n and L n . Indeed, if the input is the formula Φ from section 5.4 (resp. ϕ 0 from appendix D.2) describing the language K n (resp. L n ), the algorithm computes an automaton of size linear in n, while any deterministic automaton would be exponential, by Theorem 4 (resp. Theorem 2).

Conclusion

We showed that GFG automata still enjoy an exponential succinctness gap compared to deterministic automata for the class of LTL-definable languages, by giving a family of languages (K n ) witnessing this gap. However, the LTL formula we give for K n is exponential in n, while there is an equivalent µ-calculus formula that is linear in n. We conjecture that the family (K n ) can be used as a witness to prove an exponential gap in succinctness between the linear µ-calculus and LTL. We defined and studied a class ESafe of eventually safe languages, a natural compromise between safety and liveness specifications. We defined a fragment of linear µ-calculus, the logic E νTL, that describes the class ESafe, and can be translated to GFG coBüchi automata.

The idea of using automata that are allowed to non-deterministically jump to a new path to improve performances in LTL synthesis was implemented in [START_REF] Harding | A new algorithm for strategy synthesis in LTL games[END_REF], but the so-called "shift automaton" was based on a powerset construction, and the notion of Good-for-Games was not identified, replaced by the weaker condition of being Determinisable by Pruning. Prior to the discovery of succinctness of GFG automata, a GFG-based algorithm for model-checking of Markov decision process has been implemented in [START_REF] Klein | Are good-forgames automata good for probabilistic model checking?[END_REF], where it turned out that this particular approach was not more efficient than standard ones.

As future work, we plan to implement our approach that makes use of newly discovered features of GFG automata, in order to compare benchmarks with those present in [START_REF] Harding | A new algorithm for strategy synthesis in LTL games[END_REF][START_REF] Klein | Are good-forgames automata good for probabilistic model checking?[END_REF]. A related open challenge is to find fragments of LTL or other logics that can be translated to GFG automata with only a single exponential blowup.

A GFG automata

A.1 Proof of Lemma 1

Let A 1 = (Q 1 , Σ, q 1 , ∆ 1 , α 1 ) and A 2 = (Q 2 , Σ, q 2 , ∆ 2 , α 2 ) be two GFG automata.
Here α 1 and α 2 are arbitrary acceptance conditions specifying the set of accepting runs: α i ⊆ Q ω i for i ∈ {1, 2}. Let σ i : Σ * → Q i be a GFG strategy for A i . We build a GFG automaton A = (Q, Σ, ∆, q 0 , α) for L(A 1 ) ∪ L(A 2 ) using the usual product construction on automata:

-Q = Q 1 × Q 2 and q 0 = (q 1 , q 2 ) -∆ = {(p 1 , p 2 ) a -→ (p 1 , p 2 ) | p 1 a -→ p 1 ∈ ∆ 1 and p 2 a -→ p 2 ∈ ∆ 2 } -α = {(ρ 1 , ρ 2 ) | ρ 1 ∈ α 1 or ρ 2 ∈ α 2 } It remains to show that A is GFG. We define σ : Σ * → Q for A by σ(u) = (σ 1 (u), σ 2 (u)).
It is straightforward to verify that σ is a GFG strategy for A: whenever w ∈ L(A), we have that w can be accepted by A 1 or A 2 , so either σ 1 (w) or σ 2 (w) produces an accepting run, hence σ(w) is accepting as well.

Notice that the accepting condition α of A is a union of α 1 and α 2 . This means that depending on the nature of α 1 and α 2 , the condition α may be of the same complexity or get more complicated. For instance if α 1 and α 2 are Büchi conditions, then α is Büchi as well. If α 1 and α 2 are parity conditions, α becomes a Rabin condition, and may be transformed into a parity condition with more ranks than α 1 and α 2 .

Notice that if α 1 and α 2 are coBüchi, an alternative construction yields a GFG coBüchi automaton, using the standard construction for the union of coBüchi automata (a coBüchi state of the product is witnessed when both components have seen a coBüchi state). The resulting number of states is still in

O(|Q 1 | • |Q 2 |) in this case.
A similar construction shows that GFG automata are closed under intersection. In the same way, Büchi (resp. coBüchi) GFG automata can be intersected while keeping the acceptance condition, and parity GFG automata can be intersected at the price of increasing the number of parity ranks.

A.2 Proof of Theorem 4

We show that there is a GFG-NCW for K n with 2n + 1 states, and that any deterministic Streett automaton for K n has size at least 2 n 2n + 1 .

This proof closely follows the proof used in [START_REF] Kuperberg | On determinisation of good-for-games automata[END_REF] for the languages L n , adapted here for the languages K n . The main changes are gathered at the end of the proof, such as Lemma 20.

We start by showing that there is a linear-size GFG-NCW C n for the language K n .

The set of states of the automaton C n is Q = {⊥, 0, 1, 2, . . . , 2n -1}. The states [0, 2n -1] are deterministic: reading a ∈ Σ in such a state q the automaton moves to the successive state according to the function represented by a (or to ⊥ if this function is undefined on q). The state ⊥ is non-deterministic -the automaton can move from ⊥ over any letter a ∈ Σ to any state q ∈ [0, 2n -1]. Let the initial state of C n be ⊥ and the rejecting transitions be those of the form ⊥ a -→ q . Note that every accepting run of C n over an ω-word α indicates an infinite path in Graph(α). Therefore, we obtain the following fact.

Fact 15 L(C n ) ⊆ K n .
Lemma 16. C n is a GFG automaton recognizing the language K n .

Proof. It is enough to construct a function σ : Σ * → Q that for every ω-word α ∈ K n produces an accepting run of C n over α -it will prove that K n ⊆ L(C n ) and that C n is GFG. The strategy σ will use a finite memory (of size 2 2n ) under the form of a nonempty subset of Q \ {⊥} that will be updated at every transition. This means we want to define a function M : Σ * → 2 Q\{⊥} . We will define σ and M inductively with σ( ) = ⊥ and M ( ) = Q \ {⊥}.

Let us define the memory function M first. We define M (wa) = {δ(q, a)|q ∈ M (w) and δ(q, a) = ⊥} if this set is not empty, and M (wa) = Q \ {⊥} otherwise. Intuitively, M (w) tracks all the paths in Graph(w) that have not been cut so far, and when all such paths have been cut, it reinitializes. This information will be used by the strategy σ.

Let σ follow deterministically the transitions of C n for all the states q = ⊥: if σ(w) = q, then σ(wa) = δ(q, a) for any letter a. It remains to define σ(wa) if σ(w) = ⊥ and a successive letter a is given. In this case, we consider the set M (wa), and σ(wa) is defined to be the smallest element of M (wa). Note that this definition ensures that σ(w) ∈ M (w) for every w such that σ(w) = ⊥.

Assume that α ∈ K n . We need to prove that σ produces an accepting run of C n over α. Let p 1 , p 2 , . . . , p m be the set of infinite paths in Graph(α) (we know that 1 ≤ m ≤ n). By definition of M , the sets M (α <k ) for k ∈ N will eventually contain only states belonging to some of the infinite paths p i . Let k 0 such that for all k ≥ k 0 , for all p ∈ M (α <k ), the node (p, k) is part of an infinite path in Graph(α). Assume that σ(α <k0 ) = ⊥ (if this is not the case, we replace k 0 by k 0 + 1). Since σ(α <k0 ) belongs to M (α <k0 ), then it will follow in C n the corresponding infinite path and α will be accepted.

We assume for the sake of contradiction that there exists a deterministic Streett automaton D recognising K n that has strictly less than 2 n 2n+1 states. By Theorem 4 from [START_REF] Boker | Nondeterminism in the presence of a diverse or unknown future[END_REF], it means that we can use D as a memory structure for the automaton C n to recognise K n . Therefore, we focus on the product C n × D with the acceptance condition taken from C n . What is important is that C n × D has to follow the transitions of C n . We know that C n × D is a deterministic coBüchi automaton with strictly less than 2 n states and L(C n × D) = K n .

We will use the symbol ρ to denote finite and infinite runs of C n × D. For a given run ρ there are possibly many ω-words α that induce this run, since only the sequence of states is considered in ρ.

The rest of the argument aims at providing an ω-word α that belongs to K n but is rejected by the product automaton C n × D. Intuitively, the construction of α requires to balance between two aims: we need to infinitely often force the product automaton C n × D to take a rejecting transition of C n but at the same time to ensure that there is at least one infinite path in Graph(α). The ω-word α, an infinite path in Graph(α), and the rejecting run of C n × D over α will be constructed as a limit of inductively constructed finite approximations. We will not control exactly the way C n × D works in every position of our approximation, we will be interested only in some checkpoints controlled by partial runs. Definition 17. A partial run is a finite partial mapping τ : ω Q Cn × Q D such that τ (0) is defined and equal to (⊥, q D I ). A partial run τ is rejecting if all its states are of the form (⊥, m). We denote by τ ⊆ ρ the fact that a run ρ agrees with τ wherever τ is defined. The length of τ is the maximal moment of time k such that τ (k) is defined.

Note that the domain of a partial run τ does not have to be an initial segment of ω. The following definition is crucial. Definition 18. Let τ be a partial run of length k. We say that a value i ∈ [0, 2n -1] is alive in τ if there exists an ω-word α such that for the run ρ of C n × D over α we have τ ⊆ ρ and there exists a path p : [0, k] → [0, 2n -1] in Graph(α) that starts in the moment of time 0 and ends in the moment of time k with the value i (i.e. p(k) = i).

Note that in the above definition we actually care only about the first k letters of α. However, it is cleaner to consider ω-words α here.

Figure 1 depicts a partial run and a witness that the value i = 2 is alive.

Our aim is to construct a sequence of partial rejecting runs of increasing lengths τ 0 ⊂ τ 1 ⊂ . . . such that for all ∈ N there are at least n alive values in τ . This will give a contradiction with our assumptions by the following Lemma.

Lemma 19. Assume that there exists a sequence of partial rejecting runs τ 0 ⊂ τ 1 ⊂ . . . of increasing lengths such that for all ∈ N there exists an alive value in τ . Then there exists an ω-word α ∈ K n such that the run ρ of C n × D over α is rejecting.

Proof. Let k be the length of τ . Take any and assume that i is a value that is alive in τ . Observe that it is witnessed by:

-an ω-word α , -a run ρ of C n × D over α , such that τ ⊂ ρ , -a path p : [0, k ] → [0, 2n -1] in Graph(α ) with p (k ) = i .
(q0, m0) (q1, m1) (q2, m2) (q3, m3) (q4, m4) (q5, m5) (q6, m6) (q7, m7) (q8, m8)
Fig. 1. An example of a partial run τ and an ω-word α that witnesses the fact that 2 is alive in τ . The run ρ is the run of Cn × D over α and the states of ρ and τ agree wherever defined. The dashed path is the path witnessing that 2 is alive in τ .

Now we take a subsequence of (α , ρ , p

) ∈N that is point-wise convergent to a triple (α, ρ, p) ∈ Σ × Q Cn × Q D × [0, 2n -1] ω , such that :
ρ is the run of C n × D over α, for infinitely many we have τ ⊆ ρ, p encodes an infinite path in Graph(α).

To formally construct (α, ρ, p) we can proceed similarly as in the proof of König's lemma. We fix (α(i), ρ(i), p(i)) inductively for i = 0, 1, . . .. At each moment we require that infinitely many (α , ρ , p ) agree with (α, ρ, p) on the first i positions. Since for each i there are only finitely many choices of (α(i), ρ(i), p(i)) so we can fix these values in such a way that still infinitely many (α , ρ , p ) agree with them.

By the properties of (α, ρ, p) we know that ρ is rejecting as it contains infinitely many times a state of the form (⊥, m). On the other hand, α ∈ K n because p is a witness that Graph(α) contains an infinite path.

What remains is to construct the sequence τ inductively. Our inductive assumption is that τ is a partial rejecting run and the values 1, 3, 5, . . . , 2n-1 are alive in τ (note that there are n such values). We put τ 0 = 0 → (⊥, q D I ) . Clearly τ 0 satisfies the inductive assumption (in fact all the values i = 0, . . . , 2n -1 are alive in τ 0 ).

Let k be the length of τ . We construct τ +1 from τ by applying some words to the last state (⊥, m ) = τ (k ) of τ and observing the behaviour of C n × D.

The rest of the proof differs from the proof from [START_REF] Kuperberg | On determinisation of good-for-games automata[END_REF], as we have to account for the specificity of K n , namely that paths cannot cross.

Observe that there are N = 2 n words u 1 , . . . , u N ∈ Σ * that encode total functions f : {1, 3, 5 . . . , 2n -1} → [0, 2n -1] such that for all i ∈ {1, 3, 5 . . . , 2n -1}, we have f (i) ∈ {i, i -1}. Such a word for a function f can be built as

b i1 b i2 . . . b i k where {i 1 , . . . i k } = {i ∈ {0, 2, . . . , 2n -2} | f (i + 1) = i}.
We can assume that all the words u 1 , . . . , u N are of equal length by padding them with ι. Since there are strictly less than N = 2 n states of C n × D, there are two distinct such words u, u leading from (⊥, m ) to the same state (q , m ) of C n × D. By the construction of C n × D we know that q ∈ {0, . . . , 2n -1}.

Assume that the functions corresponding to u and u differ on 2i + 1, i.e. one of them maps 2i + 1 to 2i and the other to 2i + 1. Let X be the set of the values {u(1), u(3), . . . , u(2n -3), u(2n -1), u (2i + 1)} (we write here u(i ) for the value assigned to i by the permutation corresponding to u, the same for u ). By the above observations X contains exactly n + 1 elements. Lemma 20. There exists w ∈ Σ * that:

cuts the path from q at the last letter, maps X \ {q } to 1, 3, 5, . . . , 2n-1 if q ∈ X, maps X to 1, 3, . . . , 2n-1, and some even integer 2j if q / ∈ X.

Proof. Let A = {a i | i ∈ [0, 2n -2]} and B = {b i | i ∈ [0, 2n -2]}. Notice that if Y = {y 1 , . . . , y k } and Z = {z 1 , . . . , z k } are subsets of [0, 2n -1] with y i < y i+1 and z i < z i+1 for all i ∈ [0, 2n -2], there exists a word v ∈ Σ * mapping y i to z i for all i ∈ [1, k]. It suffices to take v = w 1 w 2 . . . w k w k w k-1 . . . w 1
where w i ∈ B * maps y i to i -1 and uses no unnecessary letters, and w i ∈ A * maps i -1 to z i in the same way. Proceeding in this order avoids the cutting of any path starting in Y .

Let us assume first that q ∈ X. If q = min X, we can find a word v mapping X to 1, 3, . . . , 2n-1, and an even integer 2j, such that q is mapped to 2j + 1. Taking w = va 2j completes the proof in this case. If q = min X, we can choose v to map X to 1, 3, . . . , 2n-1 and 2, with q mapped to 1, and take w = vb 1 .

Assume now that q / ∈ X. If q > min X. We can find a word v mapping X to 1, 3, . . . , 2n-1, and two even integers 2j and 2j , such that q is mapped to 2j + 1. We then take w = va 2j . Finally, if q < min X, we choose v to map X to 1, 3, . . . , 2n-1 and 2, 4, with q mapped to 1, and take w = vb 1 .

Since w cuts the path from q at the last letter, it means that after reading w from the state (q , m ) the automaton C n × D reaches a state of the form (⊥, m +1 ). For an illustration of these functions, see Figure 2.

Fact 21 Consider τ +1 defined as τ ∪ k + |u| + |w| → (⊥, m +1 )
. By the definition τ ⊂ τ +1 , τ +1 is rejecting, and all the values 1, 3, . . . , 2n -1 are alive in τ +1 (it is witnessed by the fact that these values were alive in τ and by the words uw and u w).

Therefore, we have constructed τ +1 that satisfies the inductive invariant. This concludes the inductive construction of the sequence (τ ) ∈N . By Lemma 19 it finishes the proof of Theorem 4. We first show that the language K n is LTL-definable using a common characterization of LTL-definable languages [START_REF] Diekert | First-order definable languages[END_REF]. We will give an explicit formula for K n in the next section.

Lemma 22. For every word w ∈ Σ * , there exists X w ⊆ [0, 2n -1] such that for all N ≥ 2n, x ∈ X w and y / ∈ X w , Graph(w N ) has a path from (x, 0) to (x, N |w|), and the path starting in (y, 0) is cut.

Proof. Let X w = {x ∈ [0, 2n -1] | Graph(w) has a path from (x, 0) to (x, |w|)}. Let y / ∈ X w , and let us prove that the path starting in (y, 0) is cut in Graph(w 2n ), which will conclude the proof. If the path in Graph(w) starting in (y, 0) is cut, then we are done. If it is not, then it ends in y 1 = y. Assume that y 1 > y (the other case being symmetric). We have y 1 / ∈ X w , for if this was the case, the path ending in y 1 would start in y 1 , and this would imply y 1 = y. Moreover, the path in Graph(w) starting in y 1 is either cut, in which case we are done since the path in Graph(w 2 ) starting in (y, 0) would be cut, or ends in (y 2 , |w|) with y 2 > y 1 : indeed, if we had y 2 < y 1 , then the paths in Graph(w) starting in (y, 0) and in (y 1 , 0) would cross, which is not possible since no letter of Σ allows such a crossing. Repeating this process yields a strictly increasing sequence y, y 1 , . . . , y k in [0, 2n -1], of length at most 2n, such that the path in Graph(w 2n ) starting in (y, 0) contains the points (y, 0), (y 1 , |w|), . . . (y k , k|w|), and is cut before reaching (k + 1)|w| on the second component.

We can now use this lemma to prove that K n is LTL-definable. We use the characterization of LTL-definable languages as aperiodic languages [START_REF] Diekert | First-order definable languages[END_REF]: A language L is LTL-definable if and only if there exists N 0 ∈ N such that for all N ≥ N 0 and u 1 , u 2 , u 3 , v ∈ Σ * , we have both of the following :

(u 1 v N u 2 )u ω 3 ∈ L ⇔ (u 1 v N +1 u 2 )u ω 3 ∈ L u 1 (u 2 v N u 3 ) ω ∈ L ⇔ u 1 (u 2 v N +1 u 3 ) ω ∈ L
The fact that K n satisfies this characterization is a consequence of Lemma 22 : when N ≥ 2n, the uncut paths in the graphs Graph(v N ) and Graph(v N +1 ) are exactly the paths starting in (x, 0) for x ∈ X v , and these paths end in x. Hence the existence of an infinite path in the graph of a word with v N as a subword does not depend on the exponent on N as long as N ≥ 2n.

B.2 An explicit LTL formula for K n

We now give an explicit formula for the language K n , using intermediate formulas with the following intuition:

for i < j and a formula θ, ϕ j i (θ) is a formula whose models are words that have an associated graph with a path starting in i, staying between i and j, touching j, and such that θ is true at the first point where the path comes back to i after touching j (if ever). Figure 3 gives a graphical representation of such a path. for i ≤ j and a formula θ, ψ j i (θ) follows the same intuition as ϕ j i , except that the path of interest is allowed to travel several (possibly infinitely many) times betwen i and j before ending up in i and verifying θ; this is illustrated in Figure 4.

The idea behind the general formula is that if there is an infinite path in Graph(w) oscillating infinitely often between i and j, then it oscillates between i Fig. 4. Formula ψ j i (θ)

and at most j -1 until it goes from i to j (without coming back to i), at which point it oscillates between i + 1 and j until it goes from j to i, and so on. This behavior will be expressible using our formulas ϕ and ψ.

We will define our formulas by recursion on j -i. Let N = 2n -1. For any i ≤ j, we will use the following notation: ψ ≤j i (θ) := i≤k≤j ψ k i (θ). We start by defining for each i the subalphabet α i that maps i to i, and the formula ψ i i (θ).

α i = Σ \ {a i-1 , a i , b i , b i+1 } ψ i i (θ) = α i WUθ
Assume now that the formulas ψ j i have been defined for all i ≤ j such that j -i < j -i. We define the formulas ϕ j i and ψ j i by:

ϕ j i (θ) = ψ ≤j-1 i (a i ∧ (ψ j i+1 (b i ∧ θ))) ψ j i (θ) = ϕ j i ( ) ∧ [(ϕ j i ( ) → ϕ j i (ϕ j i ( )))WUϕ j i (θ)]
The language K n is then described by the formula φ = F( 0≤i≤j≤N ψ j i (⊥)).

Lemma 23. φ = K n Proof. We use the notation w >r for a word w to denote the suffix of w obtained by removing the first r letters of w, and w ≤r for the removed prefix. By a path "staying between i and j", we mean a path that contains only vertices of the form (k, r) for i ≤ k ≤ j.

We will prove inductively on j -i the following induction hypothesis, for any formula θ :

1. for i < j, w |= ϕ j i (θ) if and only if there is a path in Graph(w) starting in (i, 0), staying between i and j, which is either infinite, in which case it never comes back to i once it has touched j (if at all), or contains the vertex (j, r) for some r > 0, ending in a vertex (i, s) with s > r and s minimal for this property, such that w >s |= θ.

2. for i ≤ j, w |= ψ j i (θ) if and only if there is a path in Graph(w) starting in (i, 0), staying between i and j, which is either infinite, or contains the vertex (j, r) for some r ≥ 0, and ends in a vertex (i, s) for some s > r such that w >s |= θ.

The initial case is i = j. Let θ be a fixed formula. There is nothing to prove in point 1. In point 2, by the semantic of the WU operator, w |= ψ i i (θ) if and only if w = uv with u ∈ α * i , and either v ∈ α ω i , or v |= θ. In the first case, the path starting in (i, 0) in Graph(w) is infinite ; in the second case, the rest of the induction hypothesis is satisfied, by choosing r = 0 and s such that v = w >s .

Let us prove point 1 above for some i < j, assuming that the induction hypothesis has been proved for all i , j such that j -i < j -i and all formulas θ. We will prove point 2 afterwards, using point 1. Again, let θ be a fixed formula.

For the left to right implication, let w |= ϕ j i (θ). Then, there is

k < j such that w |= ψ k i (a i ∧ (ψ j i+1 (b i ∧ θ)))
. By the induction hypothesis, there is in Graph(w) a path starting in (i, 0), staying between i and k, which is either infinite or contains the vertex (k, r) for some r > 0, a vertex (i, s) with s > r and s minimal for this property, such that w >s |= a i ∧ (ψ j i+1 (b i ∧ θ)). In the case where the path is infinite, the induction hypothesis is proven. In the other case, we know that w >s = a i v with v |= ψ j i+1 (b i ∧ θ), and using again the induction hypothesis and assuming that the path in Graph(v) starting in (i + 1, 0) is not infinite, we know that v = ub i u with Graph(u) having a path from (i + 1, 0) to (i + 1, |u|) staying between i + 1 and j and containing some vertex (j, r), and u |= θ. Putting all of this together, w = w ≤r a i ub i u , and we see that Graph(w) has a path starting in (i, 0), passing through some (j, r) for r > 0, and which stops at the first vertex (i, s) with s > r, and we have that w >s = u |= θ, which concludes the first implication.

Conversely, let w be a word satisfying the right part of the "if and only if". First case : If the path starting in (i, 0) stays between i and j and is infinite and never comes back to i once it touched j (if at all), then : either it never reaches j, in which case by the induction hypothesis w |= ψ j-1 i (θ ) for any formula θ , and in particular w |= ϕ j i (θ), and we are done ; or it passes through (j, r) for some r minimal. In this case, we can write w = ua i v with Graph(u) having a path starting in (i, 0), staying between i and k for some k < j, reaching k at some point, and ending in (i, |u|), and with the path in Graph(v) starting in (i + 1, 0) staying between i + 1 and j (since it cannot come back to i). Hence, v |= ψ j i+1 (θ ) for any θ by the induction hypothesis, and again by the induction hypothesis on ψ k i (a i ∧ ψ j i+1 (θ )) for any θ , we obtain that w |= ϕ j i (θ). Second case : If the path starting in (i, 0) stays between i and j and contains the vertex (j, r) for some r > 0, ends in a vertex (i, s) with s > r and s minimal for this property, such that w >s |= θ, then by a similar approach, we have that w = ua i vb i w >s with : the path in Graph(u) starting in (i, 0) staying between i and k for some k < j, touching k at some point, and ending in (i, |u|) ; and the path in Graph(v) starting in (i + 1, 0) staying between i + 1 and j, touching j at some point, and ending in (i + 1, |v|). Hence, by the induction hypothesis, we see that vb i w >s |= ψ j i+1 (b i ∧ θ), and that w |= ϕ j i (θ).

We now prove point 2 above. Again, fix some formula θ.

For the left to right implication, let w |= ψ j i (θ). We first note that w |= ϕ j i ( ). By the induction hypothesis, there are two cases :

First case : The path in Graph(w) starting in (i, 0) stays between i and j and is infinite. In this case, the induction hypothesis is satisfied.

Second case : The path in Graph(w) starting in (i, 0) stays between i and j, and comes back to i after touching j. In this case, we will need to inspect the second part of the formula. Since w |= (ϕ j i ( ) → ϕ j i (ϕ j i ( )))WUϕ j i (θ), the formula ϕ j i ( ) → ϕ j i (ϕ j i ( )) must be true of all suffixes of w, or of all suffixes of the form w >s for s < t for some fixed t, and w >t |= ϕ j i (θ). In the first case, by the induction hypothesis, for every s, if w >s |= ϕ j i ( ), then there is a path in Graph(w >s ) starting in (i, 0), reaching (j, r) for some r > 0, coming back to (i, s ), and w >s |= ϕ j i ( ). Consequently, the path starting in (i, 0) in Graph(w) is infinite. In the second case, the same phenomenon occurs until the time t. If the path passes through (i, t), then since w >t |= ϕ j i (θ), the path must continue and either be infinite (in which case we are done), or reach j then come back to (i, t ), and w >t |= θ, and we are also done. The only case left to consider is the case where the path passes through (k, t) for some k > i. Since w >t |= ϕ j i (θ), the path in Graph(w >t ) starting in (i, 0) cannot reach j since by doing so it would cut the original path, thus contradicting the induction hypothesis ; hence, it must be infinite, and in this case the original path cannot come back to i since it would cut the new path, so it is forced to be infinite by induction hypothesis, and we are done.

Finally, let us consider the right to left implication. Consider w satisfying the right side of the "if and only if". We again distinguish two cases :

First case : We can write w = u 1 u 2 . . . u p v for some p ≥ 1 with : for all l ∈ [1, p], Graph(u l ) has a path starting in (i, 0), staying between i and j, reaching (j, r) for some r > 0, and coming back to i for the first time after r only in (i, |u l |) ; and v |= θ. In this case, u p v |= ϕ j i (θ). If p = 1, then since in particular u p v |= ϕ j i ( ), we have w = u p v = ψ j i (θ). If p > 1, we prove by recurrence that for all l ∈ [1, p], u l u l+1 . . . u p v |= (ϕ j i ( ) → ϕ j i (ϕ j i ( )))WUϕ j i (θ). This is true for l = p (since in this case, the left part of the WU is not relevant). If this is true for some l + 1 ≤ p, then let us prove it for l. It is enough to prove that for all r ∈ [0, |u l |], (u l ) >r u l+1 . . . u p v |= ϕ j i ( ) → ϕ j i (ϕ j i ( )). If the path in Graph(u l ) starting in (i, 0) reaches (i, r), then (u l ) >r u l+1 . . . u p v |= ϕ j i ( ) by assumption on u l . In this case, by assumption on u l+1 , we also have (u l ) >r u l+1 . . . u p v |= ϕ j i (ϕ j i ( )), and the property follows. If the path in Graph(u l ) starting in (i, 0) reaches (k, r) for some k > i, then we claim that (u l ) >r u l+1 . . . u p v |= ϕ j i ( ) ; for if this was the case, then by induction hypothesis there would be a path starting in (i, r), staying between i and j, and being either infinite or reaching j at some point, contradicting the fact that the path in (k, r) must come back to i and path-crossing is not possible. Hence, the property is proved. Finally, since p ≥ 1, we see that u 1 . . . u p v |= ϕ j i ( ), and hence w |= ψ j i (θ).

Second case : If the path in Graph(w) starting in (i, 0) stays between i and j and is infinite, then there are two possible subcases. The first subcase is the one where the path oscillates infinitely often between i and j, we can write w = u 1 u 2 . . . u p . . . with the words u p having the same property as in the first case above. But in this case, by a reasoning similar to the one in the first case, we see that w |= ϕ j i ( ) and w |= G(ϕ j i ( ) → ϕ j i (ϕ j i ( ))), and hence w |= ψ j i (θ). The second subcase is the one where the path oscillates between i and j for some time before leaving i and never reaching j, or leaving j and never reaching i. In this case, we can write w = u 1 . . . u p v as above, with p ≥ 0 (there might be no u l at all) and the u l satisfying the same conditions as above, and v being such that the path in Graph(v) starting in (i, 0) stays between i and j, and either never reaches j, or reaches j but never reaches i again afterwards. By the induction hypothesis, v |= ϕ j i (θ), and a reasoning similar to the first case above (starting with v instead of u p v) leads to the same conclusion.

To conclude the proof, we now only have to show that the models of φ are exactly the words from K n . If w ∈ K n , then there is s such that w >s has an infinite path starting in (i, 0) and staying between i and j for some values of i and j. Hence, by our point 2 above, w >s |= ψ j i (⊥), and so w |= φ. Conversely, if w |= φ, then there is s such that w >s |= ψ j i (⊥). But by our result above, there is a path in Graph(w >s ) starting in (i, 0) that stays between i and j and which is infinite, since ⊥ can never be satisfied. Consequently, w ∈ K n , and this concludes the proof.

B.3 Size of the formula

Lemma 24. We have 2 N -1 < |φ| dag < 3 N +1 (N +4)!(5N +4), where N = 2n-1.

Proof. Upper bound

For 0 ≤ k ≤ N , let A(k) = 3 k (k + 1)!(5k + 4)N and B(k) = 3A(k) + 4. We will prove inductively on k = j -i that

|ψ j i (θ)| dag ≤ B(k) + |θ| dag for k ≥ 0 |ϕ j i (θ)| dag ≤ A(k) + |θ| dag for k ≥ 1
For the case k = 0, note that

|ψ i i (θ)| dag = |α i WUθ| dag < 2N + |θ| dag < B(0) + |θ| dag .
For the induction case, assume that the formulas are true for i -j < k, and take i and j such that j -i = k. Note that in the computation below, we make use of the fact that a subformula that appears at different places in a formula needs to be counted only once in the DAG-size; the places where this fact has been used are marked with a ( * ).

|ϕ j i (θ)| dag = |ψ ≤j-1 i (a i ∧ (ψ j i+1 (b i ∧ θ)))| dag ≤ (k -2) + (k -1)B(k -1) + |a i ∧ (ψ j i+1 (b i ∧ θ))| dag ( * ) ≤ (k -2) + (k -1)B(k -1) + 3 + B(k -1) + 3 + |θ| dag ≤ k + 4 + kB(k -1) + |θ| dag ≤ k + 4 + 3kA(k -1) + 4k + |θ| dag ≤ 3kA(k -1) + 5k + 4 + |θ| dag ≤ 3k(3 k-1 k!(5(k -1) + 4)N + 5k + 4 + |θ| dag ≤ 3 k .k.k!(5k -1)N + 5k + 4 + |θ| dag
Now, it is easy to check that if N ≥ 1 2 , then this last expression is less than A(k) + |θ| dag , which concludes the induction step for |ϕ j i (θ)| dag .

|ψ j i (θ)| dag = |ϕ j i ( ) ∧ [(ϕ j i ( ) → ϕ j i (ϕ j i ( )))WUϕ j i (θ)]| dag ≤ 3 + A(k) + 1 + A(k) + A(k) + |θ| dag ( * ) ≤ 3A(k) + 4 + |θ| dag
This concludes the induction proof. We now prove the upper bound on φ (using that (5N + 4)(N + 1) ≥ (5N + 4)N + 6 when N ≥ 1):

|φ| dag = |F( 0≤i≤j≤N ψ j i (⊥))| dag ≤ 1 + (N + 1) 2 -1 + (N + 1) 2 (B(N ) + 1) ( * ) ≤ (N + 1) 2 (3A(N ) + 6) ≤ (N + 1) 2 (3 N +1 (N + 1)!(5N + 4)N + 6) ≤ (N + 1) 2 (3 N +1 (N + 1)!(5N + 4)(N + 1) ≤ 3 N +1 (N + 4)!(5N + 4)

Lower bound

We will make use of the following easy fact:

Fact 25 For all formulas ϕ, |ϕ| dag is greater than or equal to the depth of the syntactic tree of ϕ.

We will actually prove that for any formula θ, ψ N 0 (θ) has a syntactic tree of depth at least 2 N -1 , which is enough for our purpose by Fact 25 since ψ N 0 (⊥) is a subformula of φ.

In order to prove this result for any θ, we consider θ as a free variable, and we compute the maximal depth at which appears this variable in the formula ψ j i (θ) for i ≤ j. We first note that for a fixed value of k = j -i, all the formulas ψ j i (θ) have the same structure, the only difference being a renaming of the leaves of the syntactic tree ; for this reason, we will call d k the maximal depth of the variable θ in these formulas. Now, assume that i < j ; we will follow a branch of the syntactic tree of ψ j i (θ). Consider the subformula ϕ j i (θ) of ψ j i (θ). In this subformula, we consider the branch that goes through ψ j-1 i (a i ∧ (ψ j i+1 (b i ∧ θ))) at the outermost i≤k≤j-1 operator. In this subformula, we again follow the path passing through the subformula ψ j i+1 (b i ∧ θ), then the path to the variable θ.

δ(q a , a) = δ( , a) = δ(q ϕ1∨ϕ2 , ) = q ϕ1 ∨ q ϕ2 δ(q ϕ1∧ϕ2 , ) = q ϕ1 ∧ q ϕ2 δ(q ϕ , a) = q ϕ δ(q X , ) = q ϕ X , where νX.ϕ X is the formula bounding the variable X in ψ.

δ(q νX.ϕ , ) = q ϕ . The values not specified here mean that the function is undefined on these values, for instance δ(a, b) with a = b.

It is shown in [START_REF] Wilke | Alternating tree automata, parity games, and modal µ-calculus[END_REF] for general branching µ-calculus that L(A) = ψ . Conversely, acceptance of a deterministic safety automaton can be expressed by a S νTL formula.

Let A = (Q, Σ, q 0 , δ, Q) be such an automaton, with Q = {q 0 , . . . , q n }. We define formulas ϕ i and ψ i recursively for i from n to 0. If ψ j is defined for all j > i :

ϕ i =       a∈Σ δ(qi,a)=qj j>i (a ∧ ψ j )       ∨       a∈Σ δ(qi,a)=qj j≤i (a ∧ X j )       and ψ i = νX i .ϕ i
It is clear that ψ 0 is a closed formula, and we claim that L(ψ 0 ) = L(A).

This can be proved recursively with the following induction hypothesis at step i : for the interpretation of the variables defined by val (X k ) = L(A, q k ) for all k, we have that L(A, q i ) = ψ i µ,val . Assuming that this hypothesis is satisfied for all j > i, we consider the following equation satisfied by L(A, q i ) :

S =       a∈Σ δ(qi,a)=qj j>i aL(A, q j )       ∪       a∈Σ δ(qi,a)=qj j<i aL(A, q j )       ∪     a∈Σ δ(qi,a)=qi aS    
Using the induction hypothesis for the j > i and the valuation val for the j < i, the following equation is again satisfied by L(A, q i ) :

S =       a∈Σ δ(qi,a)=qj j>i a ψ j µ,val       ∪       a∈Σ δ(qi,a)=qj j<i aval (X j )       ∪     a∈Σ δ(qi,a)=qi aS    
In other words, L(A, q i ) is a fixed point for S → ϕ i µ,val[Xi→S] , hence by the semantic of the νX i operator, L(A, q i ) ⊆ ψ i µ,val . Moreover, if S is that L is a coBüchi language. Moreover, L safe is suffix closed, so for all u, v ∈ Σ * and w ∈ Σ ω , we have uw ∈ Σ * L safe ⇔ suff (w) ∩ L safe = ∅ ⇔ vw ∈ Σ * L safe , showing that L is prefix-independent.

D Constructions using E νTL

D.1 Proof of Lemma 11

We define inductively the formulas ψ i for i from N to 0, each one containing X i-1 as a free variable, except for ψ 0 which is closed (recall that we use the alphabets (α i ) 0≤i≤N defined in Section B.2) :

ψ N = νX N .((α N ∧ X N ) ∨ (b N -1 ∧ X N -1 )) For 0 < i < N : ψ i = νX i .((α i ∧ X i ) ∨ (a i ∧ ψ i+1 ) ∨ (b i-1 ∧ X i-1 )) ψ 0 = νX 0 .((α 0 ∧ X 0 ) ∨ (a 0 ∧ ψ 1 ))
We finally define Φ := ψ 0 .

Lemma 11. The formula Φ has size linear in n, and Φ E = K n .

Proof. Due to the definition of the eventual semantic, we only have to show that the usual µ-calculus semantic of Φ is the set of words that have an infinite path in Graph(w) starting in (0, 0). For all i, let S i be the set of words w such that Graph(w) has an infinite path starting in (i, 0), and let val be the valuation defined by val (X i ) = S i .

Let us prove by induction on i for i from N to 0 that ψ i µ,val = val (X i ). Note that the case i = 0 is exactly what we want to prove the lemma.

For the case i = N , let ϕ

N = (α N ∧ X N ) ∨ (b N -1 ∧ X N -1
), so that ψ N = νX N .ϕ N . We have to show that S N is the greatest fixed point of the map

S → ϕ N µ,val[X N →S] . But ϕ N µ,val[X N →S] = α N S ∪ b N -1 val(X N -1
). Since a word w such that Graph(w) has an infinite path starting in (N, 0) either starts by an element of α N followed by w ∈ S N , or by b N -1 followed by w ∈ S N -1 , we see that S N is a fixed point of S → ϕ N µ,val[X N →S] . Moreover, if S is another such fixed point, then S starts by an element of α N followed by an element of S, or by b N -1 followed by an element of S N -1 , and by definition of the sets S i , this implies that any element w of S belongs to S N . Hence, S N is the maximal fixed point of the above map, and we have that S N = ψ N µ,val .

For the induction case (be it for i > 0 or i = 0), the proof is completely similar once we notice that by the induction hypothesis, ψ i+1 µ,val = S i+1 .

D.2 A E νTL formula for the original L n

We show here that the logic E νTL can also express in a succinct way the original family of languages (L n ) witnessing exponential succinctness of GFG automata. Let N = 2n -1.

We recall that the language L n on Σ = {ι, τ, σ, } is defined by interpreting the letters as permutations on the set [0, N ] ( being partial) : ι is the identity, τ = (0 1), σ = (0 1 . . . N ), (0) = ⊥ and | [1,N ] = id. We define G(w) similarly as above, and define L n to be the set of words w such that G(w) has an infinite path. We will define a formula ϕ such that ϕ defines the words w such that Graph(w) has an infinite path starting in (0, 0), and ϕ E is L n . We define inductively (for i from N to 0) the formulas ϕ i using the variables X 0 , . . . , X N (with ϕ i having as only free variable X 0 , except for ϕ 0 which is closed) :

ϕ N = νX N . ((τ ∨ ∨ ι) ∧ X N ) ∨ (σ ∧ X 0 ) For 1 < i < N : ϕ i = νX i . ((τ ∨ ∨ ι) ∧ X i ) ∨ (σ ∧ ϕ i+1 )
And finally :

ϕ 1 = νX 1 . (τ ∧ X 0 ) ∨ (( ∨ ι) ∧ X 1 ) ∨ (σ ∧ ϕ 2 ) ϕ 0 = νX 0 . (ι ∧ X 0 ) ∨ ((τ ∨ σ) ∧ ϕ 1 )
Lemma 28. ϕ 0 E = L n .

Proof. The proof is essentially similar to the proof of Lemma 11, using the valuation such that val (X i ) is the set of words w such that Graph(w) has an infinite path starting in (i, 0). For this reason, we do not detail it here.

D.3 Proof of Theorem 12

Theorem 12. C is a GFG-NCW for ψ E .

The proof that C recognizes ψ E is similar to the proof of Lemma 16 in Appendix A.2, only in a more general context.

Proof. First, let us remark that L(C) = ψ E . Indeed, Let w be a word accepted in C. Then the accepting run has a suffix not using ⊥, that is to say accepting from some state p in D min . Since we assumed p is reachable, we get that w = uv where u v ∈ L(A). We get that suff (w) ∩ suff (L(A min )) = ∅, and since L(A min ) = ϕ , by definition of the eventual semantic, we get w ∈ ψ E . Conversely, let w be a word in ψ E , then it has a suffix that is accepted by some run ρ from some q in A min . Upon reading this suffix, if C encounters ⊥ it can jump to the current state of ρ and accept the remaining of the suffix. This concludes the proof that L(C) = ψ E .

To prove that C is GFG, it is enough to construct a function σ : Σ * → Q that for every ω-word w ∈ ψ E produces an accepting run of C over w. We will do it inductively with σ( ) = q 0 . Let σ follow deterministically the transitions of C for all the states q = ⊥. It remains to define σ(ua) if σ(u) = ⊥ and a successive letter a is given. Assume that |ua| = k.

We now consider the run-DAG G of C on u. Vertices of G are from Q × N. We consider that a path is cut in G every time it encounters ⊥. Notice that since w ∈ ψ E = L(C), G must contain an infinite uncut path.

For every p ∈ Q let π p be an uncut path of maximal length in G containing the node (p, k). Note that each of these paths π p has a starting position s(π p ) ∈ N.

Let σ(ua) = p such that π p is the longest among the paths {π p | p ∈ Q}, i.e. a path π p such that s(π p ) is minimal. If there are two paths equally old, we move to that with smaller p for an arbitrary ordering on Q.

We need to prove that σ produces an accepting run ρ σ of C over w.

Let t be the minimal starting point of an infinite path π in G. Assume the run ρ σ is rejecting. This means that infinitely often, ρ σ encounters ⊥, and jumps on a state p with s(π p ) ≤ t. This is absurd since this can only be done |Q| -1 times, as after this number of cuts only the path π (or a path π reaching the same state) has been uncut and satisfies s(π) ≤ t. This concludes the proof that C is a GFG-NCW for ψ E .

Notice that we defined an infinite-memory GFG strategy σ, but it is possible to define a GFG strategy σ using memory 2 |Q| , by remembering a set of states M to visit next. When in ⊥, the automaton jumps to a state from M and removes it from M . The set M is updated when reading letters according to the transition function, and it is reinitialized to Q when empty, this also guarantees that any word from ψ E is accepted, since every path is eventually visited until an infinite path is found.

D.4 Alternative Construction for Theorem 12 using strongly connected components

We describe here another possible construction of a GFG-NCW automaton equivalent to a given E νTL formula. The construction is similar to the one given in section 5.5, except that we only determinize the strongly connected components of the intermediate automaton A nd . Let us build A nd the same way as in section 5.5. Recall that if the formula to translate is ψ, then A nd is a safety non-deterministic automaton recognizing ψ . Consider w ∈ suff ( ψ ). Then there is u = vw ∈ ψ , and an accepting run of A nd over u ; this run eventually reaches some strongly connected component with state space C of A nd and never leaves it. In particular, for some suffix w of w, the run restricted to w reaches only states from C.

Let C 1 , . . . , C n be the set of states of the strongly connected components of A nd . We define for 1 ≤ i ≤ n a safety non-deterministic automaton A i which is informally the automaton obtained from A nd by keeping only the states in C i . More formally, again omitting the accepting states since the automata are safety, if A nd = (Q, Σ, q 0 , ∆), then A i = (C i , Σ, C i , ∆| Ci×Σ ) ; note that the A i have all their states as initial states, but it is easy to build an equivalent automaton with only one more state, and only one initial state. Each automaton A i accepts exactly those suffixes w of words u ∈ ψ for which there is an accepting run of A nd over u ending in C i , and for which the run restricted to w reaches only states from C i . Since the semantic we are ultimately interested in is the eventual semantic, we can restrict ourselves to considering these automata independently from each other.

The automata A i can then be determinized and minimized as in Section 5.5, giving deterministic safety automata A i,min = (Q i , Σ, q i , ∆ i ). Once again, we can assume that the A i,min are strongly connected, as keeping only there strongly connected components will not change the eventual semantic we are aiming at.

We can perform one last optimization step: if there are states p ∈ A i,min and q ∈ A j,min with i = j such that L(p) ⊆ L(q), then A i,min can be removed from the list of components. Indeed, if a word w is accepted from p ∈ A i,min , then the same word can be accepted from q ∈ A j,min . This is because A i,min is strongly connected, so there is a path p u -→ p for some word u ∈ Σ * , so uw ∈ L(p) ⊆ L(q), and therefore if q is the state reached from q via u in A j,min , we obtain w ∈ L(q ). Thus, it is enough to keep components covering the possible residual safe languages.

Finally, we build the automaton C = (Q , Σ, ⊥, ∆ , F ), where Q = 1≤i≤n Q i ∪ {⊥}, F = 1≤i≤n Q i , and

∆ =   1≤i≤n ∆ i   ∪{(p, a, ⊥) | ∀q ∈ F, (p, a, q) / ∈ 1≤i≤n ∆ i }∪ {⊥}×Σ× 1≤i≤n Q i
The automaton C thus defined is then a GFG-NCW automaton for ψ E , as can be seen through a proof completely similar to the proof of Theorem 12.

Fig. 2 .

 2 Fig.2. The behaviour of Cn × D over uw and u w. The alive values are in circles, only edges between the alive values are drawn. The dashed edge corresponds to the action of the word u on the value 1 (u and u differ on this value). X is the set of values in circles at the moment of time k + |u|. q = 3 is cut by the last letter of w = a1a0a2, the other elements of X are mapped to 1 and 3.

Fig. 3 .

 3 Fig.3. Formula ϕ j i (θ)

Note that the Streett acceptance condition is not specified in[START_REF] Kuperberg | On determinisation of good-for-games automata[END_REF], but it is in the relevant result of[START_REF] Boker | Nondeterminism in the presence of a diverse or unknown future[END_REF]. The Streett condition for D is needed so that the condition of the form "A accepts or D rejects" is Rabin, and the game admits positional strategies.

Summing up, we have encountered along this path the formulas ψ j-1 i (θ 1 ) and ψ j i+1 (θ 2 ) for some formulas θ 1 and θ 2 , one nested in the other, before reaching the leaf θ. Hence, d j-i > 2d j-i-1 . By recursion, we get that d n-1 > 2 n-1 , which yields the announced minoration of |φ| dag .

C Properties of ESafe

C.1 Proof of Lemma 10 Proof. First of all, recall that it is equivalent whether L is DCW or NCW recognizable [START_REF] Miyano | Alternating finite automata on ω-words[END_REF], and that it is decidable whether it is the case [START_REF] Boker | Co-Büching Them All[END_REF]. Now, if L is given by a DCW D, by Theorem 9, the problem amounts to checking whether L is prefix-independent. It is the case if and only if all reachable states of D accept the same language. This can be verified in NL, by guessing two nonequivalent reachable states, and a lasso in D × D that is accepting for one but not for the other. This is actually a NL procedure for the complement, but since NL is closed under complement, we obtain that membership in ESafe is in NL for DCW inputs.

If L is given by a NCW C, the PSPACE-hardness can be obtained by reduction from NFA universality, which is PSPACE-complete. To reduce it to this problem, consider an arbitrary NFA A = (Q, Σ, ∆, q 0 , F ) on Σ. Let $ / ∈ Σ be a new letter, and q f / ∈ Q be a new state. We build a NCW C = (Q , Σ , ∆ , q 0 , {q f }) by setting

The membership of the problem in PSPACE directly follows from the fact that the problem is in NL for DCW. Indeed, we can use this algorithm with the determinization of C obtained via breakpoint construction [START_REF] Miyano | Alternating finite automata on ω-words[END_REF], yielding a PSPACE procedure.

C.2 Proof of Theorem 7

Recall that Theorem 7 states that a language is definable in S νTL if and only if it is recognized by a safety automaton.

Proof. Recall that safety languages are exactly those accepted by safety automata (i.e. with all states accepting), regardless of whether they are deterministic, nondeterministic or alternating. Indeed, removing alternation or determinizing can be done while preserving the safety condition, through simple powerset constructions.

We show that any S νTL formula can be turned to an alternating safety automaton, as a particular case of the general construction for branching µcalculus [START_REF] Wilke | Alternating tree automata, parity games, and modal µ-calculus[END_REF].

Let ψ be a S νTL formula, and sub(ψ) be the set of subformulas of ψ. We build the alternating safety automaton A = (Q, Σ, q 0 , δ) with -transitions, by choosing as set of states Q = {q ϕ | ϕ ∈ sub(ψ)} ∪ { }, and q 0 = q ψ . The transition function δ is defined as follows, where a ranges over Σ.

a fixed point, then it satisfies the two equations above (using the induction hypothesis for the first one). If w ∈ S, then either w belongs to one of the first two terms of the union in the first equation, in which case it is clearly in L(A, q i ), or it belongs to the last term, in which case it is of the form w = av with a ∈ Σ, δ(q i , a) = q i , and v in S. Repeating this process on v, we see that w ∈ L(A, q i ), so S ⊆ L(A, q i ), and L(A, q i ) is the greatest fixed point of S → φ i µ,val [Xi→S] , that is to say L(A, q i ) = ψ i µ,val , and the induction hypothesis at step i is proven. Finally, step 0 of the induction hypothesis states exactly that ψ 0 µ,val = L(ψ 0 ) = L(A, q 0 ) = L(A).

C.3 Proof of Theorem 9

We recall the statement of Theorem 9:

Theorem 9. ESafe is equal to the class of prefix-independent coBüchi languages. Moreover, if L = Σ * L safe is accepted by a NCW C, we can build a non-deterministic safety automaton A safe from C recognizing L safe with the same number of states. Conversely, if we have a non-deterministic safety automaton for L safe , we can build a NCW C for L with one more state.

We first prove the right to left inclusion. Let L be a prefix-independent coBüchi language, recognized by a NCW C = (Q, Σ, ∆, q 0 , F ), where all states are reachable from q 0 . We define the safety automaton

A safe is the safety automaton obtained from C by suppressing all the non-accepting states, and taking all accepting states as initial. Notice that L(A safe ) is suffix-closed, since all states of A safe are also initial states. Finally, let A be the coBüchi automaton with -transitions defined by (Q , Σ, ∆ , q 0 , {q 0 }), with Q = Q safe ∪ {q 0 }, ∆ = δ safe ∪ {(q 0 , a, q 0 ) | a ∈ Σ} ∪ {(q 0 , , Q 0 )} : for a word to be accepted by this automaton, we must read any prefix of the word, then jump to any initial state of A safe , from which we must stay in A safe . It follows that L(A ) = Σ * L(A safe ), and L(A safe ) is a suffix-closed safety language, so L(A ) ∈ ESafe.

We claim that L(A ) = L(C), which will prove that L(C) ∈ ESafe. First, if w ∈ L(C), then by definition of the coBüchi acceptance condition, w = uv with u ∈ Σ * , and v ∈ L(A safe ), so w ∈ Σ * L(A safe ) = L(A ). Conversely, consider w ∈ L(A ). Then, the accepting run of A on w can be decomposed into q 0 u -→ q 0 -→ q v -→ . . . , where v is accepted in A from q. This implies that v is accepted in C from q. Since q is an accessible state in C there is u ∈ Σ * such that q 0 u -→ q in C, and we get u v ∈ L(C). Since L(C) is prefix-independent, we also have that uv = w ∈ L(C), which concludes the proof of the equality L(C) = L(A ).

Let us now prove the left to right inclusion. Let L ∈ ESafe, i.e. L = Σ * L safe with L safe a suffix-closed safety language. Let A = (Q, Σ, δ, q 0 , Q) be a nondeterministic safety automaton for L safe , with all states accessible from q 0 . As before, we build a NCW C for L by adding to A a non-accepting initial state q 0 , with transitions q 0 a -→ q 0 for all a ∈ Σ, and q 0 -→ q for all q ∈ Q. This shows