Mikolaj Bojańczyk

Igor Walukiewicz

Characterizing EF and EX tree logics

We describe the expressive power of temporal branching time logics that use the modalities EX and EF. We give a forbidden pattern characterization of the tree languages definable in three logics: EX, EF and EX+EF. The properties in these characterizations can be verified in polynomial time when given a minimal deterministic bottom-up tree automaton.

We consider the definability problem for logics over binary trees: given a regular tree language decide if it can be expressed by a formula of the logic in question. The main motivation for considering this problem is to understand the expressive power of tree logics. Although a very old question, definability has gained new relevance with the XML community's burgeoning interest in tree models [START_REF] Neven | Automata, logic, and XML[END_REF]. Indeed, numerous new formalisms for describing tree properties have been recently proposed.

For words the definability question is well studied and understood. Starting from the celebrated Schutzenberger theorem [START_REF] Schützenberger | On finite monoids having only trivial subgroups[END_REF], characterizing star-free word languages by aperiodicity, numerous other language classes have been classified. In particular, we now have a good understanding of the expressive power of LTL and its fragments [START_REF] Straubing | Finite Automata, Formal Languages, and Circuit Complexity[END_REF][START_REF] Wilke | Classifying discrete temporal properties[END_REF]. This is in sharp contrast with the case of trees where much less is known.

We feel that the major goal in the study of the definability problem for trees is to characterize the expressive power of first-order logic, or equivalently CTL * [START_REF] Emerson | Sometimes' and 'not never' revisited: on branching versus linear time temporal logic[END_REF] (we consider finite binary trees here). It seems however that this is a difficult problem whose solution demands new tools and expertise. This is why we have decided to consider fragments of CTL * where the problem is easier. The fragments in question use the modalities EX (there is a successor) and EF (there is a descendant). Apart from being a step towards solving the first-order definability problem, these fragments are interesting on their own. The model-checking problem for them is easier than for CTL * , and even than for CTL: for example when a model is given by a BPP [START_REF] Esparza | Decidability of model-checking for infinite-state concurrent systems[END_REF] or by a a push-down system [START_REF] Walukiewicz | Model checking CTL properties of pushdown systems[END_REF]. The modalities EX and EF are also closely related to operators in XPath [START_REF] Koch | Monadic queries over tree-structured data[END_REF][START_REF] Franceschet | CTL model checking for processing simple XPath queries[END_REF].

We prove the definability problem decidable for three logics: EX, EF and EX+EF. These are built by using the eponymous modalities along with boolean connectives. Our decision procedures use a sort of forbidden pattern characterizations. These forbidden patterns are expressed in terms of the minimal leaves-to-root automaton recognizing a given tree language. The resulting algorithms are polynomial in the number of states of the minimal automaton. If, on the other hand, we assume that the input is a CTL formula or a nondeterministic tree automaton then we obtain the Exptime upper bound matching the obvious lower bound for the problem.

As mentioned above not much is known about the definability problem for trees. There exist basic results: characterizations of the class of regular tree languages by monadic second-order logic [START_REF] Thatcher | Generalized finite automata theory with an application to a decision problem of second-order logic[END_REF] or the µ-calculus [START_REF] Niwiński | Fixed points vs. infinte generation[END_REF]; equivalence of first-order logic and CTL * over finite binary trees [START_REF] Hafer | Computation tree logic CTL and path quantifiers in the monadic theory of the binary tree[END_REF]. Yet there is no equivalent of the Schutzenberger theorem for trees; in fact decidability of first order definability is still open. There has been some work in this direction; in particular borrowing the notion of aperiodicity from the word case is known to be insufficient [START_REF] Potthoff | First-order logic on finite trees[END_REF][START_REF] Heuter | First-order properties of trees, star-free expressions, and aperiodicity[END_REF].

It is also a valid question to compare the characterizations presented in this paper with the ones in [START_REF] Wilke | Classifying discrete temporal properties[END_REF] for the corresponding word logics X, F and X + F. Although there is some resemblance between the two, our results need more than a straightforward extension of the forbidden pattern characterizations from the word case. This is in a way unfortunate because it suggests that an equivalent of the Schutzenberger theorem for trees may also require an intricate extension of the aperiodicity.

The plan of the paper is as follows. After a preliminary section we briefly state a characterization of EX logic. This is very similar to a characterization of modal logics presented in the literature [START_REF] Otto | Eliminating recursion in the µ-calculus[END_REF], so we mention the result mostly for completeness. In the next two sections we respectively characterize the logics EF and EX+EF. Maybe counterintuitively, the argument for the weaker EF logic is longer. In the penultimate section we summarize the results, showing how they imply decidability algorithms. Finally, we justify our characterizations by pointing out why the forbidden patterns known from the word case do not adapt directly to the tree case.

A tree domain is any nonempty finite prefix-closed subset of {0, 1} * . A Σ-tree is any mapping from some tree domain to Σ. We denote by dom(t) the domain of t (as a function), elements of this set are called nodes. The root is another name for the node . Nodes in a tree are ordered by the prefix relation, which is denoted ≤. Leaves are nodes that are maximal with respect ≤. The subtree of a tree t rooted in the node v is the tree that assigns to a node w the label t(v • w). This tree is denoted as t| v and its domain is the set of nodes w such that v • w is a node of t. The left subtree of t is the tree t| 0 , the right subtree is t| 1 . A Σ-context is any Σ tree with a distinguished leaf, which is called the hole. We denote contexts by C[], D[]. We write C[t] to denote the tree obtained from the context C[] by substituting the tree t for the hole.

A Σ-language is any set of Σ-trees. Given a language L, two trees s and t are said to be L-equivalent if for every context C[], either both or none of the trees C[s] and C[t] belong to L. This is an equivalence relation. An equivalence class of this relation is called an L-type. We will denote types using the letters α, β, γ. Given two L-types α, β and a letter a, the L-type a[α, β] is uniquely defined and contains the trees equivalent to any tree with a in the root, s in the left son and t in the right son. A language is regular if it has a finite number of types.

EX+EF Formulas

EX+EF formulas are CTL * formulas which use boolean connectives, letter symbols and where the temporal modalities are allowed only in the forms EX (exists next) and EF (exists finally).

Below follows a more formal definition along with the semantics. Let Σ be an alphabet. The set of EF+EX formulas over Σ is the smallest set of formulas such that:

• Every letter a ∈ Σ is a formula.

• Boolean combinations ¬ψ, ψ∧ϕ and ψ∨ϕ of formulas are also formulas.

• If ϕ is a formula then EX 0 ϕ, EX 1 ϕ and EFϕ are formulas.

The set of EF formulas is the fragment obtained by disallowing EX 0 and EX 1 , while the set of EX formulas is obtained by disallowing EF. We now define the semantics, which with every formula associates a set of Σ-trees that satisfy it:

• A tree satisfies the formula a if its root is labeled by a;

• Satisfaction for boolean operations is defined in the standard way;

• A tree satisfies EX 0 ϕ (resp. EX 1 ϕ) if its left (resp. right) subtree satisfies ϕ;

• A tree satisfies EFϕ if it has a proper subtree that satisfies ϕ.

We call EF, EX 0 and EX 1 the modalities. Observe that the modality EF has strict semantics here: the appropriate subtree has to be proper. The formula AXϕ is used as an abbreviation of ¬EX¬ϕ, while AGϕ is used as an abbreviation of ¬EF¬ϕ.

A tree language L is definable in EF+EX if there is a formula satisfied in exactly the trees in L. Similarly we define languages definable in EF and in EX.

Languages Definable in EX

In this section we state a characterization of languages definable in EX. We do this for the sake of completeness since the characterization is essentially the same as in [START_REF] Otto | Eliminating recursion in the µ-calculus[END_REF].

Definition 1 Two trees are identical up to depth k if they are the same when restricted to {0, 1} ≤k . We say that a language L is dependent on depth k if every two trees which are identical up to depth k have the same L-type.

A context is nontrivial if its hole is not in the root.

Definition 2 Let L be a language and let α, β be two distinct L-types. We say that the language L contains an {α, β}-loop if for some nontrivial

context C[], both C[α] = α and C[β] = β hold.

Theorem 3

For a regular language L, the following conditions are equivalent:

1. L is definable in EX;
2. For some k ∈ N , L is dependent on depth k; 3. L does not have an {α, β}-loop for any two L-types α, β .

Proof

The equivalence of the first two conditions is obvious, as is the implication from 2 to 3. To end the proof of the theorem, we will show that if the language L is not dependent on any depth k, then a loop can be found.

Let k > |Types(L)| 2 and assume that L is not dependent on depth k. This means there are trees s and t which are identical up to depth k but have different types. Let v 1 , . . . , v n be all the nodes of depth k in the tree s (or equivalently in t). We define a sequence of trees s = s 0 , . . . , s n = t which gradually morphs from the tree s to the tree t:

s 0 = s and s i = s i-1 [v i := t| v i ] for i > 0 .
Since the trees s 0 and s n have different types, there must be some i ∈ {1, . . . , n} such that s i-1 and s i have different types. These two latter trees differ only below the node v i . Let w 0 < . . . < w k-1 be all the ancestors of the node v i . Given j < k, let

α j = type(s i-1 | w j ) and β j = type(s i | w j ).
Since the node v i is at depth k > |Types(L)| 2 , there must be some two indices j < k such that the equalities α j = α k and β j = β k hold. Since the types of s i-1 and s i are distinct, so are the types α j and β j . But this means that the part of s i-1 whose root is in w j and whose hole is in w k provides an {α j , β j }-loop.

Languages definable in EF

In this section we show a characterization of languages definable in EF. This is the most involved section of the paper, with a long technical proof. The characterization result, Theorem 5, shows that definability in EF is equivalent to a certain (decidable) property of the language's types. This property, however, is not directly stated in terms of types, but using an intermediate concept called the delayed type. The intuition behind a delayed type is that it is supposed to contain all the information about a tree that does not depend on the root label.

Given a Σ-tree t and a letter a ∈ Σ, we write t a to denote the tree obtained from t by relabeling the root with the letter a. With every Σ-tree t we associate its delayed type, which is the function that assigns to a letter a ∈ Σ the L-type of the tree t a . We will denote delayed types using the letters x, y, z. Note that the delayed type of a tree is uniquely determined by the types of its left and right subtrees. We write (x, a) L y if there is a tree of delayed type y having a subtree of type x(a). We also write x L y if (x, a) L y for some a ∈ Σ. This relation is a quasiorder but not necessarily a partial order, since it need not be antisymmetric.

For delayed types x, y and letters a, b ∈ Σ, we write dtype L (x, a, y, b) for the delayed type which assigns to a letter c the type c[x(a), y(b)]. In other words, this is the delayed type of a tree whose left and right subtrees have types x(a) and y(b) respectively. The set of neutral letters of a delayed type x is the set N L x = {a : x = dtype L (x, a, x, a)}. This set may be empty.

Definition 4 A Σ-language L is EF-admissible if it is a regular tree language such that all delayed types x, y and all letters a, c ∈ Σ satisfy:

P1 The relation L on delayed types is a partial order;

P2 dtype L (x, a, y, b) = dtype L (x, a, y, b ) for all b, b ∈ N L y ;
P3 if (x, a) L y then dtype L (x, a, y, c) = dtype L (y, c, y, c);

P4 dtype L (x, a, y, c) = dtype L (y, c, x, a).
Another important concept used in Theorem 5 is that of typeset dependency. The typeset of a tree is the set of types of its proper subtrees. We say that a regular language is typeset dependent if the delayed type of a tree depends only on its typeset.

Our characterization of EF is presented in the following theorem:

Theorem 5

For every language L, the following conditions are equivalent:

1. L is definable in EF, 2. L is typeset dependent, 3. L is EF-admissible.
The proof of this theorem is long and will be spread across the next three sections; the implications 1 ⇒ 2, 2 ⇒ 3 and 3 ⇒ 1 being proved in Sections 3.1, 3.2 and 3.3 respectively. For the remainder of Section 3 we assume that an alphabet Σ along with a regular Σ-language L are fixed, hence we will omit the L qualifier from the notation, writing for instance instead of L . We may assume regularity since all conditions 1, 2 and 3 imply this.

A Language Definable in EF Is Typeset Dependent

In this section, we will show that the language L is typeset dependent using the assumption that it is defined by some EF formula ψ. Definition 6 By cl(ψ) we denote the smallest set of formulas that contains ψ and is closed under negations and subformulas.

It is not difficult to see that the type of a tree is determined by the set of those formulas from cl (ψ) which it satisfies (although this correspondence need not be injective). Our first step is to show that for the delayed type, even less information is sufficient Definition 7 An existential formula is a formula of the form EFϕ. The signature Sig(t) of a tree t is the set of existential formulas from cl(ψ) that it satisfies.

Lemma 8

The signature of a tree determines its delayed type.

Proof Take two trees s and t with the same signatures. For a given letter a ∈ Σ, an easy induction on formula size shows that for all ϕ ∈ cl(ψ):

s a |= ϕ iff t a |= ϕ.
This is due to the fact that the modality EX is strict. Since the two trees s a and t a satisfy the same formulas from cl(ψ), their types must be the same. As the choice of the letter a was arbitrary, this implies that the trees s and t have the same delayed types.

Given two trees t 0 , t 1 and a letter a ∈ Σ, we write Sig(t 0 , t 1 ) instead of Sig(a[t 0 , t 1 ]). This notation is unambiguous since Sig(a[t 0 , t 1 ]) does not depend on the letter a.

Given two types α and β, we denote by dtype(α, β) the delayed type which assigns to a letter a the type a

[α, β]. A type α is reachable from a type β, denoted β α, if C[β] = α holds for some context C[].
This relation is a quasiorder and we use ≈ for the accompanying equivalence relation. The following simple lemma is given without a proof:

Lemma 9 If t is a subtree of t, then Sig(t , s) ⊆ Sig(t, s). If α β then dtype(α, β) = dtype(β, β).
The following lemma shows that for languages definable in EF, the relation ≈ is a congruence with respect to the function dtype(α, β):

Lemma 10 If α 0 ≈ β 0 and α 1 ≈ β 1 then dtype(α 0 , α 1 ) = dtype(β 0 , β 1 ).

Proof

Since a language definable in EF satisfies dtype(α, β) = dtype(β, α), it is sufficient to prove the case where

β 1 = α 1 . Let C[] be a context such that C[α 0 ] = β 0 and let D[] be a context such that D[β 0 ] = α 0 .
Both contexts exist by assumption that α 0 ≈ β 0 . Let s 0 be a tree of type α 0 and let s 1 be a tree of type α 1 . Consider the two sequences of trees {s i 0 } i≥0 and {t i 0 } i≥0 defined by induction as follows:

s 0 0 = s 0 ; t i 0 = C[s i 0 ] for i ≥ 0; s i 0 = D[t i-1 0 ] for i ≥ 1.
By a simple induction one can prove that for all i ≥ 0,

type(s i 0 ) = α 0 and type(t i 0 ) = β 0 .
From Lemma 9 we obtain the following inclusions:

Sig(s 0 0 , s 1 ) ⊆ Sig(t 0 0 , s 1 ) ⊆ Sig(s 1 0 , s 1 ) ⊆ Sig(t 1 0 , s 1 ) ⊆ . . .
Since there are only finitely many signatures, there must be some i > 0 such that Sig(s i 0 , s 1 ) = Sig(t i 0 , s 1 ). Consequently, by Lemma 8, the delayed types dtype(α 0 , α 1 ) and dtype(β 0 , α 1 ) are equal.

We are now ready to show that the language L is typeset dependent. Let s and t be two trees with the same typeset. We want are going to show that they have the same delayed type.

If this typeset is empty, then both trees have one node and, consequently, the same delayed type. Otherwise one can consider the following four types, which describe the left and right subtrees of s and t:

α 0 = type(s| 0 ) α 1 = type(s| 1 ) β 0 = type(t| 0 ) β 1 = type(t| 1 ).
We need to prove that dtype(β 0 , β 1 ) = dtype(α 0 , α 1 ). By assumption that the typesets of s and t are equal, both β 0 and β 1 occur in nonroot nodes of s and both α 0 and α 1 occur in nonroot nodes of t. Thus β 0 α holds for some α ∈ {α 0 , α 1 } and similarly for β 1 , α 0 and α 1 . The result follows from the following case analysis:

• β 0 , β 1 α for some α ∈ {α 0 , α 1 }.
By assumption we must have α β for some β ∈ {β 0 , β 1 }. Hence α ≈ β. By Lemma 10 we get

dtype(α, α) = dtype(β, β) . (1)
As β 0 , β 1 α β, from Lemma 9 we obtain dtype(β 0 , β 1 ) = dtype(β, β) .

(2)

Similarly one proves the equality

dtype(α 1 , α 2 ) = dtype(α, α) . (3)
The three equations ( 1), ( 2) and ( 3) yield the desired result.

• α 0 , α 1 β for some β ∈ {β 0 , β 1 }. As in the case above.

• A short analysis reveals that if neither of the above holds then β 0 α i β 0 and β 1 α 1-i β 1 for some i ∈ {0, 1}. Therefore β 0 ≈ α i and β 1 ≈ α 1-i and an application of Lemma 10 yields the desired result.

A Typeset Dependent Language Is EF-Admissible

This step of the proof consists of verifying that all the properties P1 to P4 are satisfied if the language is typeset dependent.

Lemma 11 L satisfies the property P1.

Proof

Condition P1 states that is a partial order on delayed types. The relation is obviously transitive and reflexive. We will show that x y x implies that the delayed types x and y are equal. Assume then that x y x. In this case, for arbitrary n we can find a tree t with nodes

v 1 ≤ w 1 ≤ v 2 ≤ w 2 ≤ • • • ≤ v n such
that subtrees rooted in the v i nodes have type x and subtrees rooted in the w i nodes have type y. Clearly for all 0 ≤ i < n we have TS(

t| v i ) ⊆ TS(t| w i ) ⊆ TS(t| v i+1 ).
If we take n to be bigger than the number of types in L then we can find some i such that TS(t| v i ) = TS(t| w i ), which by typeset dependency implies x = y.

Lemma 12 L satisfies the property P2.

Proof

Condition P2 states that if b, b are neutral letters for a delayed type y, then the delayed types dtype(x, a, y, b) and dtype(x, a, y, b ) are equal. To show that this condition is satisfied, we define by induction a sequence of trees t 0 , t 1 , . . . in the following manner. For t 0 we take some tree of delayed type y with b in the root, while t i+1 is defined as b

[b [t i , t i ], b [t i , t i ]], see Fig. 1.
Because b and b are neutral letters for the delayed type y, all the trees t i have delayed type y. Moreover, for some j > 0, the typesets of the trees t j and b [t j , t j ] are equal. Take now some tree t of delayed type x and with the label a in the root. Let s be a tree with t as the left subtree and t j as the right subtree. Similarly we define s , but with b [t j , t j ] in the right subtree. We do not specify the root letters, since we are interested in delayed types. By assumption on t j and b [t j , t j ], the trees s and s have the same typesets. Since L is typeset dependent, their delayed types must be equal. Therefore,

dtype(x, a, y, b) = dtype(s) = dtype(s ) = dtype(x, a, y, b ).
The last two properties P3 and P4 are obviously satisfied in every typeset dependent language.

A EF-Admissible Language Is Definable EF

We now proceed to the most difficult part of the proof, where a defining EF formula is found based only on the assumption that the properties P1 to P4 are satisfied. We start by stating a key property of EF-admissible languages which shows the importance of neutral letters.

Lemma 13 If the delayed type of a tree t is y, then its every proper subtree with delayed type y has its root label in N y .

Proof

Consider some proper subtree t| v of delayed type y and its root label b = t(v). Let w be the brother of the node v and let z, c be its delayed type and label, respectively. Obviously (z, c) y. Note that if the trees t and t| v have delayed type y, then so does the tree t| w for any w < v, because is a partial order. In particular, the above lemma says that nodes with delayed type y form cones whose nonroot elements have labels in N y .

Formulas Defining Delayed Types

A delayed type x is definable if there is some EF formula θ x true in exactly the trees that have delayed type x. The construction of the θ x formulas will proceed by induction on the order.

A set A of delayed types is downward closed if it contains every delayed type -smaller than an element of A. The first step is the following lemma: Lemma 14 Let x be a delayed type and let A x be a downward closed set of definable delayed types. There is a EF formula fork A

x such that:

t fork A x iff dtype(t) =
x and for all w > , dtype(t| w ) ∈ A.

A fork formula is satisfied in a maximal node of delayed type x, where moreover all descendants have delayed types in A.

We postpone the technical proof of this Lemma until Section 3.4. Meanwhile, we will use this lemma to construct a formula θ x defining x. For the rest of Section 3.3 we fix the delayed type x and assume that every delayed type y x is definable by a formula θ y .

The first case is when x has no neutral letters. Let x-denote the set {y : y x}. By Lemma 13, in a tree of delayed type x both sons have delayed types in x-, since there are no neutral letters for x. In this case we can set

θ x = fork x- x . (4)
The correctness of this definition follows immediately from Lemma 14. The definition of θ x is more involved when the set of neutral letters for x is not empty. The rest of Section 3.3 is devoted to this case.

Consider first the following formula:

θ x = EF {b ∧ θ y : y x ∧ (y, b) x} ∨ {fork x- y : y x}
The intention of this formula is to spell out evident cases when the delayed type of a node cannot be x. The first disjunct says that there is a descendant with a delayed type and a label that prohibit its ancestors to have type x.

The second disjunct says that the type of the node is not x but the types of all descendants are x. This formula works correctly only when some assumptions about the tree are made. These assumptions use the following definition: given a delayed type x, we define OK x to be the set of tree t such that:

dtype(t) x or dtype(t) = x and t( ) ∈ N x .
Note that by Lemma 13 the set OK x is closed under taking subtrees.

Lemma 15 Let t be a tree with the left and right subtrees in OK x . This tree satisfies θ x if and only if dtype(t) x.

Proof

The left to right implication was already discussed and follows from the assumptions on the θ y formulas used in θ x and from Lemma 14.

For the right to left implication, let dtype(t) = dtype(y, b, z, c) with y, b, z, c describing delayed types and labels of the left and right subtrees of t. We consider three cases:

• y = z = x. This is impossible because both the left and right subtrees of t belong to OK x , so the labels a, b must belong to N x , and thus dtype(t) = x.

• y = x and z x. Since the left subtree of t belongs to OK x , the label b belongs to N x . If the inequality (z, c) x were true (which is not necessarily implied by our assumption that z x), then by property P3 we would have

dtype(t) = dtype(y, b, z, c) = dtype(x, b, z, c) = dtype(x, b, x, b) = x ,
a contradiction with dtype(t) x. Therefore we have (z, c) x and hence the first disjunct of θ x holds. The case where z = x and y x is symmetric.

• y, z x. In this case the second disjunct in the definition of θ x must hold by Lemma 14.

Let θ x stand for y x θ y and consider the formula

ϕ x = θ x ∨ (¬θ x ∧ {a : a ∈ N x }) .
This formula will be used to define the set OK x . We use AG * as the nonstrict version of AG, i.e. AG * ϕ is an abbreviation for the formula ϕ ∧ AGϕ.

Lemma 16 A tree satisfies AG * ϕ x if and only if it belongs to OK x .

Proof

By induction on the depth of the tree.

⇒ If t satisfies ϕ x because it satisfies θ x , then it obviously belongs to OK x . Otherwise we have t( ) ∈ N x and t θ x .

By induction assumption all proper subtrees of t belong to OK x . But then, by Lemma 15, dtype(t) x. This, together with t θ x shows that the delayed type of t is x and therefore t belongs to OK x .

⇐ Let t be a tree in OK x . By induction assumption we have AGϕ x . We need to prove that t satisfies ϕ x . If type(t) x holds, then t satisfies θ x and we are done. Otherwise, as OK x (v) holds, dtype(t) = x and t( ) ∈ N x . Hence, by Lemma 15, t satisfies the second disjunct in ϕ x .

Since the type of a tree can be computed from its delayed type and root label, the following lemma ends the proof that every EF-admissible language is definable in EF:

Lemma 17 Every delayed type is definable.

Proof

By induction on the depth of a delayed type x in the order . If x has no neutral letters then the defining formula θ x is as in (4). Otherwise, we set the defining formula to be

θ x = ¬θ x ∧ ¬θ x ∧ AGϕ x .
Let us show why θ x has the required properties. By Lemma 16,

t AGϕ x iff t| 0 , t| 1 ∈ OK x . (5)
If t θ x then we get dtype(t) = x using Lemma 15 and (5). For the other direction, if dtype(t) = x then clearly ¬θ x holds in t. By Lemma 13 the left and right subtrees of t are in OK x , therefore t satisfies AGϕ x by [START_REF] Koch | Monadic queries over tree-structured data[END_REF]. But then the formula ¬θ x holds by Lemma 15.

A fork Formula

Recall Lemma 14 which was used in Section 3.3, but not proved there:

Lemma 14 Let x be a delayed type and let A x be a downward closed set of definable delayed types. There is a EF formula fork A x such that:

t fork A x iff dtype(t) =
x and for all w > , dtype(t| w ) ∈ A.

The rest of Section 3.4 is devoted to a proof of this lemma. We fix a delayed type x and a downward closed set of delayed types A. We assume that x ∈ A and that all the delayed types in A are definable.

For a delayed type y ∈ A and a letter b ∈ Σ, we say that the pair (y, b) is sufficient if dtype(y, b, y, b) is our fixed delayed type x. Given a delayed type y, we define the following equivalence relation ∼ y over Σ:

a ∼ y b iff a = b or a, b ∈ N y .
Remember that we want an EF formula expressing the fact that a tree t has delayed type x, though its proper subtrees only have smaller delayed types. Let y,b and z,c be the delayed types and root labels of the left and right subtrees of t. If the language is EF-admissible then there are essentially two possible reasons for this: If we had the next modality EX, expressing the above properties would be very simple. Unfortunately this is not the case and we will need to use some rather complicated coding, which involves the following formulas:

θ y = z y θ z for y ∈ A ∪ {x}; θ y = z y θ z for y ∈ A; θ b y = EF(θ y ∧ b) ∧ AG(θ y ⇒ (b ∨ N y )) for y ∈ A, b ∈ Σ; θ y = {θ z ∧ c : (z, c) y} for y ∈ A; ϕ b y = θ b y ∧ AGθ y ∧ AG(θ y ⇒ θ y ) for y ∈ A, b ∈ Σ.
Observe that these formulas are well defined because we have assumed that all delayed types in A are definable, hence the appropriate θ y formulas exist.

Lemma 18 If (y, b) is sufficient, a tree satisfying ϕ b y has delayed type x.

Proof

Let t be a tree that satisfies ϕ b y . First we will show that either the left or right subtree must have delayed type y and a root label ∼ y -equivalent to b. Let Y be the proper subtrees of t with delayed type y; this set is not empty because t satisfies EF(θ y ∧ b). Since is a partial order and AGθ y holds, every tree with a subtree in Y also belongs to Y . If b ∈ N y then by EF(θ y ∧ b), there is a tree in Y with the root labelled b. This must be either the left or right subtree of t as Lemma 13 says that all trees in Y apart from t| 0 and t| 1 must have labels in N y . If the letter b belongs to N y then, by AG(θ y ⇒ (b ∨ N y )) the root label of every tree in Y is in N y and hence ∼ y -equivalent to b. But this holds for either the left or right subtree, since Y is nonempty. Now we can prove that t has delayed type x. By the reasoning above, a tree s ∈ {t| 0 , t| 1 } has delayed type y and a root label ∼ y -equivalent to b. If both the left and right subtrees have delayed type y and labels ∼ y -equivalent to b then, by property P2, t is of delayed type x. If the brother of s has delayed type y but a root label c that is not

Let s 1 be a proper subtree satisfying θ y ∧ b and s 2 be a proper subtree satisfying θ z ∧ c. These exist since t satisfies both θ b y and θ c z . Let t 1 be the son of t containing s 1 , similarly we define t 2 for s 2 . By (6), the tree t 1 does not satisfy θ z , while t 2 does not satisfy θ y . Hence it must be the case that

t 1 |= θ y and t 2 |= θ z .
In particular t 1 and t 2 are different subtrees. By a reasoning similar to the one in Lemma 18, one shows that the delayed type and root label of t 1 are y, b and the delayed type and root label of t 2 are z, c. By property P2, the delayed type of the tree t is x.

Lemma 20 Let y,b and z,c be the delayed types and root labels of the left and right subtrees of t. If dtype(y, b, z, c) = x and y, z ∈ A then t |= θ (y,b,z,c) .

Proof

If (z, c) y then z y and an easy analysis shows that t satisfies ϕ b y and hence also θ (y,b,z,c) . A similar reasoning shows that if (y, b) z then t satisfies θ (y,b,z,c) . The last case is when (z, c) y and (y, b) z. But then t satisfies the formula θ b y ∧ θ c z ∧ AG(θ y ∨ θ z ). But Lemmas 19 and 20 are exactly what we need to show that the fork formula defined below satisfies the properties postulated in Lemma 14:

Languages Definable in EX+EF

The last logic we consider in this paper is EX+EF. As in the previous sections, we will present a characterization of languages definable in EX+EF.

For the rest of the section we fix an alphabet Σ along with a Σ-language L and will henceforth omit the L qualifier from notation.

Recall the type reachability quasiorder along with its accompanying equivalence relation ≈, which were defined on p. 7. The ≈-equivalence class of a type α is called here its component. We extend the relation to components by setting:

∆ Γ if α β for some α ∈ ∆ and β ∈ Γ; α Γ if α β for some β ∈ Γ.
We use the standard notational shortcuts, writing ∆ ≺ Γ when ∆ Γ but not Γ = ∆; similarly for α ≺ Γ.

Let Γ be some component and let k ∈ N . The (Γ, k)-view of a tree t is the tree view (Γ, k, t) whose domain is the set of nodes in t at depth at most k and where a node v is labeled by:

• t(v) if v is at depth smaller than k; • type(t| v ) if v is at depth k and type(t| v ) ≺ Γ; • ? otherwise.
Let views(Γ, k) denote the set of possible (Γ, k)-views. The intuition behind the (Γ, k)-view of t is that it gives exact information about the tree t for types which are ≺ smaller than Γ, while for other types it just says "I don't know". The following definition describes languages where this information is sufficient to pinpoint the type within the strongly connected component Γ.

Definition 21 Let Γ be a component and let k ∈ N . The language L is (Γ, k)-solvable if every two trees s and t with types in Γ and the same (Γ, k) view have the same type. The language is k-solvable if it is (Γ, k)-solvable for every component Γ and it is component solvable if it is k-solvable for some k.

It turns out that component solvability is exactly the property which characterizes the languages definable in EX+EF:

Theorem 22 A regular language is definable in EX+EF if and only if it is component solvable.

The proof of both implications in this theorem will be presented in the two subsections that follow.

A Component Solvable Language Is Definable in EX+EF

In this section we show that one can write EX+EF formulas which compute views. Then, using these formulas and the assumption that L is component solvable, the type of a tree can be found.

Fix some k such that L is k-solvable. Let α be a type in a component Γ. We write views(α) to denote set of possible (Γ, k)-views that can be assumed in a tree of type α. By assumption on L being k-solvable, we have:

Fact 23 Let α be a type in component Γ and let t be a tree such that type(t) α. The type of t is α if and only if its (Γ, k)-view belongs to the set views(α).

The following lemma states that views can be computed in EX+EF.

Lemma 24 Suppose that for every type β ≺ Γ, there is a EX+EF formula θ β defining it. Then for every i ∈ N and every s ∈ views(Γ, i) there is a formula ψ s satisfied in exactly the trees whose (Γ, i)-view is s.

Proof

By induction on i.

We define below a set of views which certainly cannot appear in a tree with a type in a strongly connected component Γ: Bad(Γ) = {a[s, t] : s ∈ views(α), t ∈ views(β), where α, β Γ, a[α, β] Γ} ∪ ∪{t : type(t) Γ and dom(t) = { }} Observe that Bad(Γ) is a set of (Γ, k + 1)-views. The following lemma shows that the above cases are essentially the only ones.

Lemma 25 For a tree t and a component Γ, the following equivalence holds:

type(t) Γ iff view (Γ, k + 1, t| v ) ∈ Bad(Γ) for some v ∈ dom(t).

Proof

Both implications follow easily from Fact 23 if one considers the maximal possible node v satisfying the right hand side.

The following lemma completes the proof that L is definable in EX+EF.

Lemma 26 Every type of L is definable in EX+EF.

Proof

The proof is by induction on depth of the type in the quasiorder . Consider a type α and its component Γ. By induction assumption, for all types β ≺ Γ, there is a formula θ β which is satisfied in exactly the trees of type β. Using the θ β formulas and Lemma 24 we construct the following EX+EF formula (recall that AG * is the non-strict version of AG defined on page 13):

θ Γ = AG * t∈Bad(Γ) ¬ψ t .
By Lemma 25, a tree t satisfies θ Γ if and only if type(t) Γ. Once we know that the component of the tree is Γ, we can use Fact 23 to pinpoint the exact type:

θ α = θ Γ ∧ t∈views(α) ψ t .

A Language Definable in EX+EF is Component Solvable

In this section, we are going to show that a language which is not component solvable is not definable in EX+EF. For this, we introduce an appropriate Ehrenfeucht-Fraïsé game, called the EX+EF game, which characterizes trees indistinguishable by EX+EF formulas. The game is played over two trees and by two players, Spoiler and Duplicator. The intuition is that in the k-round EX+EF game, the player Spoiler tries to differentiate the two trees using k moves.

The precise definition is as follows. At the beginning of the k-round game, with k ≥ 0, the players are faced with two trees t 0 and t 1 . If these have different root labels, Spoiler wins. If they have the same root labels and k = 0, Duplicator wins; otherwise the game continues. Spoiler first picks one of the trees t i , with i ∈ {0, 1}. Then he chooses whether to make an EF or EX move. If he chooses to make EF move, he needs to choose some nonroot node v ∈ dom(t i ) and Duplicator must respond with a non-root node w ∈ dom(t 1-i ) of the other tree. If Spoiler chooses to make an EX move, he picks a son v ∈ {0, 1} of the root in t i and Duplicator needs to pick the same son w = v in the other tree. If a player cannot find an appropriate node in the relevant tree, this player immediately looses. Otherwise the trees t i | v and t 1-i | w become the new position and the (k -1)-round game is played.

The modality nesting depth of a formula is defined by induction in the natural fashion. Formulas that correspond to letters have depth zero, the depth of a boolean combination is the maximal depth of the formulas involved, while applying EX or EF to a formula increases the depth by one.

Lemma 27 Duplicator wins the k-round EX+EF game over t 0 and t 1 iff t 0 and t 1 satisfy the same EX+EF formulas of modality nesting depth k.

Proof

A standard proof by induction on k. The case of k = 0 is obvious. Let us assume that we have proved the statement for some k and consider k + 1.

Consider first the left to right implication. We show that if a formula ϕ distinguishes the trees t 0 and t 1 , then a winning strategy for Spoiler can be found. If ϕ distinguishes the trees t 0 and t 1 , then one of its subformulas of the form EXψ or EFψ distinguishes them too. Let us consider the case of EFψ and assume without loss of generality that EFψ holds only in t 0 . This means that there is a nonroot node v 0 in the tree t 0 such that

t 0 | v 0 |= ψ and t 1 | v 1 |= ψ for all nonroot nodes v 1 of t 1
The winning strategy for Spoiler is, of course, to pick an EF move, the tree t 0 and the vertex v 0 . Since ψ is of modality nesting depth k, no matter what vertex v 1 Duplicator picks, Spoiler has -by induction assumption -a winning strategy in the k-round game over the trees t 0 | v 0 and t 1 | v 1 . A similar argument is used when the distinguishing formula is of the form EXψ.

For the right to left implication, we show how to write a distinguishing formula ψ of nesting depth k + 1 based on the assumption that Spoiler wins the k + 1-round game. Consider a winning strategy of Spoiler in this game. We assume without loss of generality that Spoiler chooses the tree t 0 to make his move. Two cases need be considered. The first is when Spoiler chooses an EF move and a subtree t 0 | v 0 . Since his strategy is winning, for every possible choice of a node v 1 in the tree t 1 , the k-round game over the trees t 0 | v 0 and t 1 | v 1 can be won by Spoiler. By induction assumption this means that for every node v 1 in the tree t 1 , there is a formula ψ v 1 of nesting depth k such that

t 0 | v 0 |= ψ v 1 and t 1 | v 1 |= ψ v 1 .
Note that in order to have ψ v 1 satisfied in t 0 | v 0 and not in t 1 | v 1 , we may have negated the formula from the induction assumption. Let ψ be a conjunction of all the ψ v 1 formulas for all choices of v 1 . The appropriate formula that distinguishes the trees t 0 and t 1 is then EFψ. A similar reasoning is used for EX.

A multicontext is like a context but it may have more than one hole. Given a multicontext C and a function ν which to every hole in C assigns a tree, we define the tree C[ν] in the natural way. Similarly we proceed when ν assigns types instead of trees: in this case C[ν] is a type. The hole depth of a multicontext C is the minimal depth of a hole in C.

For two types α, β in a component Γ we define an (α, β)-context to be a multicontext C with holes V such that there are two valuations ν α , ν β : The following lemma concludes the proof that no EX+EF formula can recognize a language which is not component solvable:

V → Γ giving the types C[ν α ] = α and C[ν β ] = β. A multicontext C is k-bad for component Γ if it
Lemma 29 If L is not component solvable then for every k there are trees s ∈ L and t ∈ L such that Duplicator wins the k-round EX+EF game over s and t.

Proof

Take some k ∈ N . If L is not component solvable then, by Lemma 28, there is a multicontext C which is k-bad for some component Γ. Let V = {v 1 , . . . , v n } be the holes of C, let ν α , ν β : V → Γ be the appropriate valuations and α = C[ν α ], β = C[ν β ] the resulting types. We will use this multicontext to find trees s ∈ L and t ∈ L such that Duplicator wins the k-round EX+EF game over s and t.

Since all the types used in the valuations ν α and ν β are from same component, there are contexts

C α 1 [], . . . , C α n [] and C β 1 [], . . . , C β n [] such that C α i [α] = ν β (v i ) C β i [β] = ν α (v i ) for all i ∈ {1, . . . , n}.
This means there are two contexts D α and D β with n holes each, such that: 1) D α and D β agree over nodes of depth less than k; 2) when all holes of D α are plugged with β, we get the type α; and 3) when all holes of D β are plugged with α, we get the type β. These are obtained by plugging the appropriate "translators" C α i [] and C β i [] into the holes of the multicontext C. Let t 0 be some tree of type α. The trees t j for j > 0 are defined by induction as follows: The winning strategy for Duplicator is obtained by following an invariant. This invariant is a disjunction of three properties, one of which always holds when the i-round game is about to be played:

t 2i+1 = D β [
1. The two trees are identical;

2. The two trees are s| v and t| v for some |v| ≤ ki;

3. The two trees are

t m | v and t m-2 | v for m ≥ k + i + 1 and v ∈ dom(D α ) if m is even; v ∈ dom(D β ) if m is odd.
The invariant holds at the beginning of the first round, due to 2, and one can verify that Duplicator can play in such a way that it is satisfied in all rounds. Item 2 of the invariant will be preserved in the initial fragment of the game when only EX moves are made, then item 3 will hold until either the game ends or item 1 begins to hold.

Decidability

In this section we round up the results by showing that our characterizations are decidable.

Theorem 30

It is decidable in time polynomial in the number of types if a language is definable in any one of the logics EX, EF or EX+EF.

Proof

Using a simple dynamic algorithm, one can compute in polynomial time all tuples (α, β, α , β ) such that for some context

C[], C[α] = α and C[β] = β .
Using this, we can find in polynomial time:

• Whether L contains an {α, β}-loop;

• The L and ≈ L relations on types.

Since the delayed type of a tree depends only on the types of its immediate subtrees, the number of delayed types is polynomial in the number of types. The relation L on delayed types can then be computed in polynomial time from the relation L . Having the relations L and L , one can check in polynomial time if L is EF-admissible.

This, along with the characterizations from Theorems 3 and 5, proves decidability for the logics EX and EF. The remaining logic is EX+EF.

By Theorem 22, it is enough to show that component solvability is decidable. In order to do this, we present an algorithm that detects if a given component Γ admits bad multicontexts of arbitrary size, cf. Lemma 28. Fix a component Γ. We define by induction a sequence B i of subsets of Γ × Γ.

• B 0 consisits of all pairs (α, β) such that α, β ∈ Γ and α = β. The sequence B i is decreasing so it reaches a fix-point B ∞ in no more than |Γ| 2 steps. The following lemma yields the algorithm for EX+EF:

Lemma 31 Γ admits bad multicontexts of arbitrary size iff B ∞ = ∅.

For the left-to-right implication suppose that B ∞ is not empty. By induction on k we show that for every k and (α, β) ∈ B ∞ , we can construct (α, β)-context of hole depth k. Take (α, β) ∈ B ∞ . We have one of the two cases from the definition above. The first is when there are a pair (α , β ) ∈ B ∞ , a type γ Γ and a letter a ∈ Σ such that type(a[α , γ ]) = α and type(a[β , γ ]) = β. By induction assumption we have an (α , β )-context C of hole depth k -1. Using this multicontext, we construct the multicontext a[C , s], where s is a tree of type γ. It is a required (α, β)-context of hole depth k. The other case is similar.

For the right-to-left implication we show that if (α, β) ∈ B i -B i+1 then all (α, β)-contexts have hole depth bounded by i. This is also done by induction on i.

Corollary 32 If the input is a CTL formula or a nondeterministic tree automaton, all of the problems in Theorem 30 are Exptime-complete.

Proof

Since, in both cases, the types can be computed in time at most exponential in the input size, the Exptime membership follows immediately from Theorem 30. For the lower bound, we will use an argument analogous to the one in [START_REF] Walukiewicz | Deciding low levels of tree-automata hierarchy[END_REF], reducing the Exptime-hard universality problems for both CTL [START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF] and nondeterministic automata [START_REF] Seidl | Deciding equivalence of finite tree automata[END_REF] to any of these problems.

We will only show here the Exptime-hardness of the problem:

Is a given CTL formula equivalent to one in EF? (*)

Let ψ be a CTL formula over some alphabet Σ. By [START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF], the question whether ψ is satisfied in all Σ-trees is Exptime-hard. We show the Exptimehardness of the problem (*) by presenting a formula ϕ which is definable in the logic EF if and only if the formula ψ is true in all Σ-trees. This formula is obtained by using ψ and some fixed formula φ -say, E(aUb) -not definable in EF:

ϕ = EX 0 ψ ∨ EX 1 φ
Clearly if ψ is true in all Σ-trees, then, by its first disjunct, ϕ is true in all Σ-trees with more than one node. This language is defined by the EF formula EX . Finally, we need to prove that if ψ is not true in all Σ-trees, then ϕ is not definable in EF. Let us assume for the sake of contradiction that ϕ is equivalent to some EF formula θ. Let Ψ be all the subformulas of θ. By assumption that the formula φ is not definable in EF, there exist two trees t 1 and t 2 that satisfy the same formulas in Ψ, but one satisfies φ and the other does not (otherwise an appropriate boolean combination of formulas in Ψ would be equivalent to φ). Therefore exchanging t 1 with t 2 in any subtree does not affect the satisfaction of θ. Let s be a tree that does not satisfy ψ, obtained by the assumption on ψ not being satisfied in all Σ-trees. Obviously for any letter a ∈ Σ we have

a[s, t 1 ] |= ϕ a[s, t 2 ] |= ϕ ,
but either both these trees satisfy θ or both do not.

6 Why Forbidden Patterns from the Word Case Do not Work

In the survey [START_REF] Wilke | Classifying discrete temporal properties[END_REF], one can find decidable characterizations for several fragments of LTL. These fragments can be seen as the word equivalents of the logics EX, EF and EX+EF considered here. One naturally asks the question: how are the word and tree cases related? In the case of the logic EX, the loop characterization from Theorem 3 is an exact analogue of the characterization corresponding to the fragment of LTL that only uses the X modality.

For the two remaining logics, however, the word and tree cases diverge. This section is devoted to showing why.

Case of EF. First we need to introduce the appropriate definitions for words. The delayed type of a word w is the function which assigns to a letter a the type of the word a • w. Two word types α, β are in the same component if there are word types α , β such that α • α = β and β • β = α. In [START_REF] Wilke | Classifying discrete temporal properties[END_REF] it is shown that a word language is definable using only the modality F if and only if the delayed type of a word is determined by the component of its type.

Hence a natural question: is a tree language definable in EF if and only if the delayed type of a tree is determined by the components of its two sons? This can be understood in two ways: the ordered pair of components, or the set of components. The first idea can be immediately disproved, for instance using the language "there is an a in the left subtree". The idea that uses sets requires a more elaborate example, which is presented here. A tree t satisfies this formula if it contains two nodes v and w which are siblings and t| v contains only a's, while t| w contains both a's and b's. This language has four types α, β, γ and , which are defined by the formulas: Each of these types is its own component. There are also four delayed types {x + , x a , x b , x γ }, which are defined in Figure 3.

Consider now the two trees s and t drawn in Figure 3 (we do not specify the root letters since we are interested only in delayed types). These trees show that the language L is not typeset dependent and therefore not in EF, since: TS(s) = TS(t) = {α, β, γ} but x γ = dtype(s) = dtype(t) = x + .

However, if the components of both sons are known, then the types of both sons are known and hence so is the delayed type of the tree.

Case of EX+EF. In [START_REF] Wilke | Classifying discrete temporal properties[END_REF] it is shown that a word language is definable using the modalities F and X if and only if one cannot find two distinct types α, β in the same component and a nonempty word w such that:

α = w • α and β = w • β. (7)
We will show that a straightforward generalization of this condition obtained by considering contexts instead of words does not work in the tree case. Consider the language K over the alphabet {a, b, c} defined by the formula This language consists of those trees where for every node v, all the minimal nodes in the set {w : w > v and t(w) = t(v)} have the same label. The ten types of the language are: 0 = ¬ψ; α σ = σ∧AX⊥; β σ,τ = ψ∧ψ σ,τ for all σ = τ ∈ {a, b, c}.

There are five components in this language: a component Γ containing the six β σ,τ types, while each of the remaining types is its own component. The language K is not k-solvable for any k ∈ N , and hence is not definable in EX+EF. We will show, however, that if in the condition (7) one considers nontrivial contexts instead of nonempty words w, the resulting condition on tree languages is satisfied by K. This goes to show that in a bad multicontext one sometimes needs the use of more than one hole.

Let C[] be a nontrivial context, i.e. one with the hole not in the root. We will show that one cannot find two distinct types in the component Γ such that

C[γ 1 ] = γ 1 and C[γ 2 ] = γ 2 . ( 8
)
Let σ be the letter in the parent v of the hole, and let w be the brother of the hole. Let V = {u : u ≥ w and C(u) = σ}. If V = ∅, or nodes in V have two different labels, then C[γ] = 0 for all types γ. Otherwise, let τ be the unique label of all nodes in V . This means that for any tree t, the type in v of C[t] is either 0 or β σ,τ , which proves that (8) cannot be satisfied.

Open Problems

This paper solves the question of definability for the logics EX, EF and EX+EF. One possible continuation are logics where instead of EF we use the non-strict modality EF * . The resulting logics are weaker than their strict counterparts (for instance the language EFa is not definable using only EF * ) and therefore decidability of the their definability problems can be investigated.

Another question is what happens if we enrich these logics with past quantification (there exists a point in the past)? This question is particularly relevant since the resulting logics are related to first-order logic with two variables.

Finally, there is CTL (and of course CTL * ). Providing a decidable characterization of CTL would be a valuable achievement, since this is a widely used logic. Note that on words CTL collapses to LTL and hence first-order logic, so such a characterization would subsume first-order definability for words.

Figure 1 :

 1 Figure 1: The tree t i+1 .

  By property P3 we get dtype(y, b, z, c) = dtype(y, b, y, b) and consequently dtype(y, b, y, b) y. As is a partial order by P1 and since y dtype(y, b, y, b) holds by definition, we get dtype(y, b, y, b) = y. Hence b belongs to set N y of neutral letters of y.

  (i) The pair (y, b) is sufficient and (z, c) y holds (or the other way round); (ii) Neither (y, b) nor (z, c) is sufficient but dtype(y, b, z, c) = x.

  ∼ y -equivalent to b then c must belong to N y , because AG(θ y ⇒ (b ∨ N y )) holds. By definition of N y we have (y, c) y. By property P3 we get dtype(y, b, y, c) = dtype(y, b, y, b) = x. Otherwise, by AGθ y , the brother of s is of delayed type z y and has a root label c such that (z, c) y (because AG(θ y ⇒ θ y ) holds). By property P3 dtype(y, b, z, c) = dtype(y, b, y, b) = x. Given two delayed types y, z ∈ A and letters b, c ∈ Σ, we define ϕ (y,b,z,c) , b) z and not the above; θ b y ∧ θ c z ∧ AG(θ y ∨ θ z ) otherwise. Note that this formula corresponds to the two cases (i) and (ii) described before Lemma 18. Lemma 19 If dtype(y, b, z, c) = x and a tree t satisfies ϕ (y,b,z,c) , then its delayed type is x. Proof If (z, c) y then by property P3, the pair (y, b) is sufficient and the lemma follows from Lemma 18. Similarly if (y, b) z. It remains to consider the case when (z, c) y and (y, b) z .

  ∧ {ϕ (y,b,z,c) : x = dtype(y, b, z, c)}

  n times t 2i , . . . , t 2i ] t 2i+2 = D α [ n times t 2i+1 , . . . , t 2i+1 ]. By an obvious induction, all the trees t 2i have type α and all the trees t 2i+1 have type β. As β = α, there exists a context D[] such that D[α] ∈ L and D[β] ∈ L (or the other way round).

Figure 2 :

 2 Figure 2: The tree t 2i+2 . To finish the proof of the lemma, we will show that Duplicator wins the k-round EX+EF game over the trees s = D[t 2k+2 ] and t = D[t 2k+1 ] .

•

  A pair (α, β) belongs to B i+1 if it belonged to B i and either there are a pair (α , β ) ∈ B i , a type γ Γ and a letter a ∈ Σ such that type(a[α , γ]) = α and type(a[β , γ]) = β ; or -there are pairs (α , β ), (α , β ) ∈ B i and a letter a ∈ Σ such that type(a[α , α ]) = α and type(a[β , β ]) = β .

Figure 3 :

 3 Figure 3: The delayed types of L along with the trees s and t Consider the {a, b}-language L defined by the formula (which uses the non-strict versions of AG and EF): ψ = EF * [EX(AG * a) ∧ EX((EF * a) ∧ (EF * b))]

α

  = AG * a; β = AG * b; γ = (EF * a) ∧ (EF * b) ∧ ¬ψ; + = ψ.

ψ

  = AG * σ =τ ∈{a,b,c} ψ σ,τwhereψ σ,τ = [EX ⇒ (σ ∧ A(σUτ ))] .

  has hole depth at least k and is an (α, β)-context for two different types α, β ∈ Γ. The following Lemma shows that (α, β)-contexts are just a reformulation of component solvability: Lemma 28 L is not component solvable if and only if for some component Γ and every k ∈ N , it contains multicontexts which are k-bad for Γ.ProofA k-bad context exists for Γ if and only if L is not (Γ, k)-solvable.


Lucas Matana Luza

Annachiara Ruospo
email: annachiara.ruospo@polito.it

Alberto Bosio
email: alberto.bosio@ec-lyon.fr

Ernesto Sanchez
email: ernesto.sanchez@polito.it

Luigi Dilillo
email: dilillo@lirmm.fr

A Model-Based Framework to Assess the Reliability of Safety-Critical Applications

Keywords: safety-critical applications, reliability, approximate computing, neural network, fault injection

Solutions based on artificial intelligence and brain-inspired computations like Artificial Neural Networks (ANNs) are suited to deal with the growing computational complexity required by state-of-the-art electronic devices. Many applications that are being deployed using these computational models are considered safety-critical (e.g., self-driving cars), producing a pressing need to evaluate their reliability. Besides, state-of-the-art ANNs require significant memory resources to store their parameters (e.g., weights, activation values), which goes outside the possibility of many resourceconstrained embedded systems. In this light, Approximate Computing (AxC) has become a significant field of research to improve memory footprint, speed, and energy consumption in embedded and high-performance systems. The use of AxC can significantly reduce the cost of ANN implementations, but it may also reduce the inherent resiliency of this kind of application. On this scope, reliability assessments are carried out by performing fault injection test campaigns. The intent of the paper is to propose a framework that, relying on the results of radiation tests in Commercial-Off-The-Shelf (COTS) devices, is able to assess the reliability of a given application. To this end, a set of different radiation-induced errors in COTS memories is presented. Upon these, specific fault models are extracted to drive emulation-based fault injections.

I. INTRODUCTION

Today, a wide variety of application domains requires smarter electronic devices and high-performance computing systems. Solutions based on artificial intelligence and brain-inspired computations like Artificial Neural Networks (ANNs) are suited to cope with this growing computational complexity. For their outstanding computational capabilities, ANNs are being increasingly deployed in many application domains. Many of these are considered safety-critical due to the gravity that a failure could cause. One peculiar characteristic of these brain-inspired models is their intrinsic robustness. Despite the claimed built-in robustness of ANNs [START_REF] Torres-Huitzil | Fault and error tolerance in neural networks: A review[END_REF], there is a pressing need for evaluating their reliability, especially if they are deployed on resource-constrained hardware devices for safety-critical applications. More precisely, it is essential to evaluate whether a hardware or software fault may cause a system failure. In parallel with reliability assessment, a lot of effort has been made to reduce the memory and energy footprint of ANNs, for instance, by leveraging on reduced bit-width data type in either training or inference phase. It is crucial to cope with the emerging trend towards deploying ANNs on resource-constrained hardware implementations that are fast and ultra-low-power, optimised for solving specific tasks. This contrasts with the trend that sees the growing complexity of the state-of-the-art ANNs that can require some kB or MB of memory for storing their parameters. In this light, Approximate Computing (AxC) has become a significant field of research to improve memory footprint, speed, and energy consumption in embedded and high-performance systems [START_REF]A survey of techniques for approximate computing[END_REF]. By relaxing the need for fully precise or completely deterministic operations, AxC substantially improves energy efficiency and reduces the memory requirement. The use of AxC can significantly reduce the cost of ANN implementations, but it may also reduce the inherent resiliency of this kind of application, which can be more prone to errors due to external perturbation (e.g., radiation harsh environment like space). The radiation-induced effects may be amplified by the AxC techniques, which can result in unacceptable outputs. On this scope, reliability assessments are carried out by performing fault injection campaigns. Depending on how faults are injected and at which abstraction level, several methodologies can be drawn. The most precise but also costly in terms of hardware resources and exposure time is radiation tests.

The main intent of the paper is to bring a framework to enable the reuse of results from radiation test campaigns in Commercial-Off-The-Shelf (COTS) devices. The reuse of the results is reached with a detailed evaluation of the radiation-induced faults. It is possible to define realistic fault models used to assess the reliability of a given application through a model-based fault injection when emulating its functionality. The ultimate goal is to use the proposed framework for quick but still accurate reliability estimation of approximate ANNs to be deployed in resourceconstrained hardware devices for safety-critical applications.

The rest of the paper is organised as follows. Section II presents different AxC techniques and related works. Section III presents the proposed framework by targeting the transition from a radiation-based fault-injection to a model-based one using realistic fault models extracted from the radiation test campaigns. Finally, Section IV concludes the paper.

II. APPROXIMATE COMPUTING TECHNIQUES

AxC techniques provide a set of design choices for a performance-accuracy trade-off evaluation, bringing the possibility to enhance, for example, speed, energy efficiency, and memory usage, at the cost of reducing the accuracy constraints at different levels of abstractions [START_REF] Han | Approximate computing: An emerging paradigm for energy-efficient design[END_REF]. Some techniques are explored in the following subsections.

A. Voltage and Frequency Scaling

Voltage scaling is a technique that aims at reducing a supply voltage level at the cost of impacting the computation timing of processing blocks or even affecting the accuracy of the final result of an application [START_REF] Chippa | Scalable effort hardware design[END_REF]. In [START_REF] Mauro | Always-on 674µW@4GOP/s error resilient binary neural networks with aggressive SRAM voltage scaling on a 22-nm IoT end-node[END_REF], by exploring the inherent noise resilience of binary neural networks and over scaling the supply voltage of the memories used in the implemented system-on-chip (SoC) at the cost of 1% of classification accuracy degradation. Furthermore, the voltage scaling may reduce the voltage threshold that is used to define the logical '1' or '0', which can result in data cells becoming stuck at a logical value or even increasing the probability of soft error occurrence, leading to a degradation in the hardware reliability and even affecting the data precision [START_REF] Chandra | Impact of technology and voltage scaling on the soft error susceptibility in nanoscale CMOS[END_REF].

Besides the clock frequency scaling that can be applied alongside the supply voltage scaling (as shown with the DVFS technique), another approach is reducing the execution rate of systematic operations. In [START_REF] Ganapathy | Approximate computing with unreliable dynamic memories[END_REF], this technique is explored by means of reducing the refresh frequency of an embedded DRAM (eDRAM) implemented in a SoC. In [START_REF] Raha | Quality-aware data allocation in approximate DRAM*[END_REF], authors propose the use of sub-optimal refresh rates on DRAM by applying a quality-aware approximate system, where, based on characterisations testes, the critical data is allocated in physical pages where the number of errors generated by the sub-optimal refresh rates is low.

B. Data Precision Reduction

The memory footprint can be directly reduced by changing the data representation of the parameters (e.g., weights, activations) of an ANN implementation. Reducing memory footprint can lead to a reduction in the energy consumption of the implementation since there is a decrease in the amount of data transferred from/to the memory [START_REF] Rodrigues | Survey on approximate computing and its intrinsic fault tolerance[END_REF]. Methods of reducing the floating-point precision, or even the bit-width used for data representation, can significantly reduce the energy consumption with a cost of degradation in the outcomes of an application [START_REF] Rubio-Gonz Ález | Precimonious: Tuning assistant for floating-point precision[END_REF]. In [START_REF] Hsiao | Energy-aware hybrid precision selection framework for mobile GPUs[END_REF], the authors present a framework to integrate the use of fixed-point data representation and a reduction in the floating-point data representation to improve the energy efficiency in mobile GPUs, reaching a reduction of about 30% with acceptable degradation in the rendered images. Reducing the bit-width of the adopted data representation can also improve the robustness of the neural network, as demonstrated in [START_REF] Ruospo | Evaluating convolutional neural networks reliability depending on their data representation[END_REF]. The implementation of these techniques are not restricted to software-based implementations but also can be implemented at the hardware level and directly in FPGA (Field Programmable Gate Array) applications. This type of improvement on hardware projects does not directly impact the software level positively. From one side, with FPGA implementations, area and energy costs can be reduced by implementing mathematical functions (e.g., logarithms). However, it can increase the application execution time at the software level, in which the data handling and operations are implemented [START_REF] Pandey | An FPGA-based fixed-point architecture for binary logarithmic computation[END_REF].

III. PROPOSED FRAMEWORK

We propose a framework to assess the reliability of AxC on ANN-based applications, enabling the trade-off estimation between the impact of radiation-induced faults and resource usage in terms of hardware and software on these applications. The proposed framework enables the use of fault models extracted from the characterisation of COTS memories in conjunction with the target environment conditions (e.g., radiation type, flux, and dose) to analyse the different scenarios regarding the reliability of the system. The idea is based on three steps: radiation-based fault injection, fault model evaluation, model-based fault injection.

A. Radiation-Based Fault Injection

Radiation-based fault injections aim at characterising a device or application and validate predictive models of events produced by the impact of ionising particles (e.g., neutrons, alphas, heavy ions, protons) on a given electronic device. The reliability assessment is carried out on the actual platform during the radiation test campaign.

One common outcome is the evaluation of Single-Bit Upsets (SBUs) due to the radiation effects. Also, Single-Event Latch-Up (SEL) may occur in the device. This kind of event can lead to permanent damage, affecting not only the memory array but also its controller part. The SEL can be observable by a sudden increase in the nominal supply current [START_REF] Gaillard | Single event effects: Mechanisms and classification[END_REF].

Moreover, in [START_REF] Nicolaidis | Stuck and weakened SDRAM cells due to heavy-ion irradiation[END_REF], the authors spotted that the retention time of a COTS DRAM memories has a significant decrease when exposed to ion irradiation. This characteristic plays an important role when scaling the refresh rate once the retention capability of the cells will decrease, and the downscaled refresh rate will be not reliable when the system is exposed to a harsh environment containing this type of particle.

Furthermore, supplementary to the device characterisation, the reliability assessment directly in the application can be explored by radiation test at both hardware and software level. Several works have been published on this scope. In [START_REF] Luza | Investigating the impact of radiation-induced soft errors on the reliability of approximate computing systems[END_REF], the authors studied the radiation-induced soft-errors based on AxC techniques applied to the data representation of weights in a Convolutional Neural Network (CNN). Withal, by using an accelerated neutron beam to inject transient errors and fault injection experiments for permanent errors, the reliability of a 54-layer CNN is assessed by exposing the entire GPU to the radiation source [START_REF] Lotfi | Resiliency of automotive object detection networks on GPU architectures[END_REF].

B. Fault Model Evaluation

Radiation-based fault injection exposed the system to similar conditions of an in-field application, e.g., space applications. From the radiation tests, it is possible to evaluate the electronic device by identifying the types of the generated faults and their frequency and appearance conditions. Based on the research group activities, several types of memories were already exposed to different radiation sources. In [START_REF] Dilillo | Soft errors in commercial off-the-shelf static random access memories[END_REF], the authors review the techniques and results of several radiation test campaigns on two commercial SRAMs (90 nm and 65 nm) technology nodes. Moreover, the effects on a SLC (Single Level Cell) NAND Flash under heavy-ions and proton irradiation were evaluated in [START_REF] Luza | Effects of heavy ion and proton irradiation on a SLC NAND Flash memory[END_REF]. Also, in [START_REF] Bosser | Single-event effects from space and atmospheric radiation in memory components[END_REF], several tests on a MRAM show that the memory is prone to suffering from SELs. Studies on these memories show that SEEs can occur in different ways, such as SBUs, Multiple Cell Upsets (MCUs), Single-Event Functional Interruptions (SEFIs), or SELs, and it generates different kinds of fault behaviours on the devices.

From recognizing the different types of errors and identifying the occurrences of each one, the estimated event cross section provides the probability of its occurrences in a given scenario. The cross section is defined as

σ bit = N F × M ( 1
)
where N is the number of events, F is the beam fluence in n/cm 2 , and M is the number of bits [START_REF] Petersen | Single Event Effects in Aerospace[END_REF].

C. Model-Based Fault Injection

Based on the radiation-induced soft errors, the model-based fault injection is proposed as a case study, where it is shown the main ideas to enable the injection of realistic fault models during the simulation or emulation of a target application. In order to define the scope, the next steps are based on neutron irradiation on a COTS self-refresh DRAM memory (results can be explored in more details in [START_REF] Luza | Effects of thermal neutron irradiation on a self-refresh DRAM[END_REF]), and the reliability assessment is based on the injection of realistic faults extract from this test campaign in applications that may use this memory to run. Then, starting from the radiation test campaigns, based on the results presented in [START_REF] Luza | Effects of thermal neutron irradiation on a self-refresh DRAM[END_REF], it was defined the cross sections for three different types of errors that were identified: SBUs, stuck-at bits, and block errors. From the estimated cross sections, we can define the E-SER (Execution Soft Error Rate), which provides the expected amount of events within a run of the defined application. The equation is:

E -SER = σ bit × M × φ × t (2)
where σ bit is the calculated cross section (cm 2 /bit), M is the memory size in bits used by the application (stored in the target), φ is the average neutron flux (n/cm 2 /s) of the target environment, and t is the application execution time in seconds.

A case study is proposed by using the CNN LeNet-5 [START_REF] Lecun | Gradient-based learning applied to document recognition[END_REF] as the application target. The trained network was exported as C code using three different data representations for the weights: the accurate network having 32-bit floating-point real numbers (Float 32), and two approximated versions: a 16-bit integer quantised CNN (Int 16), and an 8-bit integer quantised CNN (Int 8). The three replicas were then ported to an embedded system using an SoC, which provides an ARM Cortex ™ A9 processor attached to a 28 nm Artix ® 7 FPGA. This platform was then implemented to have the HyperRAM memory allocating the weights of the CNN. From this implementation, we extract two parameters used by the E-SER equation. The allocated resources in the HyperRAM memory gives us the M . Furthermore, by running the application for the determined quantity of inferences (1,000 images), we extracted t.

The estimated E-SER for the three different versions were calculated with the cross sections defined in [START_REF] Luza | Effects of thermal neutron irradiation on a self-refresh DRAM[END_REF], with an average flux of 5 × 10 As explored in the previous sections, the radiation-induced errors in memories can be seen in different ways, from just SBUs up to errors spanning a significant range of addresses. A model-based fault injection must take into account its differences. From the three types of errors that were identified in [START_REF] Luza | Effects of thermal neutron irradiation on a self-refresh DRAM[END_REF], the SBUs are the simplest ones to be injected on a target application since they can be injected on random addresses of the target memory accordingly the calculated E-SER. Stuck-at faults also occurred in random addresses, but two characteristics should be taken into account for this type of errors: it presented an intermittent behaviour that should be explored by defining a behavioural equation based on the number of occurrences for each bit address, and the injected faults may be permanent and not recoverable. Finally, block errors have shown normally a faulty address pattern when analysed by logical bitmaps. Then, the block error model should take into account its shape and size, as well as its behaviour, once write operations is generally capable of restoring the cells access.

From these assumptions, an emulator can be designed based on two processes. The application process is responsible for running the target neural network, and the injector process is responsible for introducing errors in memory locations. Both processes are executed in parallel and share the same memory resources, which should be implemented with concurrency control mechanisms. The E-SER and the fault models should be provided, and the injector process will use these inputs to determine where and when a fault should be injected into the running application. Fig. 1 depicts a top-level diagram of the emulator.

IV. CONCLUSION

In this work, we presented a framework to assess the reliability of approximate computing applications. The framework leverages the results from radiation tests in COTS devices to assess a given application's reliability. We presented radiation-induced errors targeting COTS memories, which can be just SBUs and stuck-at bits, including events that generate errors spanning a significant range of addresses. This paper also highlighted that the errors could appear in different manners and with different behaviours. Finally, it is presented an emulator architecture aimed at injecting the extracted fault models into a specific application. We explored the use of previous results to enable the reliability assessment by proposing a case study. In the future, the group's target aims to use the framework to deploy an emulator capable of handling and injecting the defined fault models. They will be used to estimate the reliability of approximate ANNs.

TABLE I ESTIMATED

 I EVENT RATE FOR THE THREE DIFFERENT CNN VERSIONS.

	CNN		E-SER [events/run]
	version	SBUs	Stuck-at bits	Block errors
	Float 32	1.04	0.53	0.40
	Int 16	0.30	0.15	0.21
	Int 8	0.10	0.05	0.13

  6 n/cm2 /s. The memory usage was approximately 4 Mb for Float 32, 2 Mb for Int 16 and 1 Mb for Int 8 with respect to the network weights. The execution time was approximately 1800 s for Float 32, 960 s for Int 16, and 600 s for Int 8. The estimated E-SER are presented in Tab. I.

This study has been achieved thanks to the financial support of the VAN ALLEN Foundation (Contract No. UM 181387) and the Region Occitanie (Contract No. UM 181386), and by the projects "IDEX Lyon OdeLe" and "ReACT".