Patricia Bouyer
email: bouyer@lsv.ens-cachan.fr

Franck Cassez
email: cassez@irccyn.ec-nantes.fr

François Laroussinie

Modal Logics for Timed Control ⋆

In this paper we use the timed modal logic Lν to specify control objectives for timed plants. We show that the control problem for a large class of objectives can be reduced to a model-checking problem for an extension (L cont ν ) of the logic Lν with a new modality. More precisely we define a fragment of Lν , namely L det ν , such that any control objective of L det ν can be translated into a L cont ν formula that holds for the plant if and only if there is a controller that can enforce the control objective. We also show that the new modality of L cont ν strictly increases the expressive power of Lν while model-checking of L cont ν remains EXPTIMEcomplete.

Introduction

Control problem. The control problem (CP) for discrete event systems was first studied by Ramadge & Wonham in [RW89]. The CP is the following: "Given a finite-state model of a plant P (open system) with controllable and uncontrollable discrete actions, a control objective Φ, does there exist a controller f such that the plant supervised by f (closed system) satisfies Φ?"The dense-time version of the CP with an untimed control objective has been investigated and solved in [MPS95]. In this seminal paper, Maler et al. consider a plant P given by a timed game automaton which is a standard timed automaton [AD94] with its set of discrete actions partitioned into controllable and uncontrollable actions. They give an algorithm to decide whether a controller exists or not, and show that if one such controller exists a witness can be effectively computed. In [WT97] a semi-algorithm has been proposed to solve the CP when the plant is defined by a hybrid (game) automaton.

Specification of control properties. In the aforementioned papers the control objective is either a safety or reachability property (or some simple Büchi conditions). In [dAHM01] the authors give an algorithm to deal with general ω-regular control objectives. It is to be noticed that those control objectives are ⋆ Work supported by ACI Cortos, a program of the French government.

often called internal in the sense that they refer to the state properties (and clocks) of the system to be controlled. In the case of timed systems they only refer to the untimed sequences of states of the system and thus have a restrictive expressiveness: it is possible to specify a property like "after p has been reached q will be reached" but nothing like "after p has been reached, q will be reached within less than d time units" (bounded liveness). Moreover, in the verification methodology for closed systems, one usually models (and thinks of) the plant P and the controller f as a closed system f (P ), and specifies a property ϕ with a suitable timed temporal logic and check whether the closed system f (P ) satisfies ϕ. It is then very natural to have similar logics in the game framework to specify timed control objectives for open systems.

Our contribution. The logic L ν [LL95] is a subset of the timed µ-calculus that can be used for specifying timed safety properties of closed timed systems. Modalities of L ν seem to be appropriate to specify timed control objectives as well because we can use existential and universal quantifications over discrete actions (as it is used in the untimed framework of [AVW03,RP03]), and also over time delays. The control problem CP for a plant (specified as a timed automaton) and a control objective in L ν expresses as folloes:

Given a timed automaton P , the plant, and a L ν formula ϕ, the safety control objective, is there a controller f s.t. f (P ) |= ϕ?

(CP)

So far there is no constraint neither on the structure nor on the power of the controller f we are looking for: it may even require unbounded memory or arbitrary small delays between two consecutive controllable actions. In this paper we focus on controllability (CP) and not on the controller synthesis problem (i.e. exhibit a witness controller).

The main result of the paper is that we can reduce CP for a plant P and an L ν control objective ϕ, to a standard model-checking problem on the plant P and a formula ϕ c of a more expressive logic L cont ν , that extends L ν with a new modality. More precisely we exhibit a deterministic fragment of L ν , namely L det ν , s.t. for all ϕ ∈ L det ν , the following reduction (RED) holds:

There exists a controller f s.t. f (P ) |= ϕ ⇐⇒ P |= ϕ c (RED)

where ϕ c is a formula of L cont ν . We also give an effective procedure to obtain ϕ c from ϕ. Further on we study the logic L cont ν and prove that it is strictly more expressive than L ν , which is a technically involved result on its own. We also show that the new modality of L cont ν is not necessary when we restrict our attention to sampling control (the controller can do an action every ∆ time units) or to Known Switch Conditions Dense-Time control (where time elapsing is uncontrollable [CHR02]). A natural question following equation (RED) above is to study the model-checking problem for timed automata against L cont ν specifications. In the paper we prove that i) the model-checking of L cont ν over timed automata is EXPTIME-complete; ii) L cont ν inherits the compositionality property of L ν .

Related work. In the discrete (untimed) case many logics used to specify correctness properties of closed systems have been extended to specify control objectives of open systems. ATL [AHK02] (resp. ATL * ) is the control version of CTL (resp. CTL * ). More recently [AVW03,RP03] have considered a more general framework in which properties of the controlled system are specified in various extensions of the µ-calculus: loop µ-calculus for [AVW03] and quantified µ-calculus for [RP03]. In both cases the control problem is reduced to a model-checking (or satisfiability) problem as in equation (RED). In the timed framework, external specifications have been studied in [DM02]: properties of the controlled system are specified with timed automata, and in [FLTM02], the control objective is given as a formula of the logic TCTL.

Outline of the paper. In section 2 we define basic notions used in the paper: timed systems, logic L ν and variants and the control problem. In section 3 we prove that (RED) holds and also that ϕ c is in L ν for two simpler control problems. Section 4 is devoted to the study of the logic L cont ν (expressiveness, decidability, and compositionality).

The proofs are omitted and can be found in [BCL05].

2 Timed Automata and the Timed Modal Logic L ν

We consider as time domain the set R ≥0 of non-negative reals. Act is a finite set of actions. 1 We consider a finite set X of variables, called clocks. A clock valuation over X is a mapping v : X → R ≥0 that assigns to each clock a time value. The set of all clock valuations over X is denoted R X ≥0 . Let t ∈ R ≥0 , the valuation v + t is defined by (v + t)(x) = v(x) + t for all x ∈ X. For Y ⊆ X, we denote by v[Y ← 0] the valuation assigning 0 (resp. v(x)) for any x ∈ Y (resp.

x ∈ X \ Y ). We denote C(X) the set of clock constraints defined as the conjunctions of atomic constraints of the form x ⊲⊳ c with x ∈ X, c ∈ Q ≥0 and ⊲⊳ ∈ {<, ≤, =, ≥, >}. For g ∈ C(X) and v ∈ R X ≥0 , we write v |= g if v satisfies g and g denotes the set {v ∈ R X ≥0 | v |= g}.

Timed Transition Systems & Timed Automata

Timed transition systems. A timed transition system (TTS) is a tuple S = (Q, q 0 , Act, -→ S ) where Q is a set of states, q 0 ∈ Q is the initial state, and

-→ S ⊆ Q × (Act ∪ R ≥0 ) × Q is a set of transitions.
If (q, e, q ′ ) ∈-→ S , we also write q e --→ S q ′ . The transitions labeled by a ∈ Act (resp. t ∈ R ≥0 ) are called action (resp. delay) transitions. We make the following common assumptions about TTSs [Yi90]:

-0-delay: q 0 --→ S q ′ if and only if q = q ′ , 1 We assume that Act and R ≥0 are disjoint.

-

Additivity: if q d --→ S q ′ and q ′ d ′ --→ S q ′′ with d, d ′ ∈ R ≥0 , then q d+d ′ ----→ S q ′′ , -Continuity: if q d --→ S q ′ , then for every d ′ and d ′′ in R ≥0 such that d = d ′ +d ′′ ,
there exists q ′′ such that q

d ′ --→ S q ′′ d ′′ ---→ S q ′ , -Time-determinism: if q e --→ S q ′ and q e --→ S q ′′ with e ∈ R ≥0 , then q ′ = q ′′ . A run is a finite or infinite sequence ρ = s 0 e1 --→ S s 1 e2 --→ S • • • en ---→ s n • • • We denote by first(ρ) = s 0 . If ρ is finite, last (ρ) denotes the last state of ρ.
Runs(q, S) is the set of runs in S starting from q and Runs(S) = Runs(q 0 , S). We use q e --→ S as a shorthand for "∃q ′ s.t. q e --→ S q ′ " and extend this notation to finite runs ρ e --→ S whenever last (ρ) e --→ S . Timed automata. A timed automaton (TA) [AD94] is a tuple A = (L, ℓ 0 , Act, X, inv, T ) where L is a finite set of locations, ℓ 0 ∈ L is the initial location, X is a finite set of clocks, inv : L → C(X) is a mapping that assigns an invariant to each location, and

T ⊆ L × [C(X) × Act × 2 X ] × L is a finite set of transitions 2 . The semantics of a TA A = (L, ℓ 0 , Act, X, inv, T ) is a TTS S A = (L × R X ≥0 , (ℓ 0 , v 0 ), Act, -→ SA ) where v 0 (x) = 0 for all x ∈ X and -→ SA consists of: i) action transition: (ℓ, v) a --→ SA (ℓ ′ , v ′ ) if there exists a transition ℓ g,a,Y -----→ ℓ ′ in T s.t. v |= g, v ′ = v[Y ← 0] and v ′ |= inv(ℓ ′ ); ii) delay transitions: (ℓ, v) t --→ SA (ℓ, v ′ ) if t ∈ R ≥0 , v ′ = v + t and v, v ′ ∈ inv(ℓ). A TA is deterministic w.r.t. Σ ⊆ Act if for all a ∈ Σ, if (ℓ, g 1 , a, Y 1 , ℓ 1 ) ∈ T and (ℓ, g 2 , a, Y 2 , ℓ 2 ) ∈ T then g 1 ∩ g 2 = ∅.

The Modal Logics

L ν , L det ν and L cont ν
The modal logic L ν [LL95,LL98]. The logic L ν over the finite set of clocks K, the set of identifiers Id, and the set of actions Act is defined as the set of formulae generated by the following grammar:

ϕ ::= tt | ff | ϕ ∧ ϕ | ϕ ∨ ϕ | x in ϕ | x ⊲⊳ c | [a] ϕ | a ϕ | [δ] ϕ | δ ϕ | Z where a ∈ Act, x ∈ K, ⊲⊳ ∈ {<, ≤, =, ≥, >}, c ∈ Q ≥0 , Z ∈ Id.
The meaning of the identifiers is specified by a declaration D assigning a L ν formula to each identifier. When D is understood we write

Z = ν Ψ Z if D(Z) = Ψ Z . We define the following shorthands in L ν : r in ϕ def = x 1 in x 2 in • • • in x n in ϕ if r = {x 1 , • • • , x n } ⊆ K.
Let S = (Q, q 0 , Act, -→ S ) be a TTS. L ν formulae are interpreted over extended states (q, v) where for q ∈ Q and v ∈ R K ≥0 . We write "S, (q, v) |= ϕ" when an extended state (q, v) satisfies ϕ in the TTS S. This satisfaction relation is defined as the largest relation satisfying the implications in Table 1. The modalities e with e ∈ Act ∪ {δ} correspond to existential quantification over action or delay transitions, and [e] is the counterpart for universal quantification. An extended state satisfies an identifier Z (denoted S, (q, v) |= Z) if it belongs to the maximal fixedpoint of the equation Z = ν Ψ Z . Finally the formula clocks are used to measure time elapsing in properties. We define ϕ S = {(q, v) | S, (q, v) |= ϕ}. We write S |= ϕ for S, (q 0 , v 0 ) |= ϕ where v 0 (x) = 0 for all x ∈ K. The logic L ν allows us to express many behavioural properties of timed systems [LL98]. For example the formula Z defined by Ψ Z = ( a∈Act [a] Z ∧ [δ] Z ∧ ϕ) holds when all reachable states satisfy ϕ. Other examples of formulae will be given later on in the paper.

S, (q, v) |= α =⇒ α with α ∈ {t t, f f} S, (q, v) |= x ⊲⊳ c =⇒ v(x) ⊲⊳ c S, (q, v) |= Z =⇒ S, (q, v) |= ΨZ S, (q, v) |= ϕ1 op ϕ2, =⇒ S, (q, v) |= ϕ1 op S, (q, v) |= ϕ2 with op ∈ {∧, ∨} S, (q, v) |= x in ϕ =⇒ S, (q, v[x ← 0]) |= ϕ S, (q, v) |= [a] ϕ =⇒ for all q a --→S q ′ , S, (q ′ , v) |= ϕ S, (q, v) |= a ϕ =⇒ there is some q a --→S q ′ , S, (q ′ , v) |= ϕ S, (q, v) |= [δ] ϕ =⇒ for all t ∈ R ≥0 s.t. q t --→S q ′ , S, (q ′ , v + t) |= ϕ S, (q, v) |= δ ϕ =⇒ there is some t ∈ R ≥0 s.t. q t --→S q ′ , S, (q ′ , v + t) |= ϕ Table 1. Satisfaction implications for L ν
The modal logic L cont ν . As we will see later in the paper, the modal operators of L ν are not sufficient to express dense-time control. Indeed we need to express the persistence (w.r.t. time elapsing) of a property until a controllable action is performed: we thus need to express that some property is true only for a subset of the states of the plant which are reachable by time elapsing before a controllable action leading to good states is possible. This kind of property cannot be expressed using the [δ] and δ operators. This is why we define the new modality [δ , the semantics of which is defined over an extended configuration (q, v) of a TTS S as follows:

S, (q, v) |= ϕ [δ ψ ⇔ either ∀t ∈ R ≥0 , q t --→ S q ′ ⇒ S, (q ′ , v + t) |= ϕ or ∃t ∈ R ≥0 s.t. q t --→ S q ′ and S, (q ′ , v + t) |= ψ and ∀0 ≤ t ′ < t, q t ′ --→ S q ′′ we have S, (q ′′ , v + t ′ ) |= ϕ (1)
Let L cont ν be the timed modal logic which extends L ν by adding the modality [δ . This operator is some kind of "Until" modality over delays. In [HNSY94] the timed µ-calculus which is studied contains a modality £ the semantics of which is close to the semantics of [δ (the main difference between £ and [δ is that £ may include an action transition after the delay).

A deterministic fragment of L ν , L det ν . In the following we will restrict the possible control objectives to properties expressed in a subset L det ν of L ν . Indeed, we want to define a transformation such that equation (RED) given in the introduction holds, the restriction is then motivated by the following remark: Remark 1. A control objective of L ν like ϕ 1 ∧ ϕ 2 intuitively requires to find a controller that both ensures ϕ 1 and ϕ 2 . In an inductive construction, this amounts to build a controller that ensures ϕ 1 ∧ ϕ 2 from two controllers: one that ensures ϕ 1 and an other that ensures ϕ 2 . This means that we must be able to merge controllers in a suitable manner. The definition of L det ν will syntactically ensure that the conjunctions of L det ν formulae can be merged safely, i.e. that they are in some sense deterministic. Indeed, any (first-level) subformula of a conjunction in L det ν will be prefixed by a modal operator with a particular action, and then the existence of a controller for ϕ 1 and another one for ϕ 2 entails the existence of a controller for ϕ 1 ∧ ϕ 2 . In the untimed case, some kind of "deterministic" form is also used (the socalled disjunctive normal form), but this is not a restriction as all formulae of the µ-calculus can be rewritten in a disjunctive normal form [JW95]. One hope could be to be able to transform any formula of L ν into an equivalent formula of L det ν , but we do not know yet if this is possible. Note that in the untimed framework, transforming formulae of the µ-calculus into formulae in disjunctive normal form is strongly related to the satisfiability problem, and in the timed case, the satisfiability problem for

L ν is still an open problem [LLW95].
We first define basic terms B ν by the following grammar:

α ::= tt | ff | x ⊲⊳ c | r in a ϕ | r in [a] ϕ with x ∈ K, r ⊆ K, c ∈ Q and a ∈ Act ∪ {δ} and ϕ ∈ L det ν (L det ν is defined hereafter). A set of basic terms A = {α 1 , α 2 , • • • , α n } is deterministic if for all σ ∈ Act∪{δ} there is at most one i s.t. α i = r in σ ϕ or α i = r in [σ]ϕ.
We then define L det ν as the deterministic fragment of L ν inductively defined as follows:

L det ν ∋ ϕ, ψ ::= X | ϕ ∨ ψ | α∈A α
with X ∈ Id and A a (finite) deterministic set of basic terms. With this restriction on the conjunctions, if there are controllers f α for all α ∈ A, we can merge them to obtain a controller for α∈A α (see remark 1 above).

Note that already many properties can be expressed in the fragment L det ν , for example safety and bounded liveness properties:

X 1 = [Bad] ff ∧ a =Problem,Bad [a] X 1 ∧ [Problem] (z in X 2 ) ∧ [δ] X 1 X 2 = z < d max ∧ [Bad] ff ∧ [Alarm] X 1 ∧ a =Alarm,Bad [a] X 2 ∧ [δ] X 2
The above formula expresses that the system is always safe (represented by property [Bad] ff), and that every Problem is followed in less than d max time units by the Alarm. The previous formula can also be specified using simpler formalism (e.g. test automaton [ABBL03]) but this is not the case for every L det ν formula. The formula X = [δ] X ∧ a∈Act [a] X ∧ δ b tt for some b ∈ Act, which means that there is always some delay s.t. b is enabled cannot be expressed with test automata.

The Control Problem

Definition 1 (Fair Plant). A fair plant (plant in the sequel) P is a TA where Act is partitionned into Act u and Act c and s.t. 1) it is deterministic w.r.t. every a ∈ Act c ; 2) in every state (ℓ, v) the TA P can let time elapse or do an uncontrollable action.

A controller [MPS95] for a plant, is a function that during the evolution of the system constantly gives information as to what should be done in order to ensure a control objective Φ. In a given state the controller can either i) "enable some particular controllable action" or ii) "do nothing at this point in time, just wait" which will be denoted by the special symbol λ. Of course a controller cannot prevent uncontrollable actions from occurring. Nevertheless, we assume that the controller can disable a controllable action at any time, and this will not block the plant because the plant is fair.

Definition 2 (Controller). Let P = (L, ℓ 0 , Act, X, inv, T ) be a plant. A controller 3 f over P is a partial function from Runs(S P ) to Act c ∪ {λ} s.t. for any finite run ρ ∈ Runs(

S P ), if f (ρ) is defined 4 then f (ρ) ∈ {e | ρ e -→ SP }.
The purpose of a controller f for a plant P is to restrict the set of behaviours in S P in order to ensure that some property holds. Closing the plant P with f produces a TTS (set of runs) corresponding to the controlled plant: Definition 3 (Controlled plant). Let P = (L, ℓ 0 , Act, X, inv, T ) be a plant, q ∈ S P and f a controller over P . The controlled plant f (S P , q) is the TTS (Q, q, Act, -→ f ) defined inductively by:

-q ∈ Q, -if ρ ∈ Runs(f (S P , q)), then last(ρ) e --→ f q ′ and q ′ ∈ Q, if last(ρ) e --→ SP q ′
and one of the following three conditions hold: 1. e ∈ Act u , 2. e ∈ Act c and e ∈ f (ρ),

3. e ∈ R ≥0 and ∀0 ≤ e ′ < e, ∃last (ρ) e ′ --→ SP q ′′ s.t. λ = f (ρ e ′ --→ SP q ′′ ).
We note f (P ) the controlled plant P by controller f from initial state of P .

3 The notation f comes from the fact that a controller is specified as a function, as strategies in game theory. 4 ρ λ -→S P stands here for ∃t > 0 s.t. last(ρ)

t -→S P s ′ .
The ∆-dense-time control problem amounts to finding a controller for a system s.t. at least ∆ ≥ 0 time units elapse between two consecutive control actions. Such a controller is called a ∆-controller and can prevent time elapsing and force a controllable action to happen at any point in time if the time elapsed since the last controllable move is more than ∆. If ∆ = 0 we admit controllers that can do two consecutive actions separated by arbitrary small delays (even 0-delay), i.e. controllers that have infinite speed. If ∆ > 0, the ∆-controllers are forced to be strongly non-zeno. We note Contr ∆ (P ) the set of ∆-controllers for plant P .

Definition 4 (∆-Dense-Time Control Problem). Let P = (L, ℓ 0 , Act, X, inv, T ) be a plant, ϕ ∈ L det ν , a (deterministic) safety control objective, and ∆ ∈ Q ≥0 . The ∆-Dense-Time Control Problem (∆-CP for short) asks the following:

Is there a controller f ∈ Contr ∆ (P ) such that f (P ) |= ϕ?

(∆-CP)

Remark 2. In the above ∆-CP, we look for controllers which can do a controllable action only if the time elapsed since the last controllable action is at least ∆. We could specify many other classes of controllers: for example we could impose the controller doing controllable actions exactly every ∆ units of time (this is called sampling control -see later), or to alternate controllable actions.

Notice that this fits very well in our framework as we will see in section 4 that L det ν is compositional : any reasonable constraint on the controller can be given as an extra (timed) automaton and taken into account simply by synchronizing it with the plant P . For example the ∆-controllers can be specified by an extra self-loop automaton where the loop is constrained by a guard x ≥ ∆, any controllable action can be done, and clock x is reset. In the following we note P ∆ the synchronized product of P with this self-loop automaton (see [AD94] for the definition of the classical synchronisation product).

From Control to Model Checking

In this section, we prove that for any control objective defined as a L det ν formula ϕ, we can build an L cont ν formula ϕ that holds for P ∆ iff there exists a ∆controller which supervises plant P in order to satisfy ϕ. This corresponds to equation (RED) we have settled in the introduction.

Dense-Time Control Problem

Let ϕ be a L det ν formula and σ ∈ Act c ∪ {λ}, we define the formula ϕ σ by the inductive translation of Fig. 1. Intuitively, formula ϕ ac will hold when there is a controller which ensures ϕ and which starts by enforcing controllable action a c whereas formula ϕ λ will hold when there is a controller which ensures ϕ and which starts by delaying. We use the shortcut ϕ to express that nothing is required for the strategy, which will correspond to σ∈Actc∪{λ} ϕ σ .We also use λ tt as a shortcut for ac∈Actc [a c ] ff. Note that the new operator [δ is used in the formula [δ] ϕ σ . This translation rule introduces the superscript a c in the disjunctive right argument of [δ . This just means that we can actually prevent time from elapsing at some point, if we perform a controllable action.

α∈A α σ def = α∈A α σ _ α∈A α σ def = _ α∈A α σ a ϕ σ def = 8 < : f f if σ, a ∈ Actc ∧ σ = a a ϕ ∧ σ t t if a ∈ Actu a ϕ otherwise x ∼ c σ def = x ∼ c ∧ σ t t δ ϕ σ def =  δ ϕ if σ = λ ϕ σ if σ ∈ Actc r in ϕ σ def = r in ϕ σ [ac] ϕ σ def =  σ t t if ac = σ ac ϕ if ac = σ [au] ϕ σ def = [au] ϕ ∧ σ t t [δ] ϕ σ def = 8 < : ϕ σ if σ ∈ Actc ϕ λ [δ " _ ac∈Actc ϕ ac " otherwise X σ def = Xσ ∧ σ t t Fig. 1. Definition of ϕ σ , ϕ ∈ L det ν and σ ∈ Act c ∪ {λ}
We can now state our main theorem about controllability:

Theorem 1. Given P a plant, ϕ ∈ L det ν a control objective, ∆ ∈ Q ≥0 , we then have:

∃f ∈ Contr ∆ (P ) s.t. f (P ) |= ϕ ⇐⇒ P ∆ |= ϕ (2)
The proof of Theorem 1 can be done by induction on the structure of the formula and is given in [BCL05].

This theorem reduces the controllability problem for properties expressed in L det ν to some model-checking problem for properties expressed in L cont ν . Note however that this theorem does not provide a method to synthesize controllers: indeed L ν and L cont ν are compositional logics (see in the next section), controller synthesis is thus equivalent to model synthesis. But, as already said, the satisfiability problem (or model synthesis) for L ν is still an open problem [LLW95]. Note also that as L cont ν is compositional (see next section), verifying P ∆ |= ϕ reduces to checking P |= ϕ /S ∆ where S ∆ is the self-loop automaton mentioned before.

Known-Switch Condition Dense-Time Control

Known-switch condition (KSC) dense-time control [CHR02] corresponds to the control of the time-abstract model of a game: intuitively this assumes that time elapsing is not controllable. A controller can thus choose to do a controllable action a ∈ Act c or to do nothing (λ), but in the latter case the controller does not control the duration of the next continuous move. To see that L ν is sufficient to express KSC dense-time control, we just need to focus on formula of the type [δ] ϕ as this is the only formula that may need the use of the [δ operator when translated into a model-checking formula. More precisely we only need to focus on the translation of [δ] ϕ λ as this is the only case that can generate a [δ formula. It is then clear that if the controller chooses λ, and as it has no way of controlling time-elapsing in the time-abstract system, it must ensure ϕ in all possible future positions in S. Thus [δ] ϕ λ simply reduces to [δ] ϕ λ . Thus L ν is sufficient to express KSC dense-time control.

Sampling Control

The sampling control problem is a version of the control problem where the controller can perform a controllable action only at dates k.∆ for k ∈ N and ∆ ∈ Q. ∆ is the sampling rate of the controller. Let P be a plant. As emphasized earlier in this section for the ∆-dense-time control, we can build a plant P ∆ where all the controllable actions are required to happen at multiple values of the sampling rate ∆. This can be done by defining a timed automaton B ∆ with one location ℓ 0 , a fresh clock y, the invariant inv(ℓ 0 ) ≡ y ≤ ∆ and a number of loops on ℓ 0 : for each a c ∈ Act c there is a loop (ℓ 0 , y = ∆, a c , {y}, ℓ 0 ). Moreover we want to leave the controller free to do nothing. To this end we add a new controllable action reset and a loop (ℓ 0 , y = ∆, reset, {y}, ℓ 0 ). As this action is not in P , it is harmless to do it and when the controller does not want to do an action, it can always choose to do reset.

Thus we can design an equivalent version of the sampling control where the controller is bound to do a controllable action at each date k.∆ with k ∈ N.

As in the previous case of KSC dense-time control problem, we just modify the definition of [δ] ϕ λ with:

[δ] ϕ λ def = [δ] ([reset] ff ∧ ϕ λ ) ∨ ac∈Actc ϕ ac
which is equivalent to [δ] ϕ . Indeed the formula [reset] ff holds precisely when no controllable action can be perfomed by the controller; and when reset tt holds, a controllable move has to be performed.

4 The Timed Modal Logic L cont ν

In this section we focus on the logic L cont ν and prove several properties of this logic, namely its expressive power, its decidability and compositionality.

L cont ν is more expressive than L ν . The modality "[δ " has been introduced for expressing control properties of open systems. We now prove that this operator adds expressive power to L ν , i.e. it can not be expressed with L ν . As usual we say that two formulae ϕ and ψ are equivalent for a class of systems S (we then write ϕ ≡ S ψ) if for all s ∈ S, s |= ϕ iff s |= ψ. A logic L is said to be as expressive as L ′ over S (denoted L S L ′ ) if for every ϕ ∈ L ′ , there exists ψ ∈ L s.t. ϕ ≡ S ψ. And L is said to be strictly more expressive than L ′ if L S L ′ and L ′ S L. We have the following result:

Theorem 2. The logic L cont ν is strictly more expressive than L ν over timed automata.

The full proof is long and technical, we give it in [BCL05]. Here we just give the techniques which we have used. Let ϕ be the

L cont ν formula ([a] ff) [δ ( b tt)
stating that no a-transition can be performed as long as (via delay transitions) no b has been enabled. The core of the proof is based on the fact that there is no L ν formula equivalent to ϕ. The difficult point is that it is not possible to find two TAs A and A ′ such that A |= ϕ, A ′ |= ϕ and A |= ψ ⇔ A ′ |= ψ for any ψ ∈ L ν . Indeed L ν allows us to build a characteristic formula for a TA [LLW95] (i.e. a formula which describes the behaviour of A w.r.t. strong timed bisimulation) and clearly the two TAs A and A ′ wouldn't be bisimilar. This is a classical problem in temporal logic [Eme91] where one shows that two temporal logics may have different expressive power even if they have the same distinguishing power. This makes the proof more difficult. Such expressiveness problems are not much considered in the timed framework. Up to our knowledge this is one of the first proofs of that type for timed logics. To prove the result, we build two families of TAs (A i ) i≥1 and (A ′ i ) i≥1 such that for every integer i, A i |= ϕ whereas A ′ i |= ϕ. We then prove that if ϕ can be expressed equivalently as formula Φ ∈ L ν (over timed automata), then there must exist some integer i ≥ 1 such that A ′ i |= Φ, which will be a contradiction. The behaviours of automata A i and A ′ i can be represented by (and infered from) the following picture. Proof (Sketch). The EXPTIME-hardness comes from the EXPTIME-hardness of the model-checking of L ν . For the EXPTIME-easyness, we just have to explain how to handle the [δ modality. Let A be a TA and Φ ∈ L cont ν . We consider the region graph [AD94] R A associated with A and the set of formula clocks K.

Clearly the classical notion of region can be used for [δ : two states in a region r satisfy the same L cont ν formulae (the semantics of [δ can be defined in term of regions as well). Then we can define procedures to label R A states with the Φ subformulae they satisfy. We can use the same algorithms as for L ν to label [δ]ϕ, δ ϕ, a ϕ, . . . and define a new procedure for the ϕ [δ ψ subformulae. This can be done easily (as soon as ϕ and ψ have already been labeled) and it consists in a classical "Until" over the delay transitions (see below a way of computing ϕ [δ ψ with DBMs). The complexity of the algorithm will remain linear in the size of R A and Φ, and finally exponential in the size of A and Φ [AL02].

⊓ ⊔

Instead of considering region techniques, classical algorithms for timed modelchecking use zones (i.e. convex sets of valuations, defined as conjunctions of xy ⊲⊳ c constraints and implemented with DBMs [Dil90,Bou04]). This makes verification more efficient in practice. In this approach ϕ is defined as sets of pairs (q, z) where z is a zone and q is a control state of the TA. This approach is also possible for L cont ν . Indeed we can define ϕ[δ ψ when ϕ and ψ are already defined as sets of symbolic configurations (q, z). We use standard operations on zones: ←z (resp. -→ z , z c ) denotes the past (resp. future, complement) of z, and z + represents the set z ∪ {v | ∃t > 0 s.t. vt ∈ z and ∀0 ≤ t ′ < t, vt ′ ∈ z} (if z is represented by a DBM in normal form, z + is computed by relaxing constraints x < c to x ≤ c). It is then easy to prove that:

ϕ [δ ψ = ← -- ϕ c c ∪ ← --------- -→ ψ ∪ ϕ c c ∩ ψ ∪ ϕ ∩ ← ------- ϕ + ∩ ψ L cont ν is compositional. An important property of L ν is that it is composi- tional [LL95,LL98
] for timed automata. This is also the case for L cont ν . A logic L is said to be compositional for a class S of models if, given an instance

(s 1 | • • • |s n ) |= ϕ with s i ∈ S and ϕ ∈ L, it is possible to build a formula ϕ/s 1 (called a quotient formula) s.t. (s 1 | • • • |s n ) |= ϕ ⇔ (s 2 | • • • |s n ) |= ϕ/s 1 .
This can be viewed as an encoding of the behaviour of s 1 into the formula. Of course this also depends on the synchronization function, but we will not enter into the details here. For ϕ ∈ L ν , A a TA, it is possible to define inductively a quotient formula ϕ/A (we refer to [LL98] for a complete description of this technique). In order to prove that L cont ν is compositional it is sufficient to define the quotient formula for the new modality ϕ [δ ψ. We define the quotient of ϕ 1 [δ ϕ 2 for a location ℓ of a TA A in the following way:

ϕ 1 [δ ϕ 2 /ℓ def = inv(ℓ) ⇒ (ϕ 1 /ℓ) [δ inv(ℓ) ∧ (ϕ 2 /ℓ)
With such a quotient construction we get the following proposition:

Proposition 1. The logic L cont ν is compositional for the class of timed automata.

We have discussed a little bit in previous sections why the property is very useful and important. In particular, the new modality of L cont ν has been added to the model-checker CMC [LL98] which implements a compositional model-checking algorithm: it first computes a quotient formula of the system and the property and then check for the satisfiability of the formula. We have added to CMC the quotient rule for the operator [δ and thus we can use CMC for checking controllability properties. We do not provide here our experimental results but better refer to the web page of the tool: http://www.lsv.ens-cachan.fr/~fl/cmcweb.html.

Conclusion

In this paper we have used the logic L ν to specify control objectives on timed plants. We have proved that a deterministic fragment of L ν allows us to reduce control problems to a model-checking problem for an extension of L ν (denoted L cont ν ) with a new modality. We have also studied the properties of the extended logic L cont ν and proved that i) L cont ν is strictly more expressive than L ν ; ii) the model-checking of L cont ν over timed automata is EXPTIME-complete; iii) L cont ν inherits the compositionality property of L ν .

Our current and future work is many-fold:

-extend our work to the synthesis of controllers. Note that this problem is strongly related to the satisfiability problem for

L ν which is still open [LLW95].
-use the features of the logic L ν to express more general types of control objectives e.g. to take into account dynamic changes of the set of controllable events as in [AVW03].

A Proof of Theorem 1

Before proving Theorem 1 we need to take some notations.

Let G = (Q, q 0 , Act, -→) be a TTS. For s ∈ Q and ∆ ∈ Q ≥0 we define:

-G s ∆ to be the sub TTS of G rooted at s such that two consecutive controllable actions (in Act c ) are separated by a time amount t s.t. t ≥ ∆; -G ∆ stands for G q0 ∆ ; -for τ ≤ ∆, G s ∆,τ is the sub TTS of G s ∆ where no controllable action occurs before τ time units from the root s; -Contr(G s ∆,τ , s) is the set of controllers for TTS G s ∆,τ from state s; Contr(G q0 ∆,0 , q 0 ) thus denotes the set of controllers that can let at least ∆ time units between two consecutive controllable actions.

If G is the semantics of a plant P = (L, ℓ 0 , Act, X, inv, T ) the TTS G q0 ∆ can be effectively constructed using a parallel composition with a self-loop automaton (with a fresh clock x) enforcing a delay greater than ∆ (e.g. by x ≥ ∆) between two controllable actions. We denote P ∆ this synchronized product.

Theorem 1 is a consequence of the following lemma: Lemma 1. For any σ ∈ Act c ∪ {λ}, any state s ∈ G and any L det ν formula Φ, we have:

∃f ∈ Contr(G s ∆,τ , s) s.t. f (G, s), (s, v) |= Φ ∧ σ tt ⇔ G s ∆,τ , (s, v) |= Φ σ
Note how this lemma interprets for formulae Φ :

∃f ∈ Contr(G s ∆,τ , s) s.t. f (G, s), (s, v) |= Φ ⇔ G s ∆,τ , (s, v) |= Φ
Proof. First we assume that the result holds for the fixpoint variables and we show the Lemma by structural induction over L det ν formulae. The cases

Φ def = x ∼ c or Φ def = r in ϕ are obvious.
-

Φ def = [a u ] ϕ: ⇒ Assume there exists f ∈ Contr(G s ∆,τ , s) s.t. f (G, s), (s, v) |= [a u ] ϕ ∧ σ tt. Then for any f (G, s) : s au ---→ s ′ , we have f (G, s), (s ′ , v) |= ϕ. Then there exists f ′ ∈ Contr(G s ∆,τ , s ′ ) s.t. f ′ (G, s ′ ), (s ′ , v) |= ϕ and the induction hypothesis provides: G s ′ ∆,τ , (s ′ , v) |= ϕ .
Since the strategies cannot block the uncontrollable actions, any action a u ∈ Act u that can be performed from (s, v) in G s ∆,τ , can also be performed in f (G, s) and then

G s ∆,τ , (s, v) |= [a u ]ϕ . Moreover f (G, s), (s, v) |= σ tt which implies that G s ∆,τ , (s, v) |= σ tt, and thus G s ∆,τ , (s, v) |= [a u ] ϕ σ . ⇐ Assume G s ∆,τ , (s, v) |= [a u ] ϕ ∧ σ tt. For any transition G s ∆,τ , s au ---→ s ′ , we have G s ∆,τ , (s ′ , v) |= ϕ . By i.h. we know that there exists f au ∈ Contr(G s ∆,τ , s ′ ) s.t. f au (G, s ′ ), (s ′ , v) |= ϕ. Let f be the strategy defined by: f (s au ---→ ρ) def = f au (ρ) for any ρ starting in state s ′ and f (s) = a c if σ = a c (note that in that case, it is possible to do a σ because G s ∆,τ , (s, v) |= σ tt), or f (s) = λ otherwise. -Φ def = a u ϕ: ⇒ Assume there exists f ∈ Contr(G s ∆,τ , s) s.t. f (G, s), (s, v) |= a u ϕ∧ σ tt. Then there exists f (G, s) : s au ---→ s ′ with f (G, s), (s ′ , v) |= ϕ. There- fore there is f ′ ∈ Contr(G s ∆,τ , s ′ ) s.t. f ′ (G, s ′ ), (s ′ , v) |= ϕ and the i.h. entails: G s ′ ∆,τ , (s ′ , v) |= ϕ . G s ∆,τ contains the behaviours of f (G, s), then G s ∆,τ , (s, v) |= a u ϕ . Moreover, f (G, s), (s, v) |= σ tt, thus G s ∆,τ , (s, v) |= a u ϕ ∧ σ tt, and thus G s ∆,τ , (s, v) |= a u ϕ σ . ⇐ Assume G s ∆,τ , (s, v) |= a u ϕ ∧ σ tt. There is a transition G s ∆,τ , s au ---→ s ′ s.t. G s ∆,τ , (s ′ , v) |= ϕ . By i.h. we know that there exists f au ∈ Contr(G s ∆,τ , s ′ ) s.t. f au (G, s ′ ), (s ′ , v) |= ϕ. Let f be the strategy defined by: f (s au ---→ ρ) def = f au (ρ) for any ρ starting in state s ′ and f (s) = a c if σ = a c , or f (s) = λ otherwise. -Φ def = a c ϕ: ⇒ There exists f ∈ Contr(G s ∆,τ , s) s.t. f (G, s), (s, v) |= a c ϕ ∧ σ tt.
Then clearly σ is a c : otherwise this would entail that f is not deterministic and requires two different controllable actions from the state (s, v). There exists f (G, s) :

s ac ---→ s ′ such that f (G, s ′ ), (s ′ , v) |= ϕ. Moreover defining f ′ ∈ Contr(G s ∆,∆ , s ′ ) by f ′ (ρ) def = f (s ac ---→ ρ) for any ρ starting in s ′ , we get that f ′ (G, s ′ ), (s ′ , v) |= ϕ. By i.h. we have G s ′ ∆,∆ , (s ′ , v) |= ϕ . G s ∆,τ contains the behaviours of f (G, s), then G s ∆,τ , (s, v) |= a c ϕ and thus G s ∆,τ , (s, v) |= a c ϕ σ . ⇐ The only possible case is σ = a c and G s ∆,τ , (s, v) |= a c ϕ . There is a transition G s ∆,τ , s ac ---→ s ′ s.t. G s ′ ∆,∆ , (s ′ , v) |= ϕ . By i.h. we know that there exists f ′ ∈ Contr(G s ∆,∆ , s ′ ) s.t. f ′ (G, s ′ ), (s ′ , v) |= ϕ.
Let f be the strategy defined by: f (s ac ---→ ρ) def = f ′ (ρ) for any ρ run starting in s ′ and f (s) = a c . f is a ∆-strategy and belongs to Contr(G s ∆,τ , s) -note that in this case τ = 0 -, and f (G, s), (s, v) |= a c ϕ and then a c tt also holds for f (G, s), (s, v).

-

Φ def = [a c ] ϕ: ⇒ If a c = σ the result is obvious. Now assume a c = σ, then there exists f ∈ Contr(G s ∆,τ , s) s.t. f (G, s), (s, v) |= [a c ] ϕ ∧ a c tt.
The same proof as above (for

Φ def = a c ϕ) gives G s ∆,τ , (s, v) |= a c ϕ , i.e. G s ∆,τ , (s, v) |= [a c ] ϕ σ . ⇐ First assume σ ∈ Act c \{a c } or σ = λ. Then G s ∆,τ , (s, v) |= σ tt we define the strategy f to be f (s) = σ. This allows us to have f (G, s), (s, v) |= [a c ]ϕ∧ σ tt (as a c is disabled by f ). Finally assume σ = a c . Then we have G s ∆,τ , (s, v) |= a c ϕ . There exists G s ∆,τ , s ac ---→ s ′ s.t. G s ′ ∆,∆ , (s ′ , v) |= ϕ . By i.h. there exists f ∈ Contr(G s ∆,∆ , s ′ ) s.t. f ′ (G, s ′ ), (s ′ , v) |= ϕ. Let f be the strategy defined by f (s) = a c and f (s ac ---→ ρ) = f ′ (ρ) for any ρ run starting in state s ′ . We have f ∈ Contr(G s ∆,τ , s) and f (G, s), (s, v) |= [a c ] ϕ ∧ σ tt. -Φ def = δ ϕ: ⇒ First assume σ = λ. If there exists f ∈ Contr(G s ∆,τ , s) s.t. f (G, s), (s, v) |= δ ϕ, then there is f (G, s), s t --→ s t (with t ∈ R) s.t. f (G, s), (s t , v + t) |= ϕ. By i.h. we have G s ′
∆,τ -t , (s ′ , v + t) |= ϕ where τt stands for max(τt, 0). And then G s ∆,τ , (s, v) |= δ ϕ because G s ∆,τ is more general than f (G, s). Now assume σ = a c . There exists f ∈ Contr(G s ∆,τ , s) s.t. f (G, s), (s, v) |= δ ϕ ∧ a c tt. This means that f (s) = a c and then no delay is allowed by the strategy and then it is equivalent to f (G, s), (s, v) |= ϕ ∧ a c tt. By i.h. we have: * There exists some delay transition in G s ∆,τ from s that does not belong to f (G, s). This means that the strategy f requires the execution of some controllable action a c from some state s t reachable from s by a delay t: f (s t --→ s t ) = a c . We then have f (G, s), (s t ′ , v + t ′ ) |= ϕ for any t ′ < t and f (G, s), (s t , v + t) |= ϕ ∧ a c tt. By i.h. we have

G s ∆,τ , (s, v) |= ϕ ac . ⇐ Assume σ = λ. If G s ∆,τ , (s, v) |= δ ϕ ,
G s t ′ ∆,τ -t ′ , (s t ′ , v + t ′ ) |= ϕ λ for any t ′ < t and G s ∆,0 , (s t , v + t) |= ϕ ac . This implies G s ∆,τ , (s, v) |= ϕ λ [δ ϕ ac . ⇐ Assume σ ∈ Act c . Then G s ∆,τ , (s, v) |= ϕ σ entails that there exists some f ∈ Contr(G s ∆,τ , s) s.t. f (G, s), (s, v) |= ϕ ∧ σ tt.
This means that f (s) = σ and that no delay is indeed allowed by the strategy f . Then we clearly have f (G, s), (s, v)

f t ′ ∈ Contr(G s ∆,τ -t , s t ′ ) s.t. f t ′ (G, s t ′ ), (s t ′ , v + t ′ ) |= ϕ and f t ′ (s t ′ ) = λ.
Let f be the strategy defined by: f (s

t ′ --→ s t ′ ) = λ for any t ′ < t, f (s t --→ s t ) = a c and f (s t ′′ --→ ρs t ′′ ) = f t ′′ (ρ) for t ′′ ≤ t. This strategy allows us to deduce f (G, s), (s, v) |= [δ] ϕ. -Φ def = i ϕ i : Direct. -Φ def = i ϕ i : ⇒ Assume there exists f ∈ Contr(G s ∆,τ , s) s.t. f (G, s), (s, v) |= i α i ∧ σ tt. Then we have f (G, s), (s, v) |= α i ∧ σ tt
f i ∈ Contr(G s ∆,τ , s) s.t. f i (G, s), (s, v) |= α i ∧ σ tt.
It remains to construct a strategy f by collecting the strategies f i 's. This is possible because ϕ belongs to L det ν , indeed any term α i is prefixed by a modality with a different label of Act ∪ {δ} and then the union of the strategies f i 's provides a strategy f that belongs to Contr(G s ∆,τ , s). This gives the result.

Then this entails that the Lemma holds for any L det ν formula without fixedpoint. But this clearly entails that it also holds for full L det ν . Indeed consider two states s and s ′ which satisfy the same formulae without fixedpoint. If s does not belong to the greatest fixedpoint of a an equation Z def = Ψ Z , then it entails that this state does not satisfy some unfolding of the formula Ψ Z (with where the first occurrences of Z have been replaced by tt), then this formula does not hold for the state s ′ .

⊓ ⊔

B Proof of Theorem 2

Let us define ϕ = ([a] ff) [δ ( b tt). We assume that we can express ϕ over timed automata as a formula Φ of L ν . This means that for every timed automaton A, A |= ϕ ⇐⇒ A |= Φ.

The two families of models. For each i ≥ 1, we define two timed automata as follows:

A i ℓ i ℓ x ≥ 1 2 2i , a 1 j=i 1 2 2j ≤ x < 1 2 2j-1 , b A ′ i ℓ ′ i ℓ x ≥ 1 2 2i+1 , a 1 j=i 1 2 2j ≤ x < 1 2 2j-1 , b
The behaviors of automata A i and A ′ i can be represented by (and infered from) the following picture.

A 1 a b A ′ 1 a b A 2 a b b A ′ 2 a b b . . .
It is easy to verify that for each i,

A i |= ϕ for each i ≥ 0 A ′ i |= ϕ for each i ≥ 0
Eliminating constants from formula Φ (-→ Φ 1 ). Time in all A i 's and A ′ i 's is bounded by 1. Let m be an integer greater than the granularity of the constants appearing in Φ. As ϕ is an untimed formula, we get the following lemma: We can assume that Φ has only constants greater than 1 (or equal to 0). Lemma 3. Under the previous assumption, we have that for every 1-bounded

timed automaton A, A |= Φ ⇐⇒ A |= Φ[x ⊲⊳ c ← truth(1 ⊲⊳ c) when c > 0].
The new formula is denoted Φ 1 and is a priori not equivalent to Φ over all timed automata, but at least over 1-bounded timed automata, and in particular over all automata A i 's and A ′ i 's, which is sufficient for what we want to prove. Note that the formula Φ 1 can be generated by the following grammar:

ϕ ::= p | tt | ff | ϕ ∧ ϕ | ϕ ∨ ϕ | x in ϕ | x ⊲⊳ 0 | [a] ϕ | a ϕ | [δ] ϕ | δ ϕ | X (3)
Eliminating clock subformulas. The only "clock" information in the formula Φ 1 are formulas of the form "x ∼ 0" and "x in •". We want to get rid off this information. For each C ⊆ X, we define inductively new formulas {ϕ} (C) as follows:

{α} (C) = α if α ∈ {p, t t, f f} {ϕ1 op ϕ2} (C) = {ϕ1} (C) op {ϕ2} (C) if op ∈ {∧, ∨} {x in ϕ} (C) = x in {ϕ} (C∪{x}) {[a]ϕ} (C) = [a]{ϕ} (C) { a ϕ} (C) = a {ϕ} (C) {X} (C) = XC {x > 0} (C) =  t t if x ∈ C f f if x ∈ C {x = 0} (C) =  t t if x ∈ C f f if x ∈ C {[δ] ϕ} (C) = {ϕ} (C) ∧ [δ] + {ϕ} (∅) { δ ϕ} (C) = {ϕ} (C) ∧ δ + {ϕ} (∅)
Intuitively the formula {ϕ} (C) expresses the fact that ϕ holds while the value of clocks in C is 0 and the value of clocks not in C are strictly greater than 0. The formula δ + ϕ is similar to that of δ ϕ but the delay must be positive. Similarly [δ] + ϕ means that for all positive delay, ϕ must hold. We do not redefine formally these two operators.

Lemma 4. For each timed automaton A, for each formula ϕ generated by the grammar (3), for each extended configuration (ℓ, u :: v), (ℓ, u :: v) |= ϕ ⇐⇒ (ℓ, u :: v) |= {ϕ} (C) where C = {x ∈ X | v(x) = 0}. In particular, in the initial configuration (u 0 = 0 and v 0 = 0),

(ℓ 0 , u 0 :: v 0 ) |= ϕ ⇐⇒ (ℓ 0 , u 0 :: v 0 ) |= {ϕ} (X)
The new formula {Φ 1 } (X) has no more clock constraints. We can thus erase all operators "x in •" because clocks are no more used. We get a new formula Φ 2 (without clocks) which is generated by the grammar

ϕ ::= p | tt | ff | ϕ ∧ ϕ | ϕ ∨ ϕ | [a] ϕ | a ϕ | [δ] + ϕ | δ + ϕ | X (4)
and thus such that for every 1-bounded timed automata A, for every configuration (ℓ, u) of A, (ℓ, u) |= ϕ ⇐⇒ (ℓ, u) |= Φ 2 (Φ 2 is equivalent to ϕ over 1-bounded timed automata).

Region abstraction. The regions for automaton A i in state ℓ i are the intervals:

0, 1 2 2i , 1 2 2i , 1 2 2i-1 , . . . , 1 2
, 1 whereas the regions for automaton A ′ i in state ℓ ′ i are the intervals:

0, 1 2 2i+1 , 1 2 2i+1 , 1 2 2i , . . . , 1 2 , 1
For all automata, only one region is needed in state ℓ, it is the interval [0, 1[. It is thus only necessary to see what happens in states ℓ i and ℓ ′ i . All regions are right-open. We denote by R i the region automaton for A i and R ′ i the region automaton for A ′ i . We can redraw automata R i and R ′ i (restricted to states ℓ i and ℓ ′ i ) as follows:

R i in ℓ i • × . . . • × ρ i r 2i r 2i-1 r 2 r 1 R ′ i in ℓ ′ i × • × . . . • × ρ ′ i r 2i+1 r 2i r 2i-1 r 2 r 1
We have that r k = 1 2 k , 1 2 k-1 , that ρ k = 0, 1 2 2k and ρ ′ k = 0, 1 2 2k+1 . Two states which have the same label (for example r i ) satisfy exactly the same formulas of (4) because they are obtained similarly by a backward computation. The labelling "•" means that both a and b can be done (leading to state ℓ) whereas the labelling "×" means that only action a can be done (also leading to state ℓ). Finally no labelling means that no action can be done.

Lemma 5. Let us fix some formula ψ generated by grammar (4).

-Let us fix some region r i and two valuations u and v in r i . Then for every j such that 2j ≥ i and for every k such that 2k + 1 ≥ 1,

(ℓ j , u) |= ψ ⇔ (ℓ j , v) |= ψ ⇐⇒ (ℓ ′ k , u) |= ψ ⇐⇒ (ℓ ′ k , v
ϕ ::= p | tt | ff | [a] ff | a tt | ϕ ∧ ϕ | ϕ ∨ ϕ | [δ] + ϕ | δ + ϕ | X (5)
For each u ∈ [0, 1[, (ℓ i , u) |= ϕ ⇐⇒ (ℓ i , u) |= Φ 4 and (ℓ ′ i , u) |= ϕ ⇐⇒ (ℓ ′ i , u) |= Φ 4 . We could say that Φ 4 is equivalent to ϕ over all automata A i 's and A ′ i 's.

Untiming the formula. We note R i (resp. R ′ i ) the set of regions in state ℓ i (resp. ℓ ′ i ) for the automaton A i (resp. A ′ i ). We define a new logic by the grammar:

ϕ ::= tt | ff | [a] ff | a tt | ϕ ∧ ϕ | ϕ ∨ ϕ | G + ϕ | F + ϕ | X (6)

.

  Model-checking of L ν over TAs is an EXPTIME-complete problem [AL02]. Adding the modality [δ does not change this result, we have: Theorem 3. The model-checking of L cont ν over timed automata is EXPTIMEcomplete.

Lemma 2 .

 2 For every positive (> 0) rational p, for every timed automaton A, A |= ϕ iff A |= Φ iff A |= Φ[c ← c.p] where Φ[c ← c.p] is the formula Φ where each constant c is replaced by the product c.p.

  , (s t , v + t) |= ϕ . By i.h. we deduce that there existsf t ∈ Contr(G s ∆,τ -t , s t ) s.t. f t (G, s t ), (s t , v + t) |= ϕ. Let f ∈ Assume σ ∈ Act c . If G s ∆,τ , (s, v) |= ϕ σ , we have by i.h. that there exists f ∈ Contr(G s ∆,τ , s) s.t. f (G, s), (s, v) |= ϕ ∧ σ tt. Then we clearly have f (G, s), (s, v) |= δ ϕ ∧ σ tt. First assume σ ∈ Act c . Assume there exists f ∈ Contr(G s ∆,τ , s) s.t. f (G, s), (s, v) |= [δ] ϕ ∧ σ tt. This implies f (G, s), (s, v) |= ϕ ∧ σ tt. By i.h. we have: G s ∆,τ , (s, v) |= ϕ σ . Assume σ = λ. Then there exists f ∈ Contr(G s ∆,τ , s) s.t. f (G, s), (s, v) |= [δ] ϕ, that is for any transition f (G, s), s t --→ s t (with t ∈ R), we have f (G, s), (s t , v + t) |= ϕ.We distinguish two cases:* Every delay transition from G s ∆,τ , s exists also in f (G, s), s. Then the induction hypothesis entails that for any t, we have 5 G s ∆,τ -t (s t , v + t) |= ϕ ε and then clearly G s ∆,τ , (s, v) |= [δ]ϕ ε and then G s ∆,τ , (s, v) |= ϕ ε [δ ϕ ac for every a c ∈ Act c .

	-Φ ⇒ def = [δ] ϕ:
		then there exists G s ∆,τ : s	t --→ s t
	with t ∈ R s.t. G s ∆,τ Contr(G s ∆,τ , s) be the strategy defined as f (s	t ′ --→ s t ′ ) = λ for any
	t ′ < t, and f (s	t --→ ρ) = f t (ρ) for any run ρ starting in state s t . Clearly
	we have f (G, s), (s, v) |= δ ϕ.

  |= [δ] ϕ ∧ σ tt. Assume σ = λ and G s ∆,τ , (s, v) |= ϕ λ [δ ϕ ac for some a c ∈ Act c . , (s t , v + t) |= ϕ λ and then by i.h. there exists f t ∈ Contr(G s ∆,τ -t , s t ) s.t. f t (G, s t ), (s t , v + t) |= ϕ and f t (s t ) = λ. Let f be the strategy defined by f (s = f t (ρ) for any run ρ starting in state s t . Clearly f belongs to Contr(G s ∆,τ , s). And we have f (G, s), (s, v) |= [δ] ϕ. * There exists t ∈ R s.t. G s ∆,τ : s t --→ s t and G s ∆,τ -t , (s t , v + t) |= ϕ ac for some a c ∈ Act c . By i.h. there exists f t ∈ Contr(G s ∆,τ -t , s t ) s.t. f t (G, s t ), (s t , v + t) |= ϕ ∧ a c tt. Clearly f t (s) = a c and f t forbids time elapsing from s t . Moreover the i.h. applied to states s t ′ with t ′ < t gives that there exists

		We
	distinguish two cases: * G s ∆,τ , (s, v) |= [δ] ϕ λ . Then for any t ∈ R, we have that G s ∆,τ : s	t --→
	s t implies G s ∆,τ t --→ s t ) = λ and f (s

t --→ ρ)

  for any i. By h.i. we have G s ∆,τ , (s, v) |= α i σ for any i, and thenG s ∆,τ , (s, v) |= i α i σ . ⇐ Assume G s ∆,τ , (s, v) |= i ϕ σ .Then by i.h. we have that there exists some

  ) |= ψ -Moreover, for all valuations u and v in ρ i , (ℓ i , u) |= ψ ⇐⇒ (ℓ i , v) |= ψ -Finally, for all valuations u and v in ρ′ i , (ℓ ′ i , u) |= ψ ⇐⇒ (ℓ ′ i , v) |= ψThe logic (4) can thus be interpreted over regions: if ψ is generated by (4), and (ℓ, r) is a "region state", then (ℓ, r) |= ψ def ⇐⇒ ∃u ∈ r s.t. (ℓ, u) |= ψ. And the following equivalence holds: (ℓ, r) |= ψ def ⇐⇒ ∀u ∈ r s.t. (ℓ, u) |= ψ. Atomic propositions. As already noticed above, formulas [e] ϕ, e ϕ (with e being either a or b) can be viewed as atomic formulas (which justifies notations "•" and "×"). Let us fix a subformula [a] ψ. Evaluate ψ in state ℓ. As there is only one region in ℓ, it holds thatψ ∩ {(ℓ, u) | u ∈ [0, 1[} = {(ℓ, u) | u ∈ [0, 1[} or ∅ First note that for each valuation u ∈ [0, 1[, (ℓ, u) |= [a] ψbecause no a can be done, and similarly (ℓ, u) |= [a] ff, and (ℓ, u) |= tt. Considering the first case, it is easy to prove that for each valuation u ∈ [0, 1[, (ℓ i , u) |= [a] ψ, in which case, we can replace the subformula [a] ψ by tt. In the second case, for each u ∈ [0, 1[, we have that (ℓ First note that for each valuation u ∈ [0, 1[, (ℓ, u) |= a ψ because no a can be done. Considering the second case, it is easy to prove that for each valuation u ∈ [0, 1[, (ℓ i , u) |= a ψ, in which case, we can replace the subformula a ψ by ff. In the first case, for each u ∈ [0, 1[, we have that (ℓ i , u) |= a ψ ⇐⇒ (ℓ i , u) |= a tt, in which case we can replace the subformula a ψ by a tt. With all these remarks we define a new formula Φ 4 from Φ 3 by rewriting a subformula [a] ψ into [a] ff if ψ does not hold in ℓ and into tt if ψ holds in ℓ, and by rewriting a subformula a ψ by ff if ψ does not hold in ℓ and by a tt if ψ holds in ℓ. The new formula Φ 4 can be generated by the grammar:

i , u) |= [a] ψ ⇐⇒ (ℓ i , u) |= [a] ff, in which case we can replace the subformula [a] ψ by [a] ff.

Let us fix a subformula a ψ. Evaluate ψ in state ℓ. As there is only one region in ℓ, it holds that

ψ ∩ {(ℓ, u) | u ∈ [0, 1[} = {(ℓ, u) | u ∈ [0, 1[} or ∅

We often write ℓ g,a,Y -----→ ℓ ′ instead of simply the tuple (ℓ, g, a, Y, ℓ ′ ).

In the following we always assume that τt stands for max(0, τt).

This logic is interpreted on the region automata R i 's and R ′ i 's. The semantics (denoted ⊢) is defined inductively by:

Operators [δ] + ψ and G + ψ interpreted over regions are not so different: the only difference stands in that the current region may not satisfy property ψ. In the same way, operators δ + ψ and F + ψ interpreted over regions are not so different: the only difference stands in that a region different from the current one has to satisfy ψ.

We rewrite the formula Φ 4 into Φ 5 by replacing each subformula [δ] + ψ by ψ∧G + ψ and each subformula δ + ψ by ψ ∨ F + ψ. It is then easy to prove the following lemma:

The formula Φ 5 is now an (fully) untimed formula. Moreover, Φ 5 is equivalent to ϕ over the two families of automata (A i ) i≥1 and (A ′ i ) i≥1 . We finally note Ψ = Φ 5 .

Gluing everything. The formula Ψ can be written in normal form as a system of equations (X i = f i (X 1 , ..., X n )) 1≤i≤n and Ψ = X 1 . We assume that each formula f i (X 1 , ..., X n ) is a boolean combination of subformulas α j i (which can be either some formula F + β j i , or G + β j i , or some atomic-like formula a tt, [a] ff, tt or ff, or some fix-point variable X j i ):

Without loss of generality we assume that no subformula α j i is a fix-point variable X k . The following lemma justifies this fact: Lemma 7. We assume that α j i = X k (with i = k). Then the new formula obtained by replacing X k by its definition formula is equivalent to the previous formula. If α j i = X i , then the new formula obtained by replacing this variable X i by tt is equivalent to the initial formula. Thus, each α j i is either an atomic proposition, or its negation, or a formula F + ϕ or a formula Gϕ.

Lemma 8. The following implications are true.

There is a sequence (γ j ) 1≤j≤k1 ∈ {tt, ff} k1 and an infinite sequence of indexes I such that b 1 (α 1 1 ← γ 1 , ..., α k1 1 ← γ ℓ1 ) is true and for each i ∈ I, for each 1

From the first line of implications of Lemma 8, for every i ∈ I, R ′ i |= α F ∧ α ¬G . We can even simplify: let's take some i 0 ∈ I, we have that for every i ≥ i 0 , R ′ i |= α F ∧ α ¬G . From the second line of implications, for every i ∈ I such that i > i 0 , we have that R ′ i-1 |= α G ∧ α ¬F . Finally we can find some i such that R ′ i |= α F ∧ α ¬G ∧ α G ∧ α ¬F and thus R ′ i |= Ψ (because for all possible simple terms, there is no problem).

⊓ ⊔


Juan Guillermo

Santos Macías

Chola Elangeswaran

Lv Zhao

Brecht Van Hooreweder

Jérôme Adrien

Éric Maire

Jean-Yves Buffiere

Wolfgang Ludwig

Pascal J Jacques

Aude Simar

Juan Guillermo Santos Macías

Eric Maire

Jean-Yves Buffière

Ductilisation and fatigue life enhancement of selective laser melted AlSi10Mg by friction stir processing

Keywords:

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Additive manufacturing (AM) has opened many opportunities for structural design and optimisation in several sectors, including aerospace, automotive and medical applications. AM offers more design opportunities, flexibility and material saving features [1]. Despite these potential advantages, there are also limitations related to the nature or the novelty of the technology, such as microstructural inhomogeneity and the presence of porosity. These specific shortcomings restrain the use of metal AM in structural components. In particular, the severe requirements imposed by the aerospace industry, notably in terms of damage and fatigue resistance, are not yet met satisfactorily immediately after the AM process. These poor performances are reported to be mainly due to microstructural inhomogeneity and excessive porosity [2].

In order to tackle these issues, several approaches are possible, such as new alloy development or optimisation of manufacturing parameters. Post-treatments also play an important role and are often necessary to reach the required mechanical performances. They range from heat treatments to reduce residual stress [START_REF]EOS GmbH -electro optical systems, Material data sheet for EOS Aluminium AlSi10Mg[END_REF] or to homogenise the microstructure [START_REF] Brandl | [END_REF], to surface finishing techniques to decrease roughness and thus to enhance fatigue resistance [2].

Other processing stages can be seen as particularly suitable solutions. One of them is hot isostatic pressing (HIP), which combines high pressure and elevated temperature to efficiently reduce porosity. The HIP process is now successfully implemented in the manufacturing strategy of AM Ti6Al4V parts [5]. Nevertheless, the use of the HIP technique also presents strong limitations. The relatively long time spent at high temperature during the HIP process ultimately coarsens the AM microstructure, leading to poor strength. Furthermore, the application of a HIP stage does not seem to bring any beneficial influence on AM AlSi10Mg parts [6][7][8][9][10], motivating the quest for new post-treatments.

The present work shows that friction stir processing (FSP) can be used for improving the mechanical behaviour of AM parts, particularly in the case of AlSi10Mg alloy processed by selective laser melting (SLM). FSP is derived from friction stir welding [11]. Using a rotating non-consumable cylindrical tool composed of a shoulder with a pin at the tip that penetrates through the material, a local thermomechanical treatment is applied, bringing microstructural changes such as particle breakdown and redistribution, homogenisation or refinement [11]. FSP can be applied locally in regions of stress concentration of critical parts.

FSP has been shown as a very effective way of improving mechanical behaviour in several materials, including cast [12][13][14][15] and wrought [16] Al alloys and Ti alloys [17]. For instance, huge improvement of ductility (i.e. increase of the elongation at failure from 0.01 before FSP to 0.15 after FSP) together with a fivefold increase of fatigue life have been reported after performing FSP on an F357 cast alloy (a hypoeutectic Al-Si alloy), while maintaining the yield strength and enhancing the ultimate tensile strength by 10% [14]. Hannard et al. [16] demonstrated the ductility enhancement brought about by FSP thanks to its ability to break down and redistribute Fe-rich intermetallic particles. However, its use on AM parts has only been reported by Ref. [18,19] for AlSi10Mg, where the authors essentially studied the influence of FSP on several microstructural features, observing promising microstructural homogenisation, and by Huang et al. [20] for Ti6Al4V, in which ductility was increased due to the elimination of the brittle phase by FSP. The nature of FSP, characterised by a short heat exposure time, avoiding microstructure coarsening, is thus expected to improve mechanical performances of SLM AlSi10Mg. SLM AlSi10Mg 150x35x5 mm plates were manufactured using an EOS M290 set-up with standard optimised parameters (Laser power = 390 W; layer thickness = 30 µm; hatch spacing = 0.19 mm; scanning speed = 1300 mm/s; scan rotation = 67°). Plates were manufactured with a build platform temperature of 35 °C. It is worth mentioning that using a higher build platform temperature during the SLM process decreases residual stresses, which can be problematic during the manufacturing process (causing part deformation and manufacturing interruption), but using higher temperature also leads to lower post-manufacturing strength. Therefore, to mimise the effect of residual stress, a stress relief heat treatment (SRHT) at 300 °C for 2 h, was performed under Ar atmosphere on some samples after the AM process. These SRHT samples were used for comparison purposes. To study the effect of FSP post-treatment on SLM processed AlSi10Mg, FSP was performed on some as built (AB) samples using a Hermle UWF 1001 H milling machine at a rotational speed of 1000 rpm and a traverse speed of 500 mm/min. Fig. 1a-c illustrate key microstructural features of AB, SRHT and FSP samples. The characteristic Si-rich eutectic interconnected network surrounding the α-Al phase of AB microstructure (Fig. 1a) is clearly broken down after FSP as presented on Fig. 1c. In both the SRHT (Fig. 1b) and FSP (Fig. 1c) samples, the Si-rich eutectic phase becomes more globular, but the very fine nature of the microstructure is preserved. Regarding the fine Si precipitates found inside the α-Al cells of the AB material [21], observable on Fig. 1a, their evolution is different after SRHT and FSP treatments. While the SRHT seems to increase their size, the fraction and number of these fine particles are lower in the FSP material. This could be due to a solutionising effect induced by the temperatures reached during FSP, which can be of the order of 80% of the melting temperature of the Al alloys [11]. Indeed, a thermocouple introduced in the centre of the FSP tool 3 mm above the shoulder gave a reading of 447 °C during the course of FSP suggesting a temperature above 500°C in the processed material. Thus, the SRHT, only reaching 300 °C, remains significantly lower than the solutionising temperature. X-ray tomography measurements were performed at the European Synchrotron Radiation Facility (ESRF) ID11 beamline (Grenoble, France) on specimens extracted from AB, SRHT and FSP plates. The voxel size was 0.75 µm. In the final analysis porosities presenting volumes smaller than 3 voxels (i.e. ⌀eq ≤ 1.3 µm) were rejected from the population. Comparison of Fig. 1d, e and f illustrates the decrease of the proportion of observable porosities from about 0.13% for the AB and SRHT samples to 0.03% for the FSP sample. In the context of fatigue resistance enhancement, it is worth noting that the most important effect of FSP is the complete elimination of the larger porosities, which can reach up to ⌀eq = 50 µm. Indeed, after FSP the remaining porosity has an equivalent diameter below 10 µm. The volume fraction of porosity larger than 5 µm equivalent diameter is about 0.09% for AB and SRHT and 0.02% for FSP. Furthermore, large Fe-rich intermetallic particles that may act as damage nucleation sites were found to be broken down and dispersed, which is also expected to be beneficial for ductility enhancement [16].

Uniaxial tensile tests were performed following ASTM E8 / E8M -15a standard. Horizontally oriented round tensile specimens were extracted by machining from the AB plates and from the FSP region. Fig. 2 presents the true stress -true strain curves of the three states. Continuous lines correspond to the uniform deformation of the specimens up to necking, which is observable on FSP and SRHT specimens, but not on AB ones. The deformation at fracture, estimated by the final size of the fractured sample (εf = ln (A0 / Af)) and the final force applied (σf = Ff / Af), are represented with a cross. The post-necking tensile behaviour of the FSP and SRHT samples until fracture are estimated using a linear extrapolation.

All samples fulfil the Considère criterion. FSP results in a decrease of the strength level. Nevertheless, the FSP material presents similar yield and ultimate tensile strength levels to the SRHT material, thus showing a satisfactory mechanical behaviour. SRHT samples show more strain hardening at an earlier stage that could be attributed to more dislocation storage by the Orowan mechanism due to the fine (⌀eq ≈ 100 nm) Si-rich precipitates observed on Fig. 1b [22,23]. A significant improvement is observed in the fracture strain of SRHT and FSP samples. They present a fourfold increase in fracture strain (εf) compared to the SLM AB material. Taking into account the necessary compromise between strength, uniform elongation, ductility and residual stress relief, these treatments can be considered as significantly positive.

The fracture strain enhancement provided by SRHT and FSP compared to AB samples can be related to the significant changes of the micro and mesostructures. The damage mechanisms were analysed using SEM imaging along the longitudinal plane (i.e. section at mid-thickness along the loading direction) of tensile samples after failure (Fig. 3a-c). The observation of the damaged area close to the fracture surface reveals differences depending on the processing conditions. Damage originates predominantly through fracture of the Si-rich eutectic network for the AB material, as depicted on Fig. 3a. In the FSP and SRHT samples, damage is also related to the Si-rich eutectic phase, but it consists of both Si-rich particle fracture and particle-matrix decohesion (Fig. 3b for SRHT and Fig. 3c for FSP). Furthermore, damage events are more numerous and larger voids are observed on the FSP material, due to larger deformation before failure allowing more cavity growth.

At a mesostructural level, the melt pool boundaries seem to have a negative effect on the mechanical behaviour. This can be observed on Fig. 3d, which shows that the crack leading to failure partially followed a melt pool boundary. As more void nucleation occurs in the coarser microstructure within the reheated regions of the melt pool boundaries, the crack tends to preferentially follow these zones. These boundaries are reported as being softer [24] and thus experiencing deformation localisation. Therefore, damage concentrates in these regions leading to more nucleation of cavities in the Si-rich eutectic phase network. FSP eliminates the melt pool structure and the differentiated zones, thus bringing an homogenisation effect at the mesostructural level. Indeed, Fig. 3e shows that melt pools apparent on the right side of the figure, unaffected by the FSP process, have disappeared in the FSP zone.

Final fracture results from the succession of damage mechanisms involving nucleation of cavities on Si-rich particles, their growth and coalescence. In the AB sample, the Si-rich interconnected network acts as a source of numerous nucleation sites for cavities. This brittle network breaks down with increasing strain since it cannot follow the α-Al matrix deformation, which is more ductile. FSP and SRHT lead to a globularisation of this network. Thus, the behaviour of these samples is expected to be driven by the ductile aluminium network that can now deform more to accommodate external loading, allowing for higher ductility.

Fatigue testing was performed following ASTM E466 -15 standard (force controlled constant amplitude). Tensile -tensile tests (R = 0.1) with a frequency of 45 Hz were carried out on an Instron E10000 stress rig.

Specimens were polished down to an arithmetic roughness Ra < 0.1 µm in order to get rid of any surface state related effects. Table 1 gives a fatigue life comparison between AB, SRHT and FSP samples tested at a stress level of 250 MPa, i.e. slightly above the yield strength of the SRHT and FSP specimens and lower than the one of the AB samples. Slight strain hardening effects are thus expected [25]. SRHT state is used as a reference in addition to the AB state since it presents a similar yield strength to the FSP state. Tests were conducted up to a maximum of 10 7 cycles. These results show that FSP samples have a fatigue life up to at least two orders of magnitude longer than AB or SRHT ones.

Although SRHT brings a similar level of ductilisation to FSP, the fatigue life is much shorter for the former condition. This suggests that porosity plays a predominant role over the microstructure on fatigue resistance. The relative density of the material is satisfactory, being well above 99.5%. However, the presence of pores of a size larger than the very fine microstructure obtained after the SLM process becomes a critical factor. The large porosities found at surface or subsurface level act as fatigue crack nucleation sites. This can be appreciated through fractography analysis of the fractured fatigue samples. Fatigue cracks were found to systematically originate on sub-surface defects for AB and SRHT materials, as extensively described in the literature [2,26,27].

Low cycle fatigue testing of continuous radius samples was performed in various steps interrupted by X-ray tomography observations (i.e. ex situ). These observations were also performed at ESRF ID11 beamline. The samples had a curvature radius r = 2.5 mm, a minimum diameter of ⌀min ≈ 1 mm, and were polished with 1200 grit SiC paper down to an Ra ≈ 1.5 µm. They were tested at a maximum stress of 195 MPa and a stress ratio of 0.15. Compared to the tests reported in Table 1, the samples used for these ones had a rougher surface and a geometry leading to a higher triaxiality, justifying the lower applied maximum stress. Tomography allows monitoring the fatigue crack growth, which occurs under mode I (Fig. 4). To obtain the data for this figure, the voxels belonging to the cracks are projected onto a plane perpendicular to the loading direction. This results in a projected view of the crack, allowing to measure its length (i.e. maximum depth of the crack front). Fatigue crack nucleation is delayed after FSP while the final growth seems slightly affected. The elimination of the large porosities after FSP essentially acts on fatigue crack nucleation and is thus a decisive factor in the fatigue life improvement. FSP on SLM AlSi10Mg alloy brings not only excellent ductility similar to SRHT material but also very significant fatigue life enhancement (see summary table on supplementary material). FSP leads to the breakdown of the Si-rich eutectic phase interconnected network, resulting in a drastic increase of ductility. FSP also leads to porosity reduction and elimination of the large defects that are the nucleation sites for fatigue cracks in AB or SRHT materials. FSP also eliminates the melt pool structure and the presence of heat affected zones in the contour of the melt pools. These inhomogeneities lead to strain localisation at melt pool boundaries, so the FSP process helps to mitigate this effect.

The benefits brought by FSP allow its postulation as a potentially viable post-treatment for SLM AlSi10Mg and other AM parts in general. As a local surface treatment, its use can be recommended for parts presenting specific zones submitted to high mechanical loads, e.g. zones of stress concentration. Considering that these parts (or specific zones alone) are to go through a final machining or surface finishing step to avoid poor fatigue resistance derived from low surface quality, a good practice would be to implement FSP just before machining. It can be carried out in a milling machine or machining centre, in the same manufacturing step, in contrast to other potential methods, such as HIP, which would need an extra step.

Fig. 1 .Fig. 2 .Fig. 3 .Fig. 4 .

 1234 Fig. 1. SEM micrographs depicting the microstructural features and 3-D X-ray synchrotron tomography reconstructions showing porosity of SLM AlSi10Mg as built (a,d), after SRHT at 300 °C during 2 h (b,e) and after FSP at 1000 rpm rotational speed and 500 mm/min traverse speed (c,f)

Table 1

 1 Fatigue testing data for SLM AlSi10Mg AB and after SRHT or FSP (2 tests per state)

	State Max stress [MPa] Min stress [MPa]	Cycles to failure
	AB	250	25	7.6-10.1 • 10 4
	SRHT	250	25	6.6-8.0 • 10 4
	FSP	250	25	No failure after 5.5-10.0 • 10 6
			Supplementary

Table 1

 1 Porosity, tensile properties and fatigue life for SLM AlSi10Mg AB and after SRHT or FSP. σy represents the yield strength, UTS represents the ultimate tensile strength, εf represents the fracture strain.

		Porosity (%)	σy [MPa]	UTS [MPa]	εf	Fatigue cycles to failure at σmax250 MPa R0.1
	AB	0.13	287±2 473±2 0.1±0.03	7.6-10.1 • 10 4
	SRHT	0.13	212±12 319±16 0.42±0.06	6.6-8.0 • 10 4
	FSP	0.03	189±5 312±8 0.4±0.06 No failure after 5.5-10.0 • 10 6

Acknowledgements

The authors would like to thank the ESRF for allocation of beam time at ID11 (experiment number MA3758). JGSM acknowledges the support of the Fonds de la recherche scientifique -FNRS (FRIA grant), Belgium. This research has also been funded (from January 2017) by the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreement n°716678). Any-Shape is acknowledged for material supply.