Michele Pagani
email: michele.pagani@pps.univ-paris-diderot.fr

Christine Tasson
email: christine.tasson@pps.univ-paris-diderot.fr

Lionel Vaux
email: lionel.vaux@univ-amu.fr

Strong Normalizability as a Finiteness Structure via the Taylor Expansion of λ-terms

published or not. The documents may come

Strong Normalizability as a Finiteness Structure via the

Taylor Expansion of λ -terms

Introduction

It is well-known that sets and relations can be presented as a category of modules and linear functions over the boolean semi-ring, giving one of the simplest semantics of linear logic. In [START_REF] Lamarche | Quantitative domains and infinitary algebras[END_REF] (see also [START_REF] Laird | Weighted relational models of typed lambda-calculi[END_REF]), it is shown how to generalize this construction to any complete 3 semi-ring R and yet obtain a model of linear logic. In particular, the composition of two matrices φ ∈ R A×B and ψ ∈ R B×C is given by the usual matrix multiplication:

(φ; ψ) a,c : = b∈B φ a,b • ψ b,c (1)
The semi-ring R must be complete because the above sum might be infinite. This is an issue, because it prevents us from considering standard vector spaces, which are usually constructed over "non-complete" fields like reals or complexes.

In order to overcome this problem, Ehrhard introduced the notion of finiteness space [START_REF] Ehrhard | Finiteness spaces[END_REF]. A finiteness space is a pair of a set A and a set A (called finiteness structure in Definition 7) of subsets of A which is closed under a notion of duality. The point is that, for any field K (resp. any semi-ring), the set of vectors in K A whose support 4 is in A constitutes a vector space (resp. a module) over K. Moreover, any two matrices φ ∈ K A×B and ψ ∈ K B×C whose supports are in resp. A B and B C (the finiteness structures associated with the linear arrow) compose, because the duality condition on the supports makes the terms in the sum of Equation (1) be zero almost everywhere. This gives rise to a category which is a model of linear logic and its differential extension.

The notion of finiteness space seems strictly related to the property of normalization. Already in [START_REF] Ehrhard | Finiteness spaces[END_REF], it is remarked that the coKleisli category of the exponential comonad is a model of simply typed λ-calculus, but it is not cpo-enriched and thus cannot interpret (at least in a standard way) fixed-point combinators, so neither PCF nor untyped λ-calculus. Moreover, in the setting of differential nets, Pagani showed that the property of having a finitary interpretation corresponds to an acyclicity criterion (called visible acyclicity [START_REF] Pagani | Visible acyclic differential nets, part I: Semantics[END_REF]) which entails the normalization property of the cut-elimination procedure [START_REF] Pagani | The Cut-Elimination Thereom for Differential Nets with Boxes[END_REF], while there are examples of visibly cyclic differential nets which do not normalize.

The goal of this paper is to shed further light on the link between finiteness spaces and normalization, this time considering the non-deterministic untyped λ-calculus. Since we deal with λ-terms and not with linear logic proofs (or differential nets), we will speak about formal power series rather than matrices at the semantical level. This corresponds to move from the morphisms of a linear category to those of its coKleisli construction. Moreover, following [START_REF] Ehrhard | Uniformity and the Taylor Expansion of Ordinary Lambda-Terms[END_REF], we describe the monomials of these power series as resource terms in normal form. The benefit of this setting is that the interpretation of a λ-term M as a power series [|M |] can be decomposed in two distinct steps: first, the term M is associated with a formal series M * of resource terms possibly with redexes, called the Taylor expansion of M (see Table 1a); second, one reduces each resource term t appearing in the support T (M ) of M * into a normal form NF(t) and sum up all the results, that is (M * t denotes the coefficient of t in M * ):

[|M |] = t∈T (M ) M * t • NF(t) (2)
The issue about the convergence of infinite sums appears in Equation (2) because there might be an infinite number of resource terms in T (M ) reducing to the same normal form and thus possibly giving infinite coefficients to the formal series [|M |]. Ehrhard and Regnier proved in [START_REF] Ehrhard | Uniformity and the Taylor Expansion of Ordinary Lambda-Terms[END_REF] that this is not the case for deterministic λ-terms, however the situation gets worse in presence of nondeterministic primitives. If we allow sums M +N representing potential reduction to M or N , then one can construct terms evaluating to a variable y an infinite number of times, like (where Θ denotes Turing's fixed-point combinator):

(Θ) λx.(x + y) → * β (Θ) λx.(x + y) + y → * β (Θ) λx.(x + y) + y + y → * β . . . (3)
We postpone to Examples 1 and 4 a more detailed discussion of (Θ) λx.(x + y), however we can already guess that this interplay between infinite reductions and non-determinism may produce infinite coefficients. One can then wonder whether there are interesting classes of terms where the coefficients of the associated power series can be kept finite. Ehrhard proved

M is SN M typable in System D+ T (M ) ∈ (T) ⊥ ∀t ∈ ∆, NF(T (M ))t is finite Th. 14 Cor. 30 if T ⊆ B if L ⊆ T Th. 36 if ∆ = T Lem. 38
Fig. 1: main results of the paper in [START_REF] Ehrhard | A finiteness structure on resource terms[END_REF] that the terms typable by a non-deterministic variant of Girard's System F have always finite coefficients. A by-product of our results is Corollary 39, which is a generalization of Ehrhard's result: every strongly normalizable nondeterministic λ-term can be interpreted by a power series with finite coefficients.

The main focus of our paper is however in the means used for obtaining this result rather than on the result itself. The proof in [START_REF] Ehrhard | A finiteness structure on resource terms[END_REF] is based on a finiteness structure S over the set of resource terms ∆, such that any term M typable in System F has the support T (M ) of its Taylor expansion in S. We show that this method can be both generalized and strengthened in order to characterize strong normalization via finiteness structures. Namely, we give sufficient conditions on a finiteness structure S over ∆ such that for every non-deterministic λ-term M : (i) if M is strongly normalizable, then T (M ) ∈ S (Corollary 30); (ii) if T (M ) ∈ S, then M is strongly normalizable (Theorem 36).

Contents. Section 2 gives the preliminary definitions: the non-deterministic λcalculus, its Taylor expansion into formal series of resource terms and the notion of finiteness structure. The proof of Item (i) splits into Sections 3 and 4, using an intersection type system (Table 2) for characterizing strong normalization. Section 5 gives the proof of Item (ii) and Section 6 concludes with Corollary 39 about the finiteness of the coefficients of the power series of strongly normalizable terms. Figure 1 sums up the main results of the paper.

Preliminaries

Non-deterministic λ-calculus Λ +

The non-deterministic λ-calculus is defined by the following grammar5 :

λ-terms Λ + : M : = x | λx.M | (M ) M | M + M
subject to α-equivalence and to the following identities:

M + N = N + M, (M + N ) + P = M + (N + P ), λx.(M + N ) = λx.M + λx.N , (M + N ) P = (M ) P + (N ) P.
The last two equalities state that abstraction is a linear operation (i.e. commutes with sums) while application is linear only in the function but not in the argument (i.e. (P ) (M + N ) = (P ) M + (P ) N ). Notice also that the sum is not idempotent: M + M = M . This is a crucial feature for making a difference between terms reducing to a value once, twice, more times or an infinite number of times (see the discussion about Equation (3) in the Introduction).

Although this follows an old intuition from linear logic, the first extension of the λ-calculus with (a priori non idempotent) sums subject to these identities was, as far as we know, the differential λ-calculus of Ehrhard and Regnier [5]. This feature is now quite standard in the literature following this revival of quantitative semantics.

The (capture avoiding) substitution of a term for a variable is defined as usual and β-reduction → β is defined as the context closure of:

(λx.M ) N → β M [N/x] .
We denote as → * β the reflexive-transitive closure of → β .

Example 1. Some λ-terms which will be used in the following are:

∆ : = λx. (x) x, Ω : = (∆) ∆, ∆ 3 : = λx. (x) xx, Ω 3 : = (∆ 3 ) ∆ 3 , Θ : = (λxy. (y) (x) xy) λxy. (y) (x) xy.
The term Ω is the prototypical diverging term, reducing to itself in one single β-step. Ω 3 is another example of diverging term, producing terms of greater and greater size:

Ω 3 → β (Ω 3 ) ∆ 3 → β (Ω 3 ) ∆ 3 ∆ 3 → β .
. . It will be used in Remark 37 to prove the subtlety of characterizing strong normalization with finiteness spaces. The Turing fixed-point combinator Θ has been used in the Introduction to construct (Θ) λx.(x + y) as an example of non-deterministic λterm morally reducing to normal forms with infinite coefficients (Equation ( 3)). Notice that, by abstraction linearity, (Θ) λx.(x+y) = (Θ) (λx.x+λx.y), however (Θ) (λx.x + λx.y) = (Θ) λx.x + (Θ) λx.y, because application is not linear in the argument. This distinction is crucial: the latter term reduces to ((Θ) λx.x) + y, with (Θ) λx.x reducing to itself without producing any further occurence of y.

Resource calculus ∆ and Taylor expansion

The syntax. Resource terms and bags are given by mutual induction:

resource terms ∆ :

s : = x | λx.s | s s bags ∆ ! : s : = 1 | s • s
subject to both α-equivalence and permutativity of (•): we most often write [s 1 , . . . , s n ] for [START_REF] Van Bakel | Complete restrictions of the intersection type discipline[END_REF] , . . . , s σ(n) ] for any permutation σ. In other words, bags are finite multisets of terms.

s 1 • (• • • • (s n • 1) • • • ) and then [s 1 , . . . , s n ] = [s σ(
x

* : = x (λx.M ) * : = λx.M * ((M ) N ) * : = n∈N 1 n! M * (N * ) n (M + N ) * : = M * + N * (a) expansion ( ) * : Λ + → Q ∆ T (x) : = {x} T (λx.M ) : = {λx.s; s ∈ T (M )} T ((M ) N ) : = s t; s ∈ T (M ) , t ∈ T (N ) ! T (M + N ) : = T (M ) ∪ T (N ) (b) support T ( ) : Λ + → B ∆
Table 1: Definition of the Taylor expansion ( ) * and of its support T ( ).

Linear extension. Let R be a rig (a.k.a. semi-ring). Of particular interest are the rigs B : = ({0, 1} , max, min) of booleans, N : = (N, +, ×) of non-negative integers and Q : = (Q, +, ×) of rational numbers. We denote as R ∆ (resp. R ∆ ! ) the set of all formal (finite or infinite) linear combinations of resource terms (resp. bags) with coefficients in R. Notice that the last formula is coherent with the notation of the concatenation of bags as a product since it expresses a distributivity law. In particular, we denote

If a ∈ R ∆ (resp. a ∈ R ∆ ! ) and s ∈ ∆ (resp. s ∈ ∆ ! ), then a s ∈ R (resp. a s ∈ R) denotes the coefficient of s in a (resp. s in a). As is well-known, R ∆ is endowed with a structure of R- module,
a n : = [a, . . . , a] n and if Q ⊆ R, a ! : = n∈N 1 n! a n .
In the case R = B, notice that B ∆ is the power-set lattice P (∆), so that we can use the set-theoretical notation: e.g. writing s ∈ a instead of a s = 0, or a ∪ b for a + b. Also, in that case the preceding formulas lead to: for

a, b ⊆ ∆, t ∈ ∆, a ⊆ ∆ ! : λx.a : = {λx.s; s ∈ a}, a ! : = {[s 1 , • • • , s n ] ; s 1 , • • • , s n ∈ a},
t a : = { t s; s ∈ a} and a a : = { s a; s ∈ a}.

Taylor expansion. Ehrhard and Regnier have used in [START_REF] Ehrhard | Uniformity and the Taylor Expansion of Ordinary Lambda-Terms[END_REF] the rig of rational numbers to express the λ-terms as formal combinations in Q ∆ . We refer to this translation ( ) * : Λ + → Q ∆ as the Taylor expansion and we recall it in Table 1a by structural induction. The supports of these expansions can be seen as a map T ( ) : Λ + → B ∆ and directly defined by induction as in Table 1b.

Example 2. From the above definitions we have:

∆ * = n 1 n! λx. x x n , ∆ 3 * = n,m 1 n!m! λx. x x n x m .
Let us denote as δ n (resp. δ n,m ) the term λx. x x n (resp. λx. x x n x m ). We can then write:

Ω * = k 1 k! n0,...,n k 1 n 0 ! • • • n k ! δ n0 [δ n1 , . . . , δ n k ] , (4)
Ω 3 * = k 1 k! n0,...,n k m0,...,m k 1 n 0 !m 0 ! • • • n k !m k ! δ n0,m0 [δ n1,m1 , . . . , δ n k ,m k ] . (5)
It is clear that the resource terms appearing with non-zero coefficients in M * describe the structure of M taking an explicit number of times the argument of each application, and this recursively. The rôle of the rational coefficients will be clearer once defined the reduction rules over ∆ (see Example 5).

Operational semantics. Let us write deg x (t) for the number of free occurrences of a variable x in a resource term t. We define the differential substitution of a variable x with a bag [s 1 , . . . , s n ] in a resource term t, denoted ∂ x t • [s 1 , . . . , s n ]: it is a finite formal sum of resource terms, which is zero whenever deg x (t) = n; otherwise it is the sum of all possible terms obtained by linearly replacing each free occurrence of x with exactly one s i , for i = 1, . . . , n. Formally,

∂ x t • [s 1 , . . . , s n ] : =    f ∈Sn t s f (1) /x 1 , . . . , s f (n) /x n if deg x (t) = n, 0 otherwise, (6)
where S n is the group of permutations over n = {1, . . . , n} and x 1 , . . . , x n is any enumeration of the free occurrences of x in t, so that t s f (i) /x i denotes the term obtained from t by replacing the i-th free occurrence of x with s f (i) .

Then, we give a linear extension of the differential substitution: if a ∈ R ∆ and a ∈ R ∆ ! , we set:

∂ x a • a = t∈∆,s∈∆ ! a t a s ∂ x t • s.
The resource reduction → r is then the smallest relation satisfying:

λx.t [s 1 , . . . , s n ] → r ∂ x t • [s 1 , . . . , s n ]
and moreover linear and compatible with the resource calculus constructors. Spelling out these two last conditions: for any t, u In fact, Corollary 39 ensures that if a is the Taylor expansion of a strongly normalizing non-deterministic λ-term then Equation ( 7) is well-defined. * . The commutation between computing normal forms and Taylor expansions has been proven in general for deterministic λ-terms [START_REF] Ehrhard | Böhm trees, Krivine's Machine and the Taylor Expansion of Lambda-Terms[END_REF] 6 and witnesses the solidity of the definitions. The general case for Λ + is still an open issue.

∈ ∆, s ∈ ∆ ! , a, b ∈ R ∆ , α ∈ R \ {0},
Example 6. Recall the notation of Equation ( 4) from Example 2 expressing the sum Ω * . All terms with n 0 = k + 1 reduce to zero in one step. For n 0 = k + 1, we have that a single term rewrites to f ∈S k δ n f (1) δ n f (2) , . . . , δ n f (k) , which is a sum of terms still in T (Ω), but with smaller size w.r.t. the redex. Therefore, every term of Ω * eventually reduces to zero, after a reduction sequence whose length depends on the initial size of the term, and whose elements are sums with supports in T (Ω). This is in some sense the way Taylor expansion models the unbounded resource consumption of the loop Ω → β Ω in λ-calculus.

We postpone the discussion of the reduction of Ω 3 * until Remark 37.

Finiteness structures induced by antireduction

Let us get back to Equation ( 7), and consider it pointwise: for all s ∈ ∆ in normal form, we want to set NF(a) s = t∈∆ a t • NF(t) s . Notice that this series can be obtained as the inner product between a and the vector ↑s with (↑s ) t = NF(t) s : one can think of s as a test, that a passes whenever the sum converges.

There is one very simple condition that one can impose on a formal series to ensure its convergence: just assume there are finitely many non-zero terms. This seemingly dull remark is in fact the starting point of the definition of finiteness spaces, introduced by Ehrhard [START_REF] Ehrhard | Finiteness spaces[END_REF] and discussed in the Introduction. The basic construction is that of a finiteness structure: Definition 7 ( [START_REF] Ehrhard | Finiteness spaces[END_REF]). Let A be a fixed set. A structure on A is any set of subsets A ⊆ P (A). For all subsets a and a ⊆ A, we write a ⊥ a whenever a∩a is finite. For all structure A ⊆ P (A), we define its dual 7) involves only pointwise finite sums. So, one is led to focus on support sets only, leaving out coefficients entirely. Henceforth, unless specified otherwise, we will thus stick to the case of R = B, and use set-theoretical notations only. This approach of ensuring the normalization of Taylor expansion via a finiteness structure was first used by Ehrhard [START_REF] Ehrhard | A finiteness structure on resource terms[END_REF] for a non-deterministic variant of System F. Our paper strengthens Ehrhard's result in several directions. In order to state them, we introduce a construction of finiteness structures on ∆ induced by anticones for the reduction order defined as follows: Definition 8. For all s, t ∈ ∆, we write t ≥ s whenever there exists a reduction t → * r a with s ∈ a. It should be clear that this defines a partial order relation (in particular we have antisymmetry because → r terminates). Definition 9. If a ⊆ ∆, ↑a : = {t ∈ ∆; ∃s ∈ a, t ≥ s} is the cone of antireduction over a. 7 For any structure T ⊆ P (∆), we write (T) = {↑a ; a ∈ T}.

A ⊥ = {a ⊆ A; ∀a ∈ A, a ⊥ a }. A finiteness structure on A is any such A ⊥ . Notice that: A ⊆ A ⊥⊥ , also A ⊆ A entails A ⊥ ⊆ A ⊥ , hence A ⊥ = A ⊥⊥⊥ . Let C 0 = {|↑s | ; s ∈ ∆, in normal form} ⊆ P (∆), we obtain that |a| ∈ C 0 ⊥ iff Equation (
We can consider the elements of T as tests, and say a set a ⊆ ∆ passes a test a ∈ T iff a ⊥ ↑a . The structure of sets that pass all tests is exactly (T)

⊥ . Then Ehrhard's result can be rephrased as follows:

Theorem 10 ([4]). If M ∈ Λ + is typable in System F then T (M ) ∈ (S sgl ) ⊥ where S sgl : = {{s} ; s ∈ ∆}.
Notice that, in contrast with the definition of C 0 , S sgl is in fact not restricted to normal forms. Our paper extends this theorem in three directions: first, one can relax the condition that M is typed in System F and require only that M is strongly normalizable; second, the same result can be established for sets of "tests" larger (hence more demanding) than S sgl ; third, the implication can be reversed for a suitable set of tests T, i.e. M is strongly normalizable iff T (M ) ∈ (T)

⊥ (and we do need T to provide more tests than just singletons: see Remark 37). In order to state our results precisely, we need to introduce a few more notions.

A, B : =

X | A → B | A ∩ B
(a) Grammar of types, X varying over a denumerable set of propositional variables

for i ∈ {1, 2} A1 ∩ A2 Ai A A B B A → B A → B (A → B) ∩ (A → C) A → (B ∩ C) Γ M : A Γ N : A (+) Γ M + N : A Γ M : A A A ( ) Γ M : A (c) Derivation rules
Table 2: the intersection type assignment system D + for Λ + Definition 11. We say that a resource term s is linear whenever each bag appearing in s has cardinality 1. A set a of resource terms is said linear whenever all its elements are linear. We say a is bounded whenever there exists a number n ∈ N bounding the cardinality of all bags in all terms in a. We then write L : = {a ⊆ ∆; a linear} and B : = {a ⊆ ∆; a bounded} .

We also denote as (M ) the subset of the linear resource terms in T (M ). Notice that (M ) is always non-empty and can be directly defined by replacing the definition of T ((M ) N ) in Table 1b with:

((M ) N ) : = { s [t] ; s ∈ (M ) , t ∈ (N )}.
Observe that S sgl , L ⊆ B.

We can sum up our results Corollary 30 and Theorem 36 as follows:

Theorem 12. Let M ∈ Λ + :
-If M is strongly normalizing, then T (M ) ∈ (T) ⊥ as soon as T ⊆ B.

-If T (M ) ∈ (T) ⊥ with L ⊆ T, then M is strongly normalizing.

3 Strongly Normalizing Terms Are D + Typable

Intersection types are well known, as well as their relation with normalizability. We refer to [START_REF] Barendregt | A filter lambda model and the completeness of type assignment[END_REF] for the original system with subtyping characterizing the set of strongly normalizing λ-terms, and [START_REF] Van Bakel | Complete restrictions of the intersection type discipline[END_REF] and [START_REF] Krivine | Lambda-calculus, types and models[END_REF] for simpler systems. However, as far as we know, the literature about intersection types for non-deterministic λ-calculi is less well established and in fact we could find no previous characterization of strong normalization in a non-deterministic setting. Hence, we give in Table 2 a variant of Krivine's system D [START_REF] Krivine | Lambda-calculus, types and models[END_REF], characterizing the set of strongly normalizing terms in Λ + . In this section, we only prove that strongly normalizing terms are typable (Theorem 14): the reverse implication follows from the rest of the paper (see Figure 1). These techniques are standard.

Remark 13. Krivine's original System D does not have ( ) and (+), but it has the two usual elimination rules for intersection (here derivable). The rule (+) is necessary to account for non-determinism, however adding just (+) to System D is misbehaving. We can find terms M and N , and a context Γ such that (M ) N is typable in System D with (+) under the context Γ but M is not: take Γ = x : A → B ∩B , y : A → B ∩B , z : A, observe that (x + y) z = (x) z +(y) z, and thus Γ (x + y) z : B but x + y is not typable in Γ . This is the reason why we introduce subtyping.

Theorem 14. For all M ∈ Λ + , if M is strongly normalizable, then there exists a derivable judgement Γ M : A in system D + .

Proof (Sketch). For M a strongly normalizable term, let l (M ) be the maximum length of a reduction from M , and s (M ) the number of symbols occurring in M . By well-founded induction on the pair (l (M ) , s (M )) we prove that there exists n M ∈ N such that for all type B and all n ≥ n M , there is a context Γ and a sequence (A 1 , . . . , A n ) of types such that Γ M :

A 1 → • • • → A n → B.
The proof splits depending on the structure of M . In case M = M 1 + M 2 , we apply the induction hypothesis on both M 1 and M 2 and conclude by rule ( ) and a contravariance property: Γ M : A whenever Γ M : A and Γ Γ . In case of head-redexes, i.e. M = ((λx.N ) P ) M 1 • • • M q , we apply the induction hypothesis on M = (N [P/x]) M 1 • • • M q and on P . Then, we conclude via a subject expansion lemma stating that:

Γ (λx.N ) P M 1 • • • M n : A, whenever Γ (N [P/x]) M 1 • • • M n :
A and there exists B such that Γ P : B.

The other cases are similar to the first one.

D + Typable Terms Are Finitary

This section proves Corollary 30, giving sufficient conditions (to be dispersed, hereditary and expandable, see resp. Definition 23, 26 and 27) over a structure T in order to have all cones ↑a for a ∈ T dual to the Taylor expansion of any strongly normalizing non-deterministic λ-term.

It is easy to check that these conditions are satisfied by the structures B of bounded sets and L of sets of linear terms (Definition 11). Moreover, as an immediate corollary one gets also that any subset T ⊆ B is also such that T (M ) ∈ (T)

⊥ for any strongly normalizable term M ∈ Λ + , so getting the first Item of Theorem 12.

Thanks to previous Theorem 14 we can prove Corollary 30 by a realizability technique on the intersection type system D + . For a fixed structure S, we associate with any type A a realizer A S (Definition 18). In the case S is adapted (Definition 17), we can prove that A S contains the Taylor expansion of any term of type A and that it is contained in S (Theorem 21). These definitions and theorem are adapted from Krivine's proof for System D [START_REF] Krivine | Lambda-calculus, types and models[END_REF].

The crucial point is then to find structures S which are adapted : here is our contribution. The structures that we study have the shape (T)

⊥ , so that we are speaking of the interaction with cones of anti-reducts of tests in a structure T. Intuitively, T is a set of tests that can be passed by any term typable in System D + (hence by any strongly normalizing term). We prove (Lemma 29) that for a structure T, being dispersed, hereditary and expandable is sufficient to guarantee that the dual structure (T)

⊥ is adapted, then achieving Corollary 30.

Definition 15 (Functional). Given two structures S, S ⊆ P (∆), we define the structure S → S : = f ⊆ ∆; ∀a ∈ S, f a ! ∈ S .

Definition 16 (Saturation). Let S, S ⊆ P (∆). We say S is S-saturated if

∀e, f 0 , . . . , f n ∈ S, ∂ x e • f 0 ! f 1 ! . . . f n ! ∈ S implies λx.e f 0 ! f 1 ! . . . f n ! ∈ S .
Definition 17 (Adaptedness). For all S ⊆ P (∆) we set

S h : = {{x} ; x ∈ V}∪ x a 1 ! • • • a n ! ;
x ∈ V, n > 0 and ∀i, a i ∈ S and say S is adapted if: Now we look for conditions to ensure that a structure S is adapted. These conditions (Definition 23, 26 and 27) are quite technical but they are easy to check, in particular the structures B and L enjoy them (Remark 28).

1. S is S-saturated; 2. S h ⊂ (S → S h ) ⊂ (S h → S) ⊂ S; 3
Definition 22. The height h (s) of a resource term s is defined inductively: h (x) : = 1, h (λx.s) : = 1 + h (s) and h ( s 0 [s 1 , . . . , s n ]) : = 1 + max i (h (s i )).

Definition 23 (Dispersed). A set a ⊆ ∆ is dispersed whenever for all n ∈ N, and all finite set V of variables, the set {s ∈ a; h (s) ≤ n and fv (s) ⊆ V } is finite. A structure S is dispersed whenever ∀a ∈ S, a is dispersed.

Definition 24. Let s ∈ ∆ and x ∈ fv (s). We define immediate subterm projections π x s ∈ P (∆), π 0 s ∈ P (∆), π 1 s ∈ P ∆ ! and π 1 s ∈ P (∆) as follows:

-if s = λx.t then π x s = {t}; otherwise π x s = ∅; -if s = t u then π 0 s = {t}, π 1 s = {u}, π 1 s = |u|; otherwise π 0 s = π 1 s = π 1 s = ∅.
Observe that up to α-conversion and the hypothesis x ∈ fv (s), the abstraction case is exhaustive. These functions obviously extend to sets of terms, up to some care about free variables. If V ⊆ V is a set of variables, we write ∆ V for the set of resource λ-terms with free variables in V .

Definition 25. For all V ⊆ V and a ⊆ ∆ V , let

π 0 a : = s∈a π 0 s ⊆ ∆ V , π 1 a : = s∈a π 1 s ⊆ ∆ V ! , π 1 a : = s∈a π 1 s ⊆ ∆ V ,
and if moreover x ∈ V , then let π x a : = s∈a π x s ⊆ ∆ V ∪{x} .

Definition 26 (Hereditary). A structure S ⊆ P (∆) is said to be hereditary if, S is downwards closed, and for all a ∈ S, π 0 a ∈ S, π 1 a ∈ S and for all x ∈ V \ fv (a), π x a ∈ S.

Definition 27 (Expandable). A structure S ⊆ P (∆) is said to be expandable if, for all x ∈ V and all a ∈ S, we have { s [x] ; s ∈ a} ∈ S.

Remark 28. The structures S sgl (Theorem 10) and L, B (Definition 11) are dispersed and expandable. The last two are also hereditary, while S sgl is not.

Lemma 29. For any structure T which is dispersed, hereditary and expandable, we have that (T) ⊥ is adapted.

Proof (Sketch). One has to prove the three conditions of Definition 17. Heredity and dispersion are used to obtain saturation (Condition 1). The inclusions of Condition 2 need all hypotheses and an auxiliary lemma proving that (T)

⊥ h ⊆ (T)
⊥ , for which dispersion is crucial. Finally, the closure under finite unions (Condition 3) is satisfied by all finiteness structures. Corollary 30. Let T ⊆ P (∆) be dispersed, hereditary and expandable. For every strongly normalizable term M , we have T (M ) ∈ (T)

⊥ . Hence, this holds for T ∈ {L, B} and for any of their subsets, such as S sgl ⊂ B.

Proof. The general statement follows from Theorems 14, 21 and Lemma 29. Remark 28 implies T (M ) ∈ (T)

⊥ for T ∈ {B, L}. The rest of the statement follows because, for any structures S, S , S ⊆ S implies S ⊥ ⊆ S ⊥ .

Finitary Terms Are Strongly Normalizing

In this section we prove Theorem 36, giving a sufficient condition for a structure T to be able to test strong normalization. The condition is that T includes at least L, i.e. the set of all sets of linear terms 8 . The proof is by contraposition, suppose that M is divergent, then T (M ) is not dual to some cone ↑a , with a ∈ L. The proof enlightens two kinds of divergence in λ-calculus: the one generated by looping terms: Ω → β Ω → β . . . and the other generated by infinite reduction sequences (M i ) i∈N with an infinite number of different terms:

Ω 3 → β (Ω 3 ) ∆ 3 → β ((Ω 3 ) ∆ 3 ) ∆ 3 → β . .

. (see Example 1).

In the first case, the cone  (Ω) of the linear expansion (Definition 11) of the looping term Ω suffices to show up the divergence, since T (Ω) ∩  (Ω) is infinite. Indeed the Taylor expansion of a looping term, say T (Ω), is a kind of "contractible space", where any resource term reduces to a smaller term within the same Taylor expansion or vanishes (see Example 6). In particular, there are unboundedly large resource terms reducing to the linear expansion (Ω).

In the case of an infinite reduction sequence of different terms, one should take, basically, the cone of all linear expansions of the terms occurring in the sequence: the linear expansion of a single term (or of a finite set of terms) might not suffice to test this kind of divergence. For example, T (Ω 3 )∩  (Ω 3 ) is finite, while T (Ω 3 ) ∩  { (Ω 3 ), ((Ω 3 ) ∆ 3 ), . . . } is infinite, so T (Ω 3 ) / ∈ (L) ⊥ . In the presence of the non-deterministic sum +, we have a third kind of divergence, which is given by infinite reduction sequences of terms (M i ) i∈N which are pairwise different but whose Taylor expansion support repeats infinitely many times: consider, e.g., the reducts of (Θ) (λx.x + y). We prove that this kind of divergence is much more similar to a loop rather than to a sequence of different λ-terms. In particular, there is a single linear resource term (depending on the reduction sequence) whose cone is able to show up the divergence. Indeed, most of the effort in the proof of Theorem 36 is devoted to deal with this kind of "looping Taylor expansion". Namely, Definition 31 gives a notion of non-deterministic reduction allowing Lemma 35, which is the key statement used in the proof of Theorem 36 for dealing with both the divergence of looping terms (like Ω) and that of looping Taylor expansions (like (Θ) (λx.x + y)). 8 This condition can be slightly weakened replacing L with: {a ⊆ ∆; a linear and fv (a) finite}. However, we prefer to stick to the more intuitive definition of L.

  where addition and scalar multiplication are defined component-wise, i.e. for a, b ∈ R ∆ and α ∈ R: (a + b) s : = a s + b s , and (αa) s : = αa s . We will write |a| ⊆ ∆ for the support of a: |a| = {s ∈ ∆; a s = 0}. Moreover, each resource calculus constructor extends to R ∆ componentwise, i.e. for any a, a 1 , . . . , a n ∈ R ∆ and a ∈ R ∆ ! , we set: λx.a : = s∈∆ a s λx.s, a a : = s∈∆, s∈∆ ! a s a s s s, [a 1 , . . . , a n ] : = s1,...,sn∈∆ (a 1 ) s1 • • • (a n ) sn [s 1 , . . . , s n ] .

Example 5 . 1 n→ r n 1 n

 511 Recall the expansions of Example 2 and consider ((∆) λx.x) !k! λx. x [x n ] (λx.x) k . The resource reduction applied to a term of this sum gives zero except for k = n + 1; in this latter case we get (n + 1)! λx.x [(λx.x) n ]. Hence we have: ((∆) λx.x) * ! λx.x [(λx.x) n ], because the coefficient (n + 1)! generated by the reduction step is erased by the fraction 1 k! in the definition of Taylor expansion. Then, the term λx.x [(λx.x) n ] reduces to zero but for n = 1, in the latter case giving λx.x. So we have: NF(((∆) λx.x) * ) = λx.x = (NF((∆) λx.x))

  . S is closed under finite unions: ∀b, b ∈ S, b ∪ b ∈ S.Definition 18 (Realizers). Let S ⊆ P (∆). To each type A of System D + , we associate a structure A S defined inductively (X being a propositional variable):X S : = S, A → B S : = A S → B S , A ∩ B S : = A S ∩ B S .Lemma 19. Let S be an adapted structure, then for every type A, A S is S-saturated, closed under finite unions and S h ⊆ A S ⊆ S.Lemma 20 (Adequacy).If S ⊆ P (∆) is adapted, x 1 : A 1 , . . . , x n : A n M : B and for all 1 ≤ i ≤ n, a i ∈ A i S , then ∂ x1,...,xn T (M ) • a 1 ! , . . . , a n ! ∈ B S .Proof (Sketch). By structural induction on the derivation of x 1 : A 1 , . . . , x n : A n M : B. The cases where the last rule is (→ i ) or (+) use respectively the facts that the realizers are saturated and closed by finite unions. The case where the last rule is ( ) is an immediate consequence of the induction hypothesis and of a lemma stating that A B implies A S ⊆ B S . Theorem 21. If S ⊆ P (∆) is adapted and M is typable in System D + , then T (M ) ∈ S. Proof. Let Γ M : B. For any x : A in Γ , {x} ∈ S h ⊂ A S by Lemma 19 and Definition 17. Hence, T (M ) = ∂ x1,...,xn T (M ) • {x 1 } ! , . . . , {x n } ! ∈ B S by Lemma 20. Again by Lemma 19, B S ⊆ S, so T (M ) ∈ S.

  whenever t → r a, we have: (compatibility) λx.t → r λx.a, t s → r a s, u t • s → r u a • s, and (linearity) αt + b → r αa + b. Resource reduction → r is confluent over the whole R ∆ and it is normalizing on the sums in R ∆ having a finite support.Proposition 3 shows that any single resource term t ∈ ∆ has a unique normal form that we can denote as NF(t). What about possibly infinite linear combinations in R ∆ ? We would like to extend the normal form operator component-Example 4. The sum in Equation (7) can be undefined for general a ∈ R ∆ . Take a = λx.x + λx.x [λx.x] + λx.x [ λx.x [λx.x]] + . . . : any single term of this sum reduces to λx.x, hence NF(a) λx.x is infinite.Another example is given by the Taylor expansion of the term in Equation (3): one can check that the sum defining NF ((Θ) λx.(x + y)) * y following Equation (7) is infinite because, for all n ∈ N, there is a resource term of the form t

	Proposition 3 ([7]). wise, as follows:	NF(a) : =	t∈∆	a t • NF(t)	(7)

n [(λx.x) n , λx.y] ∈ T ((Θ) λx.(x + y)), reducing to y. A closer inspection of the resulting coefficients (that we do not develop here) moreover shows that this infinite sum has unbounded partial sums in Q, hence it diverges in general.

We use Krivine's notation with the standard conventions, see[START_REF] Krivine | Lambda-calculus, types and models[END_REF] for reference.

The statement proven in[START_REF] Ehrhard | Böhm trees, Krivine's Machine and the Taylor Expansion of Lambda-Terms[END_REF] is actually more general, because it considers (possibly infinite) Böhm trees instead of the normal forms.

Observe that  {s} = ↑s (up to the identification of B ∆ with P (∆)).

(b) Rules generating the subtyping relation(var) Γ, x : A x : A Γ, x : A M : B (→i) Γ λx.M : A → B Γ M : A → B Γ N : A (→e) Γ (M ) N : B Γ M : A Γ M : B (∩i) Γ M : A ∩ B

We introduce a reduction rule on Λ + which corresponds to one step of β-reduction and a potential loss of some addenda in a term. For that, we need an order on Λ + expressing this loss. For instance, (Θ) (λx.x + y) + y (Θ) λx.x, thus (Θ) (λx.x + y) * (Θ) λx.x, and similarly, (Θ) (λx.x + y) * y.

Definition 31 (Partial reduction). We write M N if there exists P such that M → β P and P N , where the partial order over Λ + is defined as the least order such that M M + N ; N M + N and if M N then: M + P N + P , λx.M λx.N , (M ) P (N ) P , and (P )

Write s > t whenever s ≥ t (Definition 8) and s = t: this is a strict partial order relation.

Lemma 32. If M N and t ∈ T (N ), then there exists s ∈ T (M ) such that s ≥ t. If moreover, M N is at top level, then s > t.

i∈N is bounded, then there exists a linear term t such that T (M 0 ) ∩ ↑t is infinite. Proof (Sketch). First, it is sufficient to address the case of a sequence (S i ) i∈N of simple terms (i.e. without + as the top-level constructor) such that S i S i+1 for all i ∈ N and (h (S i )) i∈N is bounded. Besides, by Lemma 33, it is sufficient to have T (S i0 ) ∩ ↑t infinite for some i 0 ∈ N.

Then, by induction on h = max {h (S i ) ; i ∈ N}, we show that there exists i 0 ∈ N and a sequence (s j ) j∈N ∈ T (S i0 ) N such that s 0 is linear and, for all j ∈ N, s j+1 > s j . Since > is a strict order relation, this implies that the set {s j ; j ∈ N} ⊆ T (S i0 ) ∩ ↑s 0 is infinite.

First assume that there are infinitely many top level reductions. Observe that, since h (S i ) ≤ h and fv (S i ) ⊆ fv (S 0 ) for all i, the set {T (S i ) ; i ∈ N} is finite. Hence there exists an index i 0 ∈ N such that {i ∈ N; T (S i ) = T (S i0 )} is infinite. As there are infinitely many top level reductions, there are i 1 and i 2 such that i 0 < i 1 < i 2 , the reduction i 1 is at top level and T (S i2 ) = T (S i0 ). We inductively define the required sequence by choosing arbitrary s 0 ∈ (S i0 ) ⊆ T (S i0 ), and by iterating Lemma 32: for s j ∈ T (S i0 ) = T (S i2 ), we obtain s j+1 ∈ T (S i0 ) with s j+1 > s j since the reduction i 1 is at top level. Now assume that there are only finitely many top level reductions. Let i 1 be such that no reduction S i S i+1 with i ≥ i 1 is at top level. Either for all i ≥ i 1 , S i = λx.M i with M i M i+1 , and we conclude by applying the induction hypothesis to the sequence (M i+i1 ) i∈N ; or for all i ≥ i 1 , S i = (M i ) N i so that (M i ) i≥i1 and (N i ) i≥i1 are sequences of terms, at least one of them involving infinitely many partial reductions. In this case, assume for instance that we can extract from (M i ) i≥i1 an infinite subsequence (M φ(i) ) i∈N of partial reductions. It provides i 0 and a sequence (s j ) ∈ T (M φ(i 0 ) ) N with s 0 linear and, s j+1 > s j . Fix t ∈ (N φ(i 0 ) ) arbitrarily. So we set i 0 = φ(i 0 ) and s j = s j [t] for all j ∈ N.

Theorem 36. Let T be a structure such that L ⊆ T. If T (M ) ∈ (T)

⊥ then M is strongly normalizable. In particular, this holds for T ∈ {L, B}.

Proof. Assume that (M i ) i∈N is such that M = M 0 and for all i, M i → β M i+1 . We prove that T (M ) ∈ (T)

⊥ by exhibiting a ∈ T such that T (M ) ⊥ ↑a . If (h (M i )) i∈N is bounded, then fix a = {t} with t given by Lemma 35. Otherwise, ∀i ∈ N, fix t i ∈ (M i ) such that h (t i ) = h (M i ). Lemma 32 implies that there is s i ∈ T (M ) such that s i ≥ t i . Denote by s (s) the number of symbols occurring in s. Since there is no duplication in reduction → r it should be clear that if s ≥ t then s (s) ≥ s (t). Besides, s (s) ≥ h (s). Therefore, since {h

Notice that the structure S sgl of singletons used in [START_REF] Ehrhard | A finiteness structure on resource terms[END_REF] does not enjoy the hypothesis of Theorem 36 (L ⊂ S sgl ). In fact:

Remark 37. We prove that T (Ω 3 ) ∈ (S sgl ) ⊥ , although Ω 3 is not normalizing. Recall from Example 2, that the support of the Taylor expansion of Ω 3 is made of terms of the form δ n0,m0 [δ n1,m1 , . . . , δ n k ,m k ] (for k, n i , m i ∈ N). Write ∆ h = { δ -,-[. . . δ -,-. . . ] • • • [. . . δ -,-. . . ] with h bags}: in particular T (Ω 3 ) = ∆ 1 . One can easily check that if s ∈ ∆ h and s ≥ s , then s ∈ ∆ h with h ≤ h . A careful inspection of such reductions shows that they are moreover reversible: for all s ∈ ∆ h and all h ≤ h there is exactly one s ∈ ∆ h such that s ≥ s . It follows that ∆ 1 ∩ ↑ s is either empty or a singleton. Therefore T (Ω 3 ) ∈ (S sgl ) ⊥ .

Conclusion

We achieved all implications of Figure 1, but the rightmost one, concerning the finiteness of the coefficients in the normal form of the Taylor expansion of a strongly normalizing λ-term (recall Equation (2) in the Introduction). Thanks to the definition of cones (Definition 9) we immediately have the following lemma, which is the last step to Corollary 39.

Lemma 38. Let T be a structure. If T (M ) ∈ (T)

⊥ , then ∀t ∈ T, NF(T (M )) t is finite.

Applying Corollary 30 and Lemma 38 to a structure like B or S sgl , we get:

Corollary 39. Given a non-deterministic λ-term M , if M is strongly normalizable, then NF(T (M )) t is finite for all t ∈ ∆.


Benjamin Lussier

Alexandre Lampe

Raja Chatila

Jérémie Guiochet

Félix Ingrand

Marc-Olivier Killijian

David Powell

Fault Tolerance in Autonomous Systems: How and How Much?

Autonomous systems are starting to appear in space exploration, elderly care and domestic service; they are particularly attractive for such applications because their advanced decisional mechanisms allow them to execute complex missions in uncertain environments. However, systems embedding such mechanisms simultaneously raise new concerns regarding their dependability. We aim in this paper to present these concerns and suggest possible ways to resolve them. We address dependability as a whole, but focus specifically on fault tolerance. We present some particularities of autonomous systems and discuss the dependability mechanisms that are currently employed. We then concentrate on the dependability concerns raised by decisional mechanisms and consider the introduction and assessment of appropriate fault tolerance mechanisms.

INTRODUCTION

Real world experiments in autonomous systems appear in such domains as space exploration, elderly care, museum tour guidance and personal service. These are critical fields of application, as a system failure may result in catastrophic consequences regarding human lives or in economic terms. Moreover, autonomous systems might be particularly dangerous as their actions are not directly controlled by a human operator. Thus arises a need for dependability, that is a justified trust that the system will appropriately perform its mission and not cause catastrophes. One of dependability means, fault tolerance, considers in particular that faults are inevitable in any complex system, and aims to make their consequences negligible. This paper studies autonomous system particularities regarding dependability, and discusses how to improve fault tolerance in such systems.

We first describe particularities of autonomous systems in comparison with "classic" computing systems, that is the notion of robustness (somewhat similar to fault tolerance) and the use of decisional mechanisms. The second section presents a detailed state of the art on dependability and robustness mechanisms in autonomous systems. We then give conclusions and recommendations for the development of autonomous systems, and present future directions: possible fault tolerant techniques for the decisional mechanisms of autonomous systems, and an experimental framework based on simulation and fault injection for assessing their efficiency.

I. PARTICULARITIES OF AUTONOMOUS SYSTEMS

This section presents the main particularities of autonomous systems in comparison with classic computing system. We first enunciate the distinction that we make between robustness and fault tolerance, and then introduce notions specific to decisional mechanisms.

A. Robustness and fault tolerance

The concept of robustness appeared in the robotic field as an answer to the large variability of execution contexts resulting from robot operation in an open environment. If we consider that faults are just another cause of uncertainty then robustness might be considered as a superset of fault tolerance. However, a useful distinction between robustness and fault tolerance can be made by restricting the use of the former to the tolerance of adverse situations not due to faults. We therefore adopt the following definitions in the context of autonomous systems (Figure 1) [START_REF] Lussier | On Fault Tolerance and Robustness in Autonomous Systems[END_REF]:

• Robustness is the delivery of a correct service in adverse situations arising due to an uncertain system environment (such as an unexpected obstacle or a change in lighting condition affecting optical sensors). • Fault tolerance is the delivery of a correct service despite faults affecting system resources (such as a flat tire, a sensor malfunction or a software fault).

EXPLICITLY-SPECIFIED ADVERSE SITUATIONS UNEXPECTED ADVERSE ADVERSE SITUATIONS

SITUATIONS SYSTEM RESOURCES UNCERTAIN ENVIRONMENT (ROBUSTNESS) (FAULT TOLERANCE)

Figure 1: Robustness vs. fault tolerance A remark may be added about the service provided by the system. Here, we consider that a correct service is a behavior in accordance with the intended system function, from a user point of view; it is defined before execution and is embodied in the system specifications, which determines the goals to be achieved in well-defined situations. A dependable system should thus provide a correct service regarding nominal situations and explicitly-specified adverse situations.

However, an autonomous system is often required to function in an open environment, where operating conditions can not all be determined in advance. When faced with unexpected adverse situations a correct service cannot be guaranteed. However, the user may judge after execution that, given the unexpected situation that the system had to face, the service, while not correct with respect to the specification, was nevertheless acceptable. An acceptable service is generally less successful than a correct service as the system had to deal with unexpected adverse situations (it may achieve less goals, or only part of the goals).

B. Decisional Mechanisms

Decisional mechanisms are central to autonomous systems, as they embody the ability to select and choose actions to achieve specified objectives. This section presents decisional mechanisms and proposes a classification of possible faults affecting those mechanisms.

1) Characterization of decisional mechanisms: A decisional mechanism is composed of knowledge specific to the system's domain of application (such as heuristics or a model of the environment) and an inference mechanism used to solve problems by manipulating this knowledge. Ideally, the inference mechanism is independent from the application and can be re-used in a different one with new appropriate knowledge. In practice however, knowledge and inference mechanism are often hard to dissociate; for example heuristics in planners or weights in neural networks are intrinsic parts of the inference mechanism.

Applied to an ideal faultless knowledge base, an inference mechanism can be characterized by three main properties: soundness, completeness and tractability [START_REF] Nilsson | Artificial Intelligence: A New Synthesis[END_REF]:

• Soundness indicates that any conclusion raised by the inference mechanism is correct. • Completeness indicates that the inference mechanism will eventually produce any true conclusion. • Tractability characterizes the complexity of the inference mechanism: it indicates whether the inference mechanism can solve a problem in polynomial time and space, that is whether the time and memory space needed to find a solution can be defined as a polynomial function of the problem size.

Inference mechanisms currently used in autonomous systems are often sound and complete, but intractable. In practice, completeness is often relinquished through the use of heuristics, in order to improve tractability, and consequently the system performance.

2) Fault classification in decisional mechanisms: Decisional mechanisms introduce new faults in comparison to classic computing systems. From the risks of error presented in [START_REF] Boden | Benefits and Risks of Knowledge-Based Systems[END_REF] and [START_REF] Fox | Safe and Sound, Artificial Intelligence in Hazardous Applications[END_REF] we have identified internal faults in a decisional mechanism, and interaction faults between a decisional mechanism and another component or system (such as a human operator or another decisional mechanism). a) Internal faults: Internal faults in a decisional mechanism may affect either the knowledge or the inference mechanism (Figure 2) [START_REF] Lussier | State of the Art on Dependability of Autonomous Systems[END_REF]. Faults in the inference mechanism may be introduced during development of the system, either as a design fault (for example if the decisional mechanism is not adapted to the system function, or if its principle is flawed) or as a programming fault (such as a typing or algorithm error).

Faults in the system knowledge may be introduced either during development (design or programming) or in operation. Design faults may be either an explicitly-specified adverse situation that has not been covered by the developers (such as a missing procedure or an action needed to treat the adverse situation, or missing example sets used in learning for neural networks), or an imperfection in the choice criterion that possibly causes wrong conclusions to be drawn by the inference mechanism (such as faults in heuristics, or facts used for decision that are wrong in particular situations). Knowledge programming faults include both missing and faulty information in the knowledge of the decisional mechanism. Operational faults are incorrect dynamic information in the knowledge of the decisional mechanism, such as the current state of the system or information learned from the environment; these faults may be caused for example by sensor failures or imperfections, or undetected memory corruption.

b) Interaction faults: The main faults of decisional mechanisms due to interaction with other components or systems are mismatches in the exchanged information. Such faults are not specific to decisional mechanisms and can be classified in several categories [START_REF] Jones | Revised Version of DSoS Conceptual Model (DC1)[END_REF].

Semantic mismatches are development faults that arise when different languages are used by the communicating components, and lead to information loss or modification. They are of particular concern in autonomous systems, as in practice semantic mismatches are common between different components. The three-layer type of architecture for example is built from components considering different levels of abstraction, each generally using a distinct model of the system and the environment. The executive component often lacks a global view of the system to better decompose plans, whereas the upper decisional mechanism does not possess all the relevant information for dealing with error reports.

Other types of mismatch (including physical, syntactical, and temporal mismatches) are similar to other computing systems, and can also be causes of information loss or modification.

At a different level, there are also risks of interactions faults between a decisional mechanism and a human operator:

• Misguided optimism in the system capabilities: the user is overconfident regarding the decisions taken by the decisional mechanism; for example, the results given may be very precise but wrong. • Incredulity in the system capabilities: the user has no confidence regarding the decisions taken by the decisional mechanism; for example, since he does not understand the reasoning process leading to a given decision.

II. STATE OF THE ART

This section presents a state of the art concerning dependability and robustness mechanisms in autonomous systems. We cover first fault prevention and fault removal (both encompassed in the notion of fault avoidance), then fault forecasting, fault tolerance and, finally, robustness.

A. Fault avoidance

Fault avoidance aims to produce a system containing as few faults as possible. It encompasses fault prevention, that is the means to prevent the introduction or occurrence of faults, and fault removal, that is the means to reduce the number and severity of faults.

1) Fault prevention: Fault prevention in autonomous systems is mainly implemented through the modularity of software components and the use of appropriate development tools.

Motivations for the modularity of software components are threefold: to decompose a complex system into simpler independent components, to capitalize generic structures or algorithm libraries, and to ease communication and scheduling between the components. Modularity thus prevent faults first by simplifying the development of each component (although it raises the problem of the component integration), and second by allowing components to be considered somewhat independently during development and testing. Modularity appears in generic architectures such as LAAS [START_REF] Alami | An Architecture for Autonomy[END_REF], RAX [START_REF] Muscettola | Remote Agent: To Boldly Go Where No AI System Has Gone Before[END_REF], CLARAty [START_REF] Volpe | CLARAty: Coupled Layer Architecture for Robotic Autonomy[END_REF] or IDEA [START_REF] Muscettola | IDEA: Planning at the Core of Autonomous Reactive Agents[END_REF], but also in several components of these architectures.

Development tools generally include libraries of generic components, which can be instantiated to adapt to a particular piece of hardware or algorithm. They automatically generate part of the component code, accelerating the development process and reducing the risks of programming faults. Development tools are often used to develop functional layers for autonomous systems, such as the Genom modules of the LAAS architecture, or the ControlShell [START_REF] Schneider | ControlShell: A Software Architecture for Complex Electromechanical Systems[END_REF], ORCCAD [START_REF] Borrelly | The ORCCAD Architecture[END_REF] or SIGNAL [START_REF] Marchand | Specifying and Verifying Active Vision-Based Robotic Systems with the SIGNAL Environment[END_REF] environments.

2) Fault Removal: Two fault removal mechanisms are particularly used in autonomous systems: tests and formal checking.

Simulation and operating tests are essential to the development of critical computing systems. In autonomous systems, however, their role is often limited to debugging rather than proving a thorough validation. Especially in the case of research platforms, developers check correct execution of the system for just a few situations. Intensive testing was however been carried out on the RAX architecture for the DS1 project [START_REF] Bernard | Remote Agent Experiment DS1 Technology Validation Report[END_REF]: six test beds were implemented throughout the development process, incorporating 600 tests. The authors of [START_REF] Bernard | Remote Agent Experiment DS1 Technology Validation Report[END_REF] underline the relevance of intensive testing, but acknowledge particular difficulties regarding autonomous systems, notably the problem of defining suitable test oracles.

Formal checking can be used to check properties of software component executions, such as safety or liveliness. However, it generally depends upon rigorous conditions, such as synchronism, and must be considered early in the development process. The ORCCAD and SIGNAL environments implement formal checking procedures.

B. Fault forecasting

Fault forecasting aims to estimate the present number, the future incidence, and the likely consequences of faults [START_REF] Avizienis | Basic Concepts and Taxonomy of Dependable and Secure Computing[END_REF]. There are apparently few studies in fault forecasting for autonomous systems in the literature.

[7] presents studies on the failure of indoor and outdoor robots (some of which are not autonomous). Thirteen robots were observed for nearly two years, displaying an MTBF (Mean Time Between Failure) of about 8 hours, and a reliability of less than 50%. Outdoor robots were seen to fail more often than indoor ones (maybe because of the more demanding outdoor environment), and while hardware faults were the most common cause of failures (42%), the control systems (including the operating systems) were also significant sources of failures (29%).

[33] presents the implementation of the autonomous museum tour guide RoboX9 and a study of its failures during five months of operation. The MTBF reached and stayed at around 4.6 hours after four weeks of operation; 96% of failures where caused by the software components (80% due to the non-critical human interaction process, and 16% due to the critical navigation and localization process).

C. Fault tolerance

Fault tolerance is rarely explicitly mentioned in literature on autonomous systems. Although some techniques (such as temporal control by a watchdog, or positioning the system in a safe state after detection of an error) are quite common, we believe that their use is far from systematic, partly because most autonomous systems are still research platforms.

1) Error detection: Error detection in autonomous systems is mainly implemented by timing checks, reasonableness checks, safety-bag checks, and model-based diagnosis monitoring.

Timing checks are implemented by watchdogs in the RoboX9 autonomous system [START_REF] Tomatis | Designing a Secure and Robust Mobile Interacting Robot for the Long Term[END_REF]. They supervise the liveness of critical functions such as speed monitoring, obstacle avoidance, bumpers and laser sensors. By their very principle, they detect only timing errors, not value errors.

Reasonableness checks verify, for example, that a state variable of the system lies within a specified interval of possible values. RoboX9 uses a reasonableness check to monitor the robot speed. [START_REF] Klein | The Safety-Bag Expert System in the Electronic Railway Interlocking System Elektra[END_REF] consist in intercepting and blocking the system commands if they do not respect a set of safety properties specified during development. The R2C component of the LAAS architecture [START_REF] Py | Real-Time Execution Control for Autonomous Systems[END_REF] acts as such a safety-bag.

Safety-bag checks

Monitoring for diagnosis is mostly used to detect hardware faults (such as a flat tire, or an underspeed motor) rather than software faults. Diagnosis monitoring is implemented by checking system behavior against a mathematical model: for example, the MIR component of the RAX architecture detects the presence of faults by comparing its sensor values with theoretical values from the model.

2) System recovery: System recovery in autonomous systems is mainly implemented by error containment, positioning in a safe state, and hardware and software reconfiguration.

Error containment (to limit error propagation) is implemented in RoboX9 through the use of dedicated processors. One processor executes critical tasks (such as localization and navigation) whereas another one executes less fundamental and less thoroughly tested interaction tasks (such as the user interface and the face-tracking function).

Positioning in a safe state may be executed after a critical component failure or while executing a time-consumng recovery action, such as re-planning. For example, the RoboX9 system positions itself in a safe state when a critical subsystem fails, and the Care-O-Bot system [START_REF] Graf | Mobile Robot Assistants -Issues for Dependable Operation in Direct Cooperation With Humans[END_REF] stops when a platform fault causes it to collide with an obstacle or person. Positioning in a safe state can also be executed after activation of a safetybag, by blocking or halting activities which invalidate the safety properties.

Hardware reconfiguration is performed in the RAX architecture through functional diversification of the hardware components: when a hardware failure is detected, the MIR component seeks a new system configuration able to fulfill the functions of the faulty component.

Software reconfiguration can be executed either by switching between different execution modes or by corrective maintenance (which can be seen as an ultimate form of faulttolerance) through the use of a patch. Switching between different execution modes may be realized through exception handling or through switching to an alternative decomposition of a task into elementary actions (see "modalities" below in section II-D.2.b). Patches have been implemented to recover the Martian rovers Pathfinder and Sojourner as they failed respectively because of priority and RAM management failures.

D. Robustness

Robustness in autonomous systems may be implemented in two ways:

• Systematic treatment applied in all situations, through observation of the current situation and selection of actions to be taken. • Specific treatment applied only to adverse situations, through explicit detection of the adverse situation and triggering of an appropriate contingency procedure. 1) Observation and action selection: Systematic treatment by observation and action selection is similar to the fault tolerance technique of fault masking [START_REF] Avizienis | Basic Concepts and Taxonomy of Dependable and Secure Computing[END_REF]. This approach exploits the massive redundancy resulting from the combinations and permutations of possible actions that can be carried out in any given situation. Thus, should an adverse situation prevent a subset of actions, it is likely that a sequence of alternate actions exists that allows the system to achieve its objectives. This approach to robustness is mainly implemented by planning and learning.

Planning gives an autonomous system the ability to select sequences of actions to achieve a set of objectives from an initial situation. It implicitly deals with environment uncertainties first by covering a large number of situations, which would be extremely fastidious to implement through imperative programming, and second, by tolerating situations that may not have been envisaged during system design, but which are compatible with its knowledge.

In CIRCA [START_REF] Goldman | Using Model Checking to Plan Hard Real-Time Controllers[END_REF], this approach is taken one step further by taking into account prior knowledge about dangerous situations that may cause system failure. This prior knowledge is expressed as additional constraints input to the planner in order to ensure that the produced plans avoid such situations.

Least-commitment planning also aims to facilitate systematic treatment of adverse situations caused by environment uncertainties. It typically resolves a CSP (Constraint Satisfaction Problem) to minimally constrain the plan produced, and thereby provide temporal and resource flexibility during the plan execution. Adverse situations that were unknown while planning may thus be tolerated. The IxTeT planner from LAAS and the planner from RAX and IDEA implement leastcommitment planning.

Similarly to planning, learning offers a systematic treatment of adverse situations by covering a larger number of situations than could be covered by explicit programming.

2) Detection and contingency procedure triggering: Specific treatment by detection and contingency procedure triggering is similar to the fault tolerance technique of error detection and recovery, as it aims to treat an adverse situation detected beforehand.

a) Detection: Detection is mainly implemented by execution control, situation recognition, and diagnosis.

Execution control supervises the execution of plans produced by the planner. A plan is generally developed under the condition that each of its actions will execute correctly; failure of an action thus indicates the appearance of an adverse situation that has not been taken into consideration by the planner. Execution control is the most used mechanism to detect adverse situations in the LAAS and CLARAty architectures.

Situation recognition uses an event chronicle to identify the current situation of the system and its environment among several generic models specified or learned during development. Work on situation recognition as a detection mechanism and its application may be found in [START_REF] Dousson | Evolution Tracking and Chronical Recognition[END_REF] and [START_REF] Despouys | An Integrated Architecture for Planning and Execution Control in Dynamic Environments[END_REF]. Monitoring of the system for diagnosis is generally used to reveal physical faults affecting the system hardware. However, diagnosis mechanisms may also ascertain the situation of the system and its environment: in [START_REF] Morisset | Robel: Synthesizing and Controlling Complex Robust Robot Behaviors[END_REF] the system learns a Markov Decision Process (MDP) to diagnose its situation, matching values of observable state variables to each type of possible situation.

b) Contingency procedure execution: Specific treatment of an adverse situation is achieved in planning through replanning and plan repair, or in execution control through task retry and modality switching.

Re-planning consists in developing a new plan from the current situation and the objectives yet to be achieved by the system, explicitly taking into account the adverse circumstances that caused the failure of the previous plan. Positioning the system in a safe state may often precede a re-planning. Planners in the LAAS and CIRCA [START_REF] Goldman | Using Model Checking to Plan Hard Real-Time Controllers[END_REF] architectures use replanning.

Plan repair shares the same objectives as re-planning, but seeks a faster solution under the assumption that part of the previous plan may still be valid; execution of this valid partial plan is also executed at the same time as the plan repair. However, plan repair is sometimes impossible, so re-planning is required. The executive planner IxTeT-eXeC from the LAAS architecture [START_REF] Lemai | Interleaving Temporal Planning and Execution in Robotics Domains[END_REF] uses plan repair.

Since a high-level action requested by the planner can be decomposed into several alternative sequences of low-level tasks by the executive, task retry aims to select and execute another sequence of tasks whenever a previous one has failed, until either the action is successful or all decompositions have failed (in which case the action is reported as failed to the planner).

Modality switching extends the principle of task retry: each modality represents a possible decomposition of an action, particularly suited to a specific set of situations. Execution control selects the modality to be executed, and changes modalities when necessary (either when the action has failed, or when another set of situations has been detected). Modality switching may thus be carried out either when a change occurs in the environment (robustness), or when a modality fails due to some system malfunction (fault tolerance). [START_REF] Morisset | Robel: Synthesizing and Controlling Complex Robust Robot Behaviors[END_REF] applies modality switching to robot localization and navigation; [START_REF] Ranganathan | A Reactive Robot Architecture with Planning on Demand[END_REF] presents switching between two navigation modes similar to modalities.

III. TOWARDS FAULT TOLERANCE AND DEPENDABILITY IN AUTONOMOUS SYSTEMS

This section gives first some partial conclusions from our analysis of the current literature and some general recommendations concerning the development of critical autonomous systems. We then discuss the area on which we are focussing our attention.

A. State of the art analysis

Several conclusions can be drawn from the state of the art presented in the previous section.

1) Generally, we feel that the development of autonomous systems is lacking a holistic approach to dependability, through the combined use of its four means (fault prevention, fault removal, fault tolerance and fault forecasting). Currently, fault avoidance (i.e., fault prevention and removal) is largely privileged compared to fault acceptance (i.e., fault tolerance and forecasting).

2) When fault tolerance is considered, the focus is on hardware faults, especially faults that affect sensors and actuators. Nonetheless, fault forecasting studies show that software faults should also be taken into consideration. 3) Very few techniques address fault tolerance with respect to development faults. Robustess techniques contribute somewhat to it, but are surely insufficient for critical applications. 4) The autonomous systems community has yet to develop a measurement culture, both with respect to temporal performance and dependability: for example, we have found very few studies relating to fault forecasting of autonomous systems.

B. Recommendations for developing autonomous systems

This section presents conclusions and recommendations aiming to improve dependability in critical autonomous systems, adapted from [START_REF] Lecubin | SPAAS: Software Product Assurance for Autonomy on-board Spacecraft[END_REF].

1) An inference mechanism (the part of a decisional mechanism that is independent of the application) can be used for different applications, and problems encountered during its verification and validation are similar to those of "classic" software components. In practice however, inference mechanisms and knowledge are generally tightly linked, and it can be impossible to validate them separately. Moreover, validity may be complicated as autonomous systems have to take into account a large number of situations. 2) The use of learning mechanisms is not recommended for critical systems: first it is difficult to establish and ascertain their behavior as it emerges from examples; second, and in particular for online learning, the system behavior evolves without any direct control from the operator. 3) Although autonomous systems are supposed to operate with as little human intervention as possible, it is recommended to allow direct intervention by a human operator should the need arise (e.g., through remote control or an emergency stop switch). 4) A major challenge for development of autonomous systems is the occurrence of unexpected adverse situations. Robustness techniques can aim to ensure acceptable behavior but specific measures have to ascertain whether the system responses are safe and correct. Offline intensive simulation tests and online safety-bag mechanisms are thus strongly recommended. 5) Knowledge used by decisional mechanisms is a key factor in establishing the system behavior. In practice, the problems of correctness and completeness are complicated by the almost unavoidable presence of heuristics, which may trade correctness and completeness for tractability. We feel that more work is needed in this field, concerning first, the dependable formulation of knowledge and second, techniques for handling residual faults in the formulated knowledge.

C. Area of work

Our work aims to devise mechanisms for tolerating development faults in autonomous systems, an area which, as far as we know, is one that is yet to be explored. We focus on decisional mechanisms, and more particularly on their knowledge, as they represent the main distinction between autonomous systems and classic (non-autonomous) computing, for which efficient fault tolerance mechanisms have already been developed.

Two complementary aspects have to be considered: system safety and system reliability.

• The safety aspect aims to render the probability of a catastrophic failure negligible. Mechanisms for ensuring safety focus on the detection of errors that might violate safety constraints followed by positioning the system in a safe state. • The reliability aspect aims to give correct or acceptable timely decisions, that is decisions that first, allow the system to provide a correct or acceptable service, and second, guarantee temporal constraints imposed by the system and environment dynamics. Ensuring reliability despite faults requires some form of error detection and service recovery.

Error detection has to be implemented in both cases. Covering a sufficient set of development faults requires the use of several complementary techniques: timing and execution checks, reasonableness checks, checks by diversified components, and, specifically for the safety aspect, safety-bag checks. Checks by diversified components appear to be difficult to implement in some decisional mechanisms (such as planners) since there are often a large number of valid possible plans, which cannot all be compared. Moreover, two equally valid plans may be strongly dissimilar, making it difficult to define a satisfactory choice criterion. Nonetheless, an automated generation of plan oracles has been successfully implemented during the validation of the RAX system [START_REF] Feather | Automatic Generation of Test Oracles -From Pilot Studies to Application[END_REF].

Concerning the safety aspect, the use of a safety-bag to detect dangerous situations and and position the system in a safe state is attractive for many critical systems. We believe that safety-bags are a promising technique for autonomous systems, since their efficiency is not affected by uncertainties in the system behavior due to the use of decisional mechanisms. Nonetheless, work remains to be done on the expression of safety constraints to be dynamically verified, the actions needed to position the system in a safe state, and possibly more complex reaction capabilities.

Concerning the reliability aspect, two cases can be distinguished: the acceptability of decisions, and their timeliness. The acceptability of decisions can be disrupted by compromises in development, faults in decisional mechanisms, or environment changes 1 ; we think that knowledge diversification, either in the heuristics or in the domain-specific model of a decisional mechanism, is a potential fault tolerance mechanism for addressing this concern. To improve the timeliness of decisions, possible fault tolerant techniques include concurrent 1 According to concepts presented in the first part of this article, problems raised by environment changes relate to robustness rather than fault tolerance. use of different heuristics, or a relevant selection according to the type of problem addressed by the system.

IV. FUTURE DIRECTIONS

We are currently focussing on fault tolerance techniques addressing the reliability aspect of decisional mechanisms. We present below some possible alternatives for implementing fault tolerance in decisional mechanisms and then propose an experimental framework for assessing their efficiency. We are currently implementing this framework, prior to prototyping some of the evoked mechanisms.

A. Fault tolerance capabilities for decisional mechanisms

This section presents several possible research paths that we have identified for improving fault tolerance in decisional mechanisms.

1) Agent-based type of architecture: Although the "threelayer" type of architecture [START_REF] Gat | On Three-Layer Architectures[END_REF] is by far preponderant today in the development of complex autonomous systems, the agentbased type of architecture proposed in IDEA [START_REF] Muscettola | IDEA: Planning at the Core of Autonomous Reactive Agents[END_REF] offers a promising alternative. It actually considers an autonomous system as a group of multiple "agents", each possessing deliberative mechanisms and the same symbolic representation, and implementing a different system function (Figure 3). Each agent is capable of making independent decisions and taking actions to satisfy local goals based on requests from other agents and its perceived environment. In comparison with more classical architectures, we think that several aspects of the agent-based type of architecture may improve system dependability and robustness:

• The same symbolic representation is used by the planning and executive components of all agents, thus limiting the risks of semantic mismatch (particularly model mismatch) between planning and execution control (fault avoidance). • The flexibility of modular agent-based programming may allow the system to correctly react to a larger set of adverse situations than other more monolithic architectures. • The system is explicitly divided into task-specific components (the agents), which may diminish error propagation and facilitate error recovery (fault tolerance).

2) Plan analysis: As a decisional mechanism may generate erroneous plans (for example because of residual development faults in the model), it is interesting to check on-line the validity of a plan before its execution, that is whether it contains inconsistencies, and possibly whether it advances the system towards achieving its goals. Such an error detection mechanism could trigger some form of forward recovery. It might be possible to develop an on-line acceptance test based on the previously mentioned work by Feather and Smith on oracles for off-line testing of the correctness of plans produced by the DS1 planner [START_REF] Feather | Automatic Generation of Test Oracles -From Pilot Studies to Application[END_REF].

3) Heuristic diversification: As previously stated, heuristics are used in decisional mechanisms to deal with the computational complexity of an AI algorithm, often at the cost of its completeness. Moreover, a heuristic is generally specialized: its use gives good performance on particular types of problems, but is not able to solve others. We think that using several diversified heuristics rather than a single one may deal with these difficulties. Two possibilities can be considered:

• The heuristics are executed competitively for each problem, and the system chooses to execute the solution given by the first heuristic to satisfy an evaluation criterion, for example the first heuristic to find a solution, or the first to find a correct solution in spite of development faults if this correctness may be assessed by a corresponding acceptance test, e.g., by plan analysis as previously presented (compensation recovery).

• One heuristic is privileged and executed first; other heuristics may be successively tried if no (correct) solution is found in a set time (forward recovery). Either way, a set of heuristics adapted to the different problems that the decisional mechanism may face needs to be identified. An analysis and classification of the heuristics regarding the type of problems that they solve efficiently may be particularly useful to help choose the successive order of the heuristics to be executed in our forward recovery proposition.

4) Model diversification: Diversification of the model consists in the implementation of different descriptions of the system, environment, tasks, or procedures used by the decisional mechanism to draw inferences. The decisional mechanism detects the presence of an adverse situation when an executive procedure or a plan produced from one of these models fails (although it is unable to ascertain whether this situation is caused by a system fault or by an environmental uncertainty). It may then try to recover from the possible failure by switching to another model and re-planning. This technique aims to tolerate development faults in the model descriptions, in a similar way to software diversification in classic computing systems. Whether it is efficient for autonomous systems remains to be seen.

B. Fault tolerance comparison between different decisional mechanisms

The implementation of any fault tolerance mechanism often negatively impacts the system performance and development costs, principally because it requires redundancy at some level to detect an error or accomplish a recovery. Evaluation of such mechanisms is thus essential to ascertain whether their effectiveness outweighs their overheads. We present in this section the simulation and fault injection environment that we are currently implementing to experimentally evaluate the efficiency of the various possibilities previously presented.

The use of simulation rather than the execution of the actual system is mainly motivated by two reasons:

• The large number of experiments required to perform a significant evaluation: experiments on real systems usually need more time to be executed, and are more difficult to automate. • The hazardous behavior of the system during an experiment: as we inject faults in the system, we cannot predict its behavior, which may cause damage to itself or its direct surroundings. Previous studies have demonstrated that fault injection may efficiently simulate real software faults [START_REF] Daran | Modelling Erroneous Software Behavior and Application to Testset Validation by Fault Injection[END_REF] [START_REF] Jarboui | Computer System Dependability. Benchmarking and Fault Representativeness[END_REF]. We particularly focus on two techniques:

• Mutation of a program source is the introduction of a unique fault through the modification of a particular line of code. It simulates programming faults accurately, but is generally costly in time as one mutated version of the program must be compiled for each fault. • Interception and modification of the inputs or outputs of a program aims to simulate errors caused by the fault rather than the fault itself. 1) Simulation environment: The simulation environment that we intend to use is represented in Figure 4. Different decisional mechanisms can be implemented on top of a hardware interface (composed of Genom modules from the LAAS architecture), providing requests to a virtual robot that operates as part of the simulation environment. This environment may be decomposed into three elements: a robot simulator named Gazebo2 , an interface library named Pocosim, and some modules from the functional layer of a three-layer type of architecture.

• The robot simulator Gazebo is used to simulate the physical world and the actions of the autonomous system; it takes as input a file describing the environment of the simulation (mainly a list of static or dynamic obstacles containing their position, and the physical description of the robot) and executes the movement of the robot and dynamic obstacles, and possible interactions between objects.

• The Pocosim library [START_REF] Joyeux | Simulation in the LAAS Architecture[END_REF] is a software bridge between the simulated robot (executed on Gazebo) and the software commands generated by the Genom modules: it transforms commands to the actuators into movements or actions to be executed on the simulated robots, and relays the sensor inputs that Gazebo produces from the simulation. • The Genom modules [START_REF] Fleury | Genom: A Tool for the Specification and the Implementation of Operating Modules in a Distributed Robot Architecture[END_REF] compose the hardware interface between decisional mechanisms and the simulated hardware: they execute non-decisional algorithms and generate commands to the simulated system from requests given by upper-level components. Special libraries must be used with the modules that are supposed to control the hardware components of the system, in order to link them with the Pocosim bridge; other modules are integrated as they are. Existing modules can be used without modifying their source code.

The Genom modules receive requests from, and send reports to, the upper decisional mechanisms, including the decisional mechanism to be evaluated. Typically, these decisional mechanisms may be a planner and an executive (as in a classic three-layer type of architecture), or a hierarchy of agents (as in multi-agent type of architecture).

Currently, we are integrating the different components of the simulation environment with the OpenPRS executive and the IxTeT-eXeC temporal executive and planner of the LAAS architecture. From this base, we should be able to implement the various possibilities evoked in section IV-A: most techniques imply only modifying (or possibly replacing) the IxTeT-eXeC component. However, the comparison with the agent-based architecture requires replacing both IxTeT-eXeC and OpenPRS by agents possessing equivalent knowledge in order for the comparison to be valid. This may prove difficult since the programming approaches for the two systems are not similar.

2) Fault injection: In order to establish a campaign of experiments for assessing the fault tolerance capabilities of a particular decisional mechanism, we need to determine four different aspects (Figure 5) [START_REF] Arlat | Fault Injection for Dependability Validation -A Methodology and Some Applications[END_REF]: the faults (or faultload) to be injected into the system, the activity (or workload) that the robot will execute during an experiment, the results that we need to observe and store, and the measures that we will use to sum up the results and compare the different systems. For the measures to be representative, a sufficient number of experiments must be performed: automation of experiments is thus imperative (e.g., through the use of shell scripts).

OPENPRS

IxTeT-eXeC • Faultload: Each experiment focusses on a specific fault; to narrow our focus, we consider only software faults affecting decisional mechanisms. Faults may be injected either by mutating the model given to the planner, or by intercepting and modifying (for example by bit-flipping) a report or a request between the planner and the executive. As the model is generally directly parsed by the decisional mechanisms, there is no need to compile the mutants obtained from the model. • Workload: The activity encompasses the task that the system must carry out, and the environment in which it will evolve. We have chosen the case of a space rover, required to take pictures of particular locations, to upload them into a remote database during given communication windows, and to return home in a set time. An environment is a set of static obstacles unknown to the robot (possibly blocking the system from executing one of its goals), which introduces uncertainties and stresses the system navigation mechanism. Each experiment should be composed of different runs using different environments, in order to activate the system's functionalities as broadly as possible.

¡ ¡ ¢ ¢ ¢ £ £ ¤ ¤ ¥ ¥ ¦ ¦ ¦ § §
• Results: To establish relevant measures, we need to gather results concerning whether the injected fault has been activated during the experiment, and possibly whether it has been detected and correctly identified by the system. We also need to know the list of different objectives that the system has successfully completed. Other useful results include the distance covered by the system and the duration of its activity. The information pertaining to system activity (completion of objectives, distance and duration) must be obtained from Gazebo during the execution of an experiment, whereas information concerning treatment of the fault and its subsequent error(s) must be obtained through observation of the targeted decisional mechanism.

• Measures: Measures consist of dependability-specific measures and other performance measures. Dependability measures encompass principally the coverage of each decisional mechanism implemented with respect to the faults injected and activated, and the error detection latency. Performance measures quantify the degree of success of the system regarding its mission: the mean number of goals it has achieved, and the mean time and distance required.

CONCLUSION

In this article, we have presented several basic concepts:

• Robustness and fault tolerance, both characterizing the resilience of a system towards particular adverse situations; robustness characterizes resilience towards uncertainties of the environment, and fault tolerance characterizes resilience towards faults affecting the system resources.

• Decisional mechanisms are central to autonomous systems as they embody the ability to dynamically select appropriate actions to achieve specific objectives; they are composed of knowledge specific to a domain of application and an inference mechanism used to solve problems. We also summarized the state of the art in dependability and robustness mechanisms used in autonomous systems, and some conclusions that we drew from it. In particular:

• Fault avoidance is largely privileged compared to other dependability means, although it rarely appears to be implemented intensively enough. • Development faults are hardly addressed by fault tolerant mechanisms in autonomous systems; robustness techniques somewhat compensate this problem, but are surely insufficient for critical applications. We presented our specific area of interest: the development of fault tolerance mechanisms for autonomous systems, and more particularly techniques for tolerating residual faults in the knowledge used by decisional mechanisms. Two aspects can be considered:

• The safety aspect aims to minimize the probability of a catastrophic failure. We believe that the use of safety-bags may be efficient to detect unsafe system commands and react by positioning the system in a safe state, but more work is needed on the expression of safety constraints to be checked by the safety-bag. • The reliability aspect distinguishes two cases: the acceptability of decisions and their timeliness. Reliability in the presence of faults requires error detection and system recovery. We are currently focussing on this particular aspect. We finally described the current and future directions of our work. We presented four possible research paths to improve fault tolerance in decisional mechanisms:

• The use of agent-based type of architecture to take advantage of their flexibility and internal semantic consistency. • Plan analysis for detecting errors on-line by checking the validity of plans before their execution.

• Heuristics diversification to tolerate residual faults in the heuristics or their inability to treat specific situations. • Model diversification to implement redundant models to compensate for possible faults in domain-specific knowledge.

Figure 2 :

 2 Figure 2: Internal faults in decisional mechanisms

Figure 3 :

 3 Figure 3: Agent-based type of architecture: IDEA principle

Figure 4 :

 4 Figure 4: Simulation environment

Figure 5 :

 5 Figure 5: Proposed experimental framework

From the "player/stage project", http://playerstage.sourceforge.net

We also presented an experimental framework based on simulation and fault injection that we are currently implementing to assess the efficiency of these mechanisms.