Caterina Urban
email: urban@di.ens.fr

Antoine Miné
email: mine@di.ens.fr

Radhia Cousot

Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation ⋆

We present new static analysis methods for proving liveness properties of programs. In particular, with reference to the hierarchy of temporal properties proposed by Manna and Pnueli, we focus on guarantee (i.e., "something good occurs at least once") and recurrence (i.e., "something good occurs infinitely often") temporal properties. We generalize the abstract interpretation framework for termination presented by Cousot and Cousot. Specifically, static analyses of guarantee and recurrence temporal properties are systematically derived by abstraction of the program operational trace semantics. These methods automatically infer sufficient preconditions for the temporal properties by reusing existing numerical abstract domains based on piecewise-defined ranking functions. We augment these abstract domains with new abstract operators, including a dual widening.

To illustrate the potential of the proposed methods, we have implemented a research prototype static analyzer, for programs written in a C-like syntax, that yielded interesting preliminary results.

Introduction

Temporal properties play a major role in the specification and verification of programs. The hierarchy of temporal properties proposed by Manna and Pnueli [START_REF] Manna | A Hierarchy of Temporal Properties[END_REF] distinguishes four basic classes:

safety properties: "something good always happens", i.e., the program never reaches an unacceptable state (e.g., partial correctness, mutual exclusion); -guarantee properties: "something good happens at least once", i.e., the program eventually reaches a desirable state (e.g., termination); -recurrence properties: "something good happens infinitely often", i.e., the program reaches a desirable state infinitely often (e.g., starvation freedom); -persistence properties: "something good eventually happens continuously".

while1 ( x ≥ 0 ) do 2 x := x + 1; while 3 ( true ) do if 4 ( x ≤ 10 ) then 5 x := x + 1; else 6 x := -x; fi This paper concerns the verification of programs by static analysis. We set our work in the framework of Abstract Interpretation [START_REF] Cousot | Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints[END_REF], a general theory of semantic approximation that provides a basis for various successful industrial-scale tools (e.g., Astrée [START_REF] Bertrane | Static Analysis and Verification of Aerospace Software by Abstract Interpretation[END_REF]). Abstract Interpretation has to a large extent concerned safety properties and has only recently been extended to program termination [START_REF] Cousot | An Abstract Interpretation Framework for Termination[END_REF], which is just a particular guarantee property.

In this paper, we generalize the framework proposed by Cousot and Cousot for termination [START_REF] Cousot | An Abstract Interpretation Framework for Termination[END_REF] and we propose an abstract interpretation framework for proving guarantee and recurrence temporal properties of programs. Moreover, we present new static analysis methods for inferring sufficient preconditions for these temporal properties. Let us consider the program SIMPLE in Figure 1, where the program variables are interpreted in the set of mathematical integers 1 . The first while loop is an infinite loop for the values of x greater than or equal to zero: at each iteration the value of x is increased by one. The second while loop is an infinite loop: at each iteration, the value of x is increased by one or negated when it becomes greater than ten. Given the guarantee property "x = 3 at least once", where x = 3 is the desirable state, our approach is able to automatically infer that the property is true if the initial value of x is smaller than or equal to three. Given the recurrence property "x = 3 infinitely often", our approach is able to automatically infer that the property is true if the initial value of x is strictly negative (i.e., if the first while loop is never entered).

Our approach follows the traditional methods for proving liveness properties by means of a well-founded argument (i.e., a function from the states of a program to a well-ordered set whose value decreases during program execution). More precisely, we build a well-founded argument for guarantee and recurrence properties in an incremental way: we start from the desirable program states, where the function has value zero (and is undefined elsewhere); then, we add states to the domain of the function, retracing the program backwards and counting the maximum number of performed program steps as value of the function. Additionally, for recurrence properties, this process is iteratively repeated in order to construct an argument that is also invariant with respect to program execution steps so that even after reaching a desirable state we know that the execution will reach a desirable state again. We formalize these intuitions into sound and complete guarantee and recurrence semantics that are systematically derived by abstract interpretation of the program operational trace semantics.

In order to achieve effective static analyses, we further abstract these semantics. Specifically, we leverage existing numerical abstract domains based on piecewise-defined ranking functions [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF][START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF][START_REF] Urban | A Decision Tree Abstract Domain for Proving Conditional Termination[END_REF] by introducing new abstract operators, including a dual widening. The piecewise-defined ranking functions are attached to the program control points and represent an upper bound on the number of program execution steps before the program reaches a desirable state. They are automatically inferred through backward analysis and yield sufficient preconditions for the guarantee and recurrence temporal properties. We prove the soundness of the analysis, meaning that all program executions respecting these preconditions indeed satisfy the temporal properties, while a program execution that does not respect these preconditions might or might not satisfy the temporal properties.

To illustrate the potential of our approach, let us consider again the program SIMPLE in Figure 1. Given the guarantee property "x = 3 at least once", the piecewise-defined ranking function inferred at program control point 1 is:

f g 1 (x) =      -3x+10 x < 0 -2x+6 x ≥ 0 ∧ x ≤ 3 undefined otherwise
which bounds the wait (from the control point 1) for the desirable state x = 3 by -3x+10 program execution steps if x < 0, and by -2x+6 execution steps if x ≥ 0 ∧ x ≤ 3. In case x > 3, the analysis is inconclusive. In fact, if x > 3 the guarantee property is never true so the precondition x ≤ 3 for the guarantee property is the weakest precondition. Given the recurrence property "x = 3 infinitely often", the piecewise-defined ranking function at program point 1 bounds the wait for the next occurrence of the desirable state x = 3 by -3x+10 program execution steps:

f r 1 (x) = -3x+10 x < 0 undefined otherwise
Note that, if x ≥ 0 ∧ x ≤ 3, x = 3 occurs once but not infinitely often:

f g 1 is defined for x ≥ 0 ∧ x ≤ 3 but not f r 1 .
Again, the sufficient precondition x < 0 is also a necessary precondition. At program point 3 (i.e., at the beginning of the second while loop), we get the following piecewise-defined ranking function:

f g 3 (x) = f r 3 (x) = -3x+9 x ≤ 3 -3x+72 x > 3
which bounds the wait (from the control point 3) for the next occurrence of x = 3 by -3x+9 execution steps if x ≤ 3, and by -3x+72 execution steps if x > 3.

Our Contribution. In summary, this paper makes the following contributions. First, we present an abstract interpretation framework for proving guarantee and recurrence temporal properties of programs. In particular, we generalize the framework proposed by Cousot and Cousot for termination [START_REF] Cousot | An Abstract Interpretation Framework for Termination[END_REF]. Moreover, by means of piecewise-defined ranking function abstract domains [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF][START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF][START_REF] Urban | A Decision Tree Abstract Domain for Proving Conditional Termination[END_REF], we design new static analysis methods to effectively infer sufficient preconditions for these temporal properties, and provide upper bounds in terms of program execution steps on the wait before a program reaches a desirable state. Finally, we provide a research prototype static analyzer for programs written in a C-like syntax.

Limitations. In general, liveness properties are used to specify the behavior of concurrent programs and are satisfied only under fairness hypotheses. In this paper, we model concurrent programs as non-deterministic sequential programs and we assume that the fair scheduler is explicitly represented within the program (e.g., see [START_REF] Francez | Fairness[END_REF] and Example 6 in Section 8). We plan, as part of our future work, to extend our framework in order to explicitly express and handle fairness properties.

Outline of the Paper. Section 2 introduces the preliminary notions used in the paper. In Section 3, we give a brief overview of Cousot and Cousot's abstract interpretation framework for termination. In Section 4, we define a small specification language to describe guarantee and recurrence properties. The next two sections are devoted to the main contribution of the paper: we formalize our framework for guarantee and recurrence properties in Section 5 and in Section 6, respectively. In Section 7, we present decidable guarantee and recurrence abstractions based on piecewise-defined ranking functions. We describe our prototype static analyzer in Section 8. Finally, Section 9 discusses related work and Section 10 concludes.

Trace Semantics

Following [START_REF] Cousot | Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation[END_REF][START_REF] Cousot | An Abstract Interpretation Framework for Termination[END_REF], as a model of the operational semantics of a program, we use a transition system Σ,τ , where Σ is the (possibly infinite) set of program states and the program transition relation τ ⊆ Σ ×Σ describes the possible transitions between states during program execution. Note that this model allows representing programs with (possibly unbounded) non-determinism. Let Σ n be the set of all finite program state sequences of length n ∈ N. We use ε to denote the empty sequence, i.e., Σ 0 {ε}. The set of final states Ω {s ∈ Σ | ∀s ′ ∈ Σ : s,s ′ ∈ τ } can be understood as a set of sequences of length one and the program transition relation τ can be understood as a set of sequences of length two. Let Σ + n∈N + Σ n be the set of all non-empty finite sequences, Σ * Σ 0 ∪ Σ + be the set of all finite sequences, Σ ω be the set of all infinite sequences, Σ +∞ Σ + ∪ Σ ω be the set of all non-empty finite or infinite sequences and Σ * ∞ Σ * ∪ Σ ω be the set of all finite or infinite sequences. We write σσ ′ for the concatenation of sequences σ,σ ′ ∈ Σ +∞ (with σǫ = ǫσ = σ and σσ ′ = σ when σ ∈ Σ ω ), T + T ∩ Σ + for the selection of the non-empty finite sequences of T ⊆ Σ +∞ , T ω T ∩ Σ ω for the selection of the infinite sequences of T ⊆ Σ +∞ and T ;

T ′ {σsσ ′ | s ∈ Σ ∧ σs ∈ T ∧ sσ ′ ∈ T ′ } for the merging of sets of sequences T,T ′ ⊆ Σ +∞ .
The maximal trace semantics τ +∞ ⊆ Σ +∞ generated by a transition system Σ,τ is the union of the set of all non-empty finite program execution traces that are terminating with a final state, and the set of all infinite execution traces. It can be expressed as a least fixpoint in the complete lattice Σ +∞ ,⊑,⊔,⊓,Σ ω ,Σ + [8]:

τ +∞ lfp ⊑ φ +∞ φ +∞ (T ) Ω ⊔ (τ ; T ) (1)
where

T 1 ⊑ T 2 T + 1 ⊆ T + 2 ∧ T ω 1 ⊇ T ω 2 and T 1 ⊔T 2 (T + 1 ∪T + 2 ) ∪ (T ω 1 ∩T ω 2 ).

Termination Semantics

The Floyd/Turing traditional method for proving program termination [START_REF] Floyd | Assigning Meanings to Programs[END_REF] consists in inferring ranking functions, namely mappings from program states to elements of a well-ordered set (e.g., O,< , the well-ordered set of ordinals) whose value decreases during program execution.

In [START_REF] Cousot | An Abstract Interpretation Framework for Termination[END_REF], Cousot and Cousot prove the existence of a most precise program ranking function2 τ t ∈ Σ ⇀ O that can be expressed in fixpoint form as follows:

τ t lfp ∅ φ t φ t (v) λs.      0 s ∈ Ω sup{v(s ′ )+1 | s,s ′ ∈ τ } s ∈ pre(dom(v)) undefined otherwise ( 2
)
where ∅ is the totally undefined function,

v 1 v 2 dom(v 1 ) ⊆ dom(v 2 ) ∧ ∀x ∈ dom(v 1 ) : v 1 (x) ≤ v 2 (x) and pre(X) {s ∈ Σ | ∀s ′ ∈ Σ : s,s ′ ∈ τ ⇒ s ′ ∈ X}.
The most precise ranking function τ t extracts the well-founded part of the transition relation τ : starting from the final states in Ω, where the function has value zero, and retracing the program backwards while mapping each program state in Σ definitely leading to a final state (i.e., a program state such that all the traces to which it belongs are terminating) to an ordinal in O representing an upper bound on the number of program execution steps remaining to termination. The domain dom(τ t ) of τ t is the set of states definitely leading to program termination; any trace starting in a state s ∈ dom(τ t ) must terminate in at most τ t (s) execution steps, while at least one trace starting in a state s ∈ dom(τ t ) does not terminate: Theorem 1. A program terminates for all execution traces starting from an initial state s ∈ Σ if and only if s ∈ dom(τ t ).

We would like to emphasize the elegance of the abstract interpretation theory which allows to tie together seemingly unrelated semantics by different abstractions of the same operational trace semantics, i.e., the maximal trace semantics (1) [START_REF] Cousot | Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation[END_REF]. The semantics, rather than being first derived by intuition and then proved correct, are systematically derived by abstract interpretation. Specifically, in [START_REF] Cousot | An Abstract Interpretation Framework for Termination[END_REF], in order to derive the most precise ranking function (2), Cousot and Cousot define the following abstraction functions:

-The prefix abstractions pf ∈ Σ +∞ → P(Σ +∞ ) and pf ∈ P(Σ +∞ ) → P(Σ +∞ ) yield respectively the set of prefixes of a sequence σ ∈ Σ +∞ and the set of prefixes of a set of sequences

T ⊆ Σ +∞ : pf(σ) {σ ′ ∈ Σ +∞ | ∃σ ′′ ∈ Σ * ∞ : σ = σ ′ σ ′′ } pf(T ) {pf(σ) | σ ∈ T } (3)
The neighborhood of a sequence σ ∈ Σ +∞ in a set of sequences T ⊆ Σ +∞ is the set of sequences σ ′ ∈ T with a common prefix with σ:

{σ ′ ∈ T | pf(σ)∩pf(σ ′ ) = ∅}.
-The termination abstraction α t ∈ P(Σ +∞ ) → P(Σ + ) selects from a set of sequences T ⊆ Σ +∞ the sequences that are finite and whose neighborhood in T consists only of finite traces:

α t (T ) {σ ∈ T + | pf(σ) ∩ pf(T ω ) = ∅} (4)
Example 1. Let T = {ab, aba, ba, bb, ba ω }, then α t (T ) = {ab, aba}. In fact, pf(ab) ∩ pf(ba ω ) = ∅ and pf(aba

) ∩ pf(ba ω ) = ∅, while pf(ba) ∩ pf(ba ω ) = {b,ba} and pf(bb) ∩ pf(ba ω ) = {b}. ⊓ ⊔ -The transition abstraction → α∈ P(Σ +∞ ) → P(Σ × Σ) extracts from a set of sequences T ⊆ Σ +∞ the smallest transition relation r ⊆ Σ ×Σ that generates T : → α (T ) { s,s ′ | ∃σ,σ ′ ∈ Σ * ∞ : σss ′ σ ′ ∈ T } -The ranking abstraction α rk ∈ P(Σ ×Σ) → (Σ ⇀ O)
provides the rank of the elements in the domain of a relation r ⊆ Σ ×Σ:

α rk (r)s      0 ∀s ′ ∈ Σ : s,s ′ ∈ r sup α rk (r)s ′ +1 s ′ ∈ dom(α rk (r)) ∧ s,s ′ ∈ r otherwise -The variant abstraction α v ∈ P(Σ + ) → (Σ ⇀ O)
provides the rank of the elements in the domain of the smallest transition relation that generates a set of sequences T ⊆ Σ + :

α v (T ) α rk ( → α (T )) (5)
The most precise ranking function (2) can now be explicitly defined as abstract interpretation of the program maximal trace semantics (1) [START_REF] Cousot | An Abstract Interpretation Framework for Termination[END_REF]:

τ t α v (α t (τ +∞ ))
In Section 5 and Section 6, we will follow the same abstract interpretation approach in order to systematically derive sound and complete semantics for proving guarantee and recurrence temporal properties of programs.

Specification Language

In general, we define a program property as a set of sequences. A program has a certain property if all the program execution traces belong to the property. In this paper, with respect to the hierarchy of temporal properties proposed in [START_REF] Manna | A Hierarchy of Temporal Properties[END_REF], we focus on guarantee ("something good happens at least once") and recurrence ("something good happens infinitely often") properties. In particular, we consider guarantee and recurrence properties that are expressible by temporal logic.

We define a small specification language, which will be used to describe properties of program states. Let X be a finite set of program variables. We split the program state space Σ into program control points L and environments E X → Z,

δ ::= X | n | -δ | δ1 ⋄δ2 X ∈ X , n ∈ Z, ⋄ ∈ {+,-, * ,/} β ::= true | false | !β | β1 ∨β2 | β1 ∧β2 | δ1 ⊲⊳ δ2 ⊲⊳ ∈ {<,≤,=, =,>,≥} ϕ ::= β | l : β | ϕ1 ∨ϕ2 | ϕ1 ∧ϕ2 l ∈ L Fig. 2. Syntax of State Properties.
which map each program variable to an integer value. In Figure 2 we define inductively the syntax of the state properties. The predicate l : β allows specifying a state property at a particular control point l ∈ L. We write s |= ϕ when the state s ∈ Σ has the property ϕ, and Σ ϕ {s ∈ Σ | s |= ϕ} for the set of states Σ ϕ ⊆ Σ that have the property ϕ.

In the following, we define the program properties of interest by means of the temporal operators always and eventually ♦. The guarantee properties are expressible by a temporal formula of the form ♦ϕ, for some state property ϕ. The formula expresses that at least one state in every program execution trace has the property ϕ, but it does not promise any repetition. In general, the guarantee properties are used to ensure that some event happens once during a program execution, such as program termination or eventual consistency. Indeed, program termination can be expressed as the guarantee property ♦l e : true, where l e ∈ L is the program final control point.

The recurrence properties are expressible by a temporal formula of the form ♦ϕ, for some state property ϕ. The formula expresses that infinitely many states in every program execution trace have the property ϕ. In general, the recurrence properties are used to ensure that some event happens infinitely many times during a program execution (e.g., a request is always eventually answered).

Guarantee Temporal Properties

In the following, we generalize Section 3 from termination to guarantee properties. We define a sound and complete semantics for proving guarantee temporal properties by abstract interpretation of the program maximal trace semantics.

Let S ⊆ Σ be a set of states and let S +∞ ⊆ Σ +∞ be the set of non-empty finite or infinite sequences of states in S ⊆ Σ. In the following, we write S Σ \S for the set of states that are not in S and T S T ∩ S +∞ for the selection of the sequences of T that are non-empty sequences of states in S.

In order to define our semantics we need the following abstraction functions:

-The subsequence abstraction α s ∈ P(Σ +∞ ) → P(Σ +∞ ) extracts from a set of sequences T ⊆ Σ +∞ the subsequences of sequences in T :

α s (T ) {σ ∈ Σ +∞ | ∃σ ′ ∈ Σ * ,σ ′′ ∈ Σ * ∞ : σ ′ σσ ′′ ∈ T }
-The guarantee abstraction α g ∈ P(Σ) → P(Σ +∞ ) → P(Σ + ), given a set of states S ⊆ Σ and a set of sequences T ⊆ Σ +∞ , extracts from T ⊆ Σ +∞ the subsequences of sequences of T whose neighborhood in α s (T ) consists only of sequences of states in S that are terminating with a state s ∈ S:

α g (S)T σs ∈ α s (T ) ∩ Σ + s ∈ S ∧ σ ∈ S * ∧ ∀σ ′ ∈ pf(σ) : T σ ′ ∩ S+∞ = ∅ (6)
where pf ∈ Σ +∞ → P(Σ +∞ ) is the prefix abstraction (3) of Section 3 and

T σ {σσ ′′ ∈ Σ +∞ | σ ′′ ∈ Σ * ∞ ∧ ∃σ ′ ∈ Σ * ∞ : σ ′ σσ ′′ ∈ T } is the set of suffixes of sequences of T ⊆ Σ +∞ with prefix σ ∈ Σ +∞ . Example 2. Let T = {cd ω ,(cd) ω }, then T d = {d ω ,(dc) ω }. ⊓ ⊔ Example 3. Let T = {(abcd) ω , (cd) ω , a ω , cd ω } and S = {c}, then α g (S)T = {c,bc}.
Let us consider the trace (abcd) ω : the subsequences of (abcd) ω that are terminating with c (and never encounter c before) are {c,bc,abc,dabc}. Let us consider the subsequence abc:

T ab ∩ S+∞ = ∅ but T a ∩ S+∞ = {a ω }. Now let us consider dabc: T dab ∩ S+∞ = ∅ and T da ∩ S+∞ = ∅ but T d ∩ S+∞ = {d ω }. ⊓ ⊔
The guarantee semantics τ g ∈ P(Σ) → (Σ ⇀ O) of a program can now be defined by abstract interpretation of the program maximal trace semantics (1):

τ g (S) α v (α g (S)τ +∞ ) = lfp ∅ φ g (S) φ g (S)v λs.      0 s ∈ S sup{v(s ′ )+1 | s,s ′ ∈ τ } s ∈ pre(dom(v)) ∧ s ∈ S undefined otherwise (7)
where α v ∈ P(Σ + ) → (Σ ⇀ O) is the variant abstraction (5) presented in Section 3. Intuitively, given a set of states S ⊆ Σ, the guarantee semantics τ g (S) is defined starting from the states in S and retracing the program backwards while mapping each program state definitely leading to S (i.e., a program state such that all the traces to which it belongs eventually reach a state in S) to an ordinal in O representing an upper bound on the number of program execution steps remaining to S. The domain dom(τ g (S)) of τ g (S) is the set of states definitely leading to a state in S: any trace starting in a state s ∈ dom(τ g (S)) must reach a state in S in at most τ g (S)s execution steps, while at least one trace starting in a state s ∈ dom(τ g (S)) does not reach S.

Note that, when S is the set of final states Ω, φ g (Ω) = φ t and we rediscover precisely Cousot and Cousot's termination semantics [START_REF] Cousot | An Abstract Interpretation Framework for Termination[END_REF] presented in Section 3.

Let ϕ be a state property. We define the ϕ-guarantee semantics τ g ϕ ∈ Σ ⇀ O:

τ g ϕ τ g (Σ ϕ ) (8)
The semantics τ g ϕ is sound and complete for proving a guarantee property ♦ϕ:

Theorem 2. A program satisfies a guarantee property ♦ϕ for all execution traces starting from an initial state s ∈ Σ if and only if s ∈ dom(τ g ϕ ).

6 Recurrence Temporal Properties

In the following, we define a sound and complete semantics for proving recurrence temporal properties by abstract interpretation of the program maximal trace semantics, following the same approach used in Section 5 for guarantee temporal properties. In particular, the recurrence semantics that we are going to define reuses the guarantee semantics of Section 5 as starting point: from the guarantee that some event happens once during a program execution, the recurrence semantics ensures that the event happens infinitely many times.

In order to define our semantics we need the following abstraction function:

-The recurrence abstraction α r ∈ P(Σ) → P(Σ +∞ ) → P(Σ + ), given a set of states S ⊆ Σ and a set of sequences T ⊆ Σ +∞ , extracts from T the subsequences of sequences of T whose neighborhood in α s (T ) consists only of sequences of states in S that are terminating with a state in S, and that are prefixes of sequences of T that reach infinitely often a state in S:

α r (S)T gfp ⊆ α g (S)T φ α r (T,S) φ α r (T,S)T ′ α g ( pre(T )T ′ ∩ S)T (9)
where pre(T )

T ′ {s ∈ Σ | ∀σ ∈ Σ * ,σ ′ ∈ Σ * ∞ : σsσ ′ ∈ T ⇒ pf(σ ′ ) ∩ T ′ = ∅} and α g ∈ P(Σ) → P(Σ +∞ ) → P(Σ +
) is the guarantee abstraction (6) of Section 5.

To explain intuitively (9), we use the Kleene dual fixpoint theorem [START_REF] Cousot | Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation[END_REF] to rephrase α r (S)T as follows:

α r (S)T = i∈N T i+1 where T i+1 φ α r (T,S) i (α g (S)T )

Then, for i = 0, we get the set T 1 = α g (S)T of subsequences of sequences of T that guarantee S at least once. For i = 1, starting from T 1 , we derive the set of states S 1 = pre(T )T 1 ∩ S (i.e., S 1 ⊆ S) whose successors all belong to the subsequences in T 1 , and we get the set T 2 = α g (S 1 )T of subsequences of sequences of T that guarantee S 1 at least once and thus guarantee S at least twice. Note that all the subsequences in T 2 terminate with a state s ′ ∈ S 1 and therefore are prefixes of subsequence of T that reach S at least twice. More generally, for each i ∈ N, we get the set T i+1 of subsequences which are prefixes of subsequences of T that reach S at least i+1 times, i.e., the subsequences that guarantee S at least i+1 times. The greatest fixpoint thus guarantees S infinitely often.

Example 4. Let T = {(cd) ω ,ca ω ,d(be) ω } and let S = {b,c,d}. For i = 0, we have T 1 = α g (S)T = {b,eb,c,d}. For i = 1, we derive S 1 = {b,d}, since c(dc) ω ∈ T and pf((dc) ω ) ∩ T 1 = {d} = ∅ but ca ω ∈ T and pf(a ω ) ∩ T 1 = ∅. We get T 2 = α g (S 1 )T = {b, eb, d}. For i = 2, we derive S 2 = {b}, since d(be) ω ∈ T and pf((be) ω ) ∩ T 1 = {b} = ∅ but d(cd) ω ∈ T and pf((cd) ω ) ∩ T 2 = ∅. We get T 3 = α g (S 2 )T = {b,eb} which is the greatest fixpoint: the only subsequences of sequences in T that guarantee S infinitely often start with b or eb.

⊓ ⊔

The recurrence semantics τ r ∈ P(Σ) → (Σ ⇀ O) of a program can now be defined by abstract interpretation of the program maximal trace semantics (1):

τ r (S) α v (α r (S)τ +∞ ) = gfp τ g (S) φ r (S)
φ r (S)v λs. v(s) s ∈ dom(τ g ( pre(dom(v)) ∩ S)) undefined otherwise [START_REF] Cousot | Higher Order Abstract Interpretation (and Application to Comportment Analysis Generalizing Strictness, Termination, Projection, and PER Analysis[END_REF] where α v ∈ P(Σ + ) → (Σ ⇀ O) is the variant abstraction (5) presented in Section 3 and τ g ∈ P(Σ) → (Σ ⇀ O) is the guarantee semantics (7) defined in Section 5. Note that, given the definition of ( 7), (10) contains a nested fixpoint.

Given a set of states S ⊆ Σ, the recurrence semantics τ r (S) maps each program state definitely leading infinitely many times to S to an ordinal in O representing an upper bound on the number of execution steps remaining to the next occurrence of a state in S: any trace starting in a state s ∈ dom(τ r (S)) must reach the next occurrence of a state in S in at most τ r (S)s execution steps, while at least one trace starting in a state s ∈ dom(τ r (S)) reaches a state in S at most finitely many times.

Let ϕ be a state property. We the define ϕ-recurrence semantics τ r ϕ ∈ Σ ⇀ O:

τ r ϕ τ r (Σ ϕ ) (11)
The semantics τ r ϕ is sound and complete for proving a recurrence property ♦ϕ: Theorem 3. A program satisfies a recurrence property ♦ϕ for all execution traces starting from an initial state s ∈ Σ if and only if s ∈ dom(τ r ϕ ).

Piecewise-Defined Ranking Functions

The termination semantics τ t of Section 3, the ϕ-guarantee semantics τ g ϕ of Section 5 and the ϕ-recurrence semantics τ r ϕ of Section 6 are usually not computable (i.e., when the program state space is infinite).

In [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF][START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF][START_REF] Urban | A Decision Tree Abstract Domain for Proving Conditional Termination[END_REF], we present decidable abstractions of τ t by means of piecewisedefined ranking functions over natural numbers [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF], over ordinals [START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF] and with relational partitioning [START_REF] Urban | A Decision Tree Abstract Domain for Proving Conditional Termination[END_REF]. In the following, we will briefly recall the main characteristics of these abstractions and we will show how to modify the abstract domains in order to obtain decidable abstractions of τ g ϕ and τ r ϕ as well.

Abstract Termination Semantics

The formal treatment given in the previous sections is defined over general transition systems. In practice, it is sufficient to provide a transfer function for each atomic instruction of a programming language to define a semantics for all the programs in the language and obtain an effective static analysis after opportune abstraction.

In [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF], we provide an isomorphic definition of the termination semantics τ t ∈ Σ ⇀ O for a C-like programming language by partitioning with respect to the set of program control points L: τ t ∈ L → (E ⇀ O). In this way, to each control point l ∈ L corresponds a function v ∈ E ⇀ O and to each program statement i corresponds a transfer function i t ∈ (E ⇀ O) → (E ⇀ O). As an example, given an assignment x := e of the expression e to the variable x ∈ X , the transfer function is defined as follows:

x := e t v λρ. sup{v(ρ[x → z])+1 | z ∈ e ρ} ∀z ∈ e ρ : ρ[x → z] ∈ dom(v) undefined otherwise
where e ∈ E → ℘(Z) maps an environment ρ ∈ E to the set of all possible values for the expression e in the given environment. In case of a loop statement the transfer function involves a least fixpoint. More details can be found in [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF]. Subsequently, in [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF][START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF][START_REF] Urban | A Decision Tree Abstract Domain for Proving Conditional Termination[END_REF] we present an abstract termination semantics τ α t ∈ L → V: to each program control point l ∈ L corresponds an element v ∈ V of an abstract domain V, equipped with a concretization function γ ∈ V → (E ⇀ O) and a sound abstract transfer function i α t ∈ V → V for each program statement i. In particular, the elements of the abstract domain V are piecewise-defined ranking functions represented by means of two parameter abstract domains: an abstract domain whose elements establish the shape of the pieces of the ranking functions, and an abstract domain whose elements represent the value of the ranking functions within their pieces. As an example, in [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF] we consider piecewise-defined ranking functions whose pieces have the shape of intervals and whose value is represented by an affine function.

The abstract transfer functions are combined together to compute an abstract ranking function for a program through backward analysis. The starting point is the constant function equal to zero at the program final control point. This function is then propagated backwards towards the program initial control point taking assignments and tests into account and, in case of loops, solving least fixpoints by iteration with a widening operator. We give an intuition for how the abstract assignment transfer function works by means of the following example:

Example 5. Let us consider the piecewise-defined ranking function with value 2x+1 for x ∈ [-∞,3] and undefined elsewhere, and the assignment x := x + 1. The abstract assignment transfer function substitutes the variable x with the expression x + 1 and increases the value of the function by one (to take into account that one more program step is needed before termination). The result is the piecewisedefined ranking function with value 2(x+1)+1+1 = 2x+4 for x+1 ∈ [-∞,3] (i.e., x ∈ [-∞,2]) and undefined elsewhere.

⊓ ⊔

We refer to [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF][START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF][START_REF] Urban | A Decision Tree Abstract Domain for Proving Conditional Termination[END_REF] for more details.

The abstract transfer functions are sound with respect to the approximation order [START_REF] Cousot | Higher Order Abstract Interpretation (and Application to Comportment Analysis Generalizing Strictness, Termination, Projection, and PER Analysis[END_REF] for further discussion on approximation and computational order of an abstract domain):

v 1 ⊑ v 2 dom(v 1 ) ⊇ dom(v 2 ) ∧ ∀x ∈ dom(v 2 ) : v 1 (x) ≤ v 2 (x) (see
Theorem 4. i t γ(v) ⊑ γ( i α t v)
The backward analysis computes an over-approximation of the value of the most precise ranking function τ t and an under-approximation of its domain of definition dom(τ t ). In this way, an abstraction provides sufficient preconditions for program termination: if the abstraction is defined on a program state, then all the program execution traces branching from that state are terminating.

Abstract Guarantee Semantics

In the following, we describe how to reuse the piecewise-defined ranking function abstract domains introduced in [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF][START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF][START_REF] Urban | A Decision Tree Abstract Domain for Proving Conditional Termination[END_REF] and what changes are required in order to obtain decidable abstractions of the ϕ-guarantee semantics τ g ϕ (8). First, as before, we partition the ϕ-guarantee semantics τ g ϕ ∈ Σ ⇀ O with respect to the set of program control points L:

τ g ϕ ∈ L → (E ⇀ O). The transfer functions i g ϕ ∈ (E ⇀ O) → (E ⇀ O)
behave as the transfer functions for the termination semantics but in addition they reset the value of the ranking function for the environments that have the property ϕ. As an example, the transfer function for an assignment x := e is now defined as follows:

x := e g v λρ.

     0 ρ |= ϕ sup{v(ρ[x → z])+1 | z ∈ e ρ} ρ |= ϕ ∧ ∀z ∈ e ρ : ρ[x → z] ∈ dom(v) undefined otherwise
where ρ |= ϕ means that the environment ρ ∈ E has the property ϕ (cf. Section 4). Then, we define the abstract ϕ-guarantee semantics τ α g ϕ ∈ L → V: to each program control point l ∈ L corresponds a piecewise-defined ranking function v ∈ V. To each program statement i corresponds a sound (with respect to the approximation order ⊑) abstract transfer function i α g ϕ ∈ V → V:

Theorem 5. i g ϕ γ(v) ⊑ γ( i α g ϕ v)
We give an intuition for how the abstract assignment transfer function now works by means of the following example: Example 6. Let us consider the guarantee property ♦(x = 3) and let us consider again, as in Example 5, the piecewise-defined ranking function with value 2x+1 for x ∈ [-∞,3] and undefined elsewhere, and the assignment x := x + 1. As in Example 5, the abstract assignment transfer function substitutes the variable x with the expression x+1 and increases the value of the function by one. Unlike Example 5, it also resets the value of the function for x ∈ [START_REF] Biere | Liveness Checking as Safety Checking[END_REF][START_REF] Biere | Liveness Checking as Safety Checking[END_REF]. The result is the piecewise-defined ranking function with value 2x+4 for x ∈ [-∞,2], 0 for x ∈ [START_REF] Biere | Liveness Checking as Safety Checking[END_REF][START_REF] Biere | Liveness Checking as Safety Checking[END_REF] and undefined elsewhere.

⊓ ⊔

As before, the abstract transfer functions are combined together through backward analysis. The starting point is now the constant function equal to zero only for the environments that have the property ϕ, and undefined elsewhere, at the program final control point. The backward analysis computes an over-approximation of the value of the function τ g ϕ and an under-approximation of its domain of definition dom(τ g ϕ ). In this way, an abstraction provides sufficient preconditions for the guarantee property ♦ϕ: if the abstraction is defined on a program state, then all the program execution traces branching from that state eventually reach a state with the property ϕ. Note that, when the property ϕ is l e : true, where l e ∈ L is the program final control point, we rediscover the backward termination analysis from Section 7.1.

Abstract Recurrence Semantics

In the following, we describe how to reuse the piecewise-defined ranking function abstract domains introduced in [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF][START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF][START_REF] Urban | A Decision Tree Abstract Domain for Proving Conditional Termination[END_REF] and what changes are required in order to obtain decidable abstractions of the ϕ-recurrence semantics τ r ϕ [START_REF] Cousot | An Abstract Interpretation Framework for Termination[END_REF]. As before, we associate each program control point l ∈ L with a different ranking function v ∈ V: τ r ϕ ∈ L → (E ⇀ O). The transfer functions i r ϕ ∈ (E ⇀ O) → (E ⇀ O) behave as the transfer functions for the guarantee semantics with the only difference that they reset the value of the ranking function for the environments that have the property ϕ only if all successors of the environments (by means of the program statement i) belong to the domain of the ranking function; hence, they ensure that each time ϕ is satisfied, it will be satisfied again in the future. As an example, the transfer function for an assignment x := e is defined as follows:

x := e r v λρ.

     0 ρ |= ϕ ∧ ∀z ∈ e ρ : ρ[x → z] ∈ dom(v) sup{v(ρ[x → z])+1 | z ∈ e ρ} ρ |= ϕ ∧ ∀z ∈ e ρ : ρ[x → z] ∈ dom(v) undefined otherwise
Then, we define the abstract ϕ-recurrence semantics τ α r ϕ ∈ L → V by means of sound (with respect to ⊑) abstract transfer functions i α r ϕ ∈ V → V:

Theorem 6. i r ϕ γ(v) ⊑ γ( i α r ϕ v)
We give an intuition for how the abstract assignment transfer function now works by means of the following example: Example 7. Let us consider the guarantee property ♦(x = 3) and let us consider again, as in Example 6, the piecewise-defined ranking function with value 2x+1 for x ∈ [-∞,3] and undefined elsewhere, and the assignment x := x + 1. Unlike Example 6, the abstract assignment transfer function does not reset the value of the function for x ∈ [START_REF] Biere | Liveness Checking as Safety Checking[END_REF][START_REF] Biere | Liveness Checking as Safety Checking[END_REF] because the ranking function is undefined for x ∈ [START_REF] Bradley | An Incremental Approach to Model Checking Progress Properties[END_REF][START_REF] Bradley | An Incremental Approach to Model Checking Progress Properties[END_REF] (i.e., the successor of the environment x ∈ [START_REF] Biere | Liveness Checking as Safety Checking[END_REF][START_REF] Biere | Liveness Checking as Safety Checking[END_REF] by means of the assignment x := x + 1). The result is the piecewise-defined ranking function with value 2x+4 for x ∈ [-∞,2], and undefined elsewhere.

Let us consider instead the piecewise-defined ranking function with value 2x+1 for x ∈ [-∞,4] and undefined elsewhere. The result of the assignment x := x + 1 is now the piecewise-defined ranking function with value 2x+4 for x ∈ [-∞,2], 0 for x ∈ [START_REF] Biere | Liveness Checking as Safety Checking[END_REF][START_REF] Biere | Liveness Checking as Safety Checking[END_REF] and undefined elsewhere.

⊓ ⊔

Since the program final states cannot satisfy a recurrence property, the starting point of the recurrence backward analysis is now the totally undefined function at the program final control point. This function is then propagated backwards towards the program initial control point.

Note that, in case of a loop statement, according to the definition (10) of τ r ϕ from Section 5, the transfer function involves a least fixpoint nested into a greatest fixpoint. Nested fixpoints are solved by iteration with the same widening operator used for termination [START_REF] Urban | A Decision Tree Abstract Domain for Proving Conditional Termination[END_REF] for the least fixpoint, and a new dual widening operator ▽ for the greatest fixpoint. The dual widening ▽ obeys (i) γ(A) ⊓ γ(B) ⊑ γ(A ▽ B), and (ii) for any sequence (X n ) n∈N , the sequence

Y 0 = X 0 , Y n+1 = Y n ▽ X n+1 stabilizes (i.e., ∃i : Y i+1 = Y i ).
Dual widenings are rather unknown and, up to our knowledge, only few practical instance has been proposed (e.g., [START_REF] Chakarov | Expectation Invariants for Probabilistic Program Loops as Fixed Points[END_REF][START_REF] Miné | Inferring Sufficient Conditions with Backward Polyhedral Under-Approximations[END_REF]). In our case, the dual widening ▽ enforces the termination of the analysis by preventing the set of pieces of a piecewise-defined ranking function from growing indefinitely: given two piecewise-defined ranking functions v 1 ∈ V and v 2 ∈ V, it enforces the piecewise-definition of the first function v 1 on the second function v 2 . Then, for each piece of the ranking functions, it maintains the value of the function only if both v 1 and v 2 are defined on that piece (cf. Figure 3). The backward analysis computes an over-approximation of the value of the function τ r ϕ and an under-approximation of its domain dom(τ r ϕ ). In this way, an abstraction provides sufficient preconditions for the recurrence property ♦ϕ: if the abstraction is defined on a program state, then all the program execution traces branching from that state always eventually reach a state with the property ϕ.

Implementation

We have incorporated the static analysis methods for guarantee and recurrence temporal properties that we have presented into our prototype static analyzer FuncTion based on piecewise-defined ranking functions. It is available online 3 .

The prototype accepts (non-deterministic) programs written in a C-like syntax and, when the guarantee or recurrence analysis methods are selected, it accepts state properties written as C-like pure expressions. It is written in OCaml and, at the time of writing, the available abstract domains to control the pieces of the ranking functions are based on intervals, octagons and convex polyhedra, and the available abstract domain to represent the value of the ranking functions is based on affine functions. The operators for the intervals, octagons and convex polyhedra abstract domains are provided by the APRON library [START_REF] Jeannet | Apron: A Library of Numerical Abstract Domains for Static Analysis[END_REF]. It is also possible to activate the extension to ordinal-valued ranking functions [START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF] and tune the precision of the analysis by adjusting the widening delay.

The analysis proceeds by structural induction on the program syntax, iterating loops with widening (and, for recurrence properties, both widening and dual widening) until stabilization. In case of nested loops, the analysis stabilizes the inner loop for each iteration of the outer loop.

To illustrate the effectiveness of our new static analysis methods, we consider more examples besides the program SIMPLE of Section 1.

Example 8. Let us consider the program COUNT-DOWN in Figure 4 and the recurrence property ♦x = 0. At each iteration of the outer loop, the variable x takes the value of some counter c (which initially has value one); then, the inner loop decreases the value of x and increases the value of the counter c until x becomes less than or equal to zero. The recurrence property is clearly satisfied and indeed our prototype (parameterized by intervals and affine functions) is able to prove it: the piecewise-defined ranking function inferred at program control point 1 bounds the wait for the next occurrence of the desirable state x = 0 by five program execution steps (i.e., executing the assignment c := 1, testing the outer loop condition, executing the assignment x := c, testing the inner loop condition and executing the assignment x := x -1). The analysis infers a more interesting raking function associated to program control point 4:

f r 4 (x,c) =                3c+2 x < 0 ∧ c > 0 3 x < 0 ∧ c = 0 1 x = 0 ∧ c ≥ 0 3x-1 (x = 1 ∧ c ≥ -1) ∨ (x ≥ 2 ∧ c ≥ -2) undefined otherwise
The function bounds the wait for the next occurrence of x = 0 by 3c+2 execution steps if x < 0 ∧ c > 0, by 3 execution steps if x < 0 ∧ c = 0 (i.e., testing the inner loop condition, testing the outer loop condition and executing the assignment x := c), by 1 execution step if x = 0 ∧ c ≥ 0 (i.e., testing the inner loop condition) and by 3x-1 execution steps if (x = 1 ∧ c ≥ -1) ∨ (x ≥ 2 ∧ c ≥ -2). In the last case there is a precision loss due to a lack of expressiveness of the intervals abstract domain: if x is strictly positive at program control point 4, the weakest precondition ensuring infinitely many occurrences of the desirable state x = 0 is c ≥ -x (which is not representable in the intervals abstract domain).

⊓ ⊔ while 1 ( true ) do 2 x := ?;

while 3 ( x = 0 ) do if 4 ( x > 0 ) then 5 x := x -1; else 6 x := x + 1; fi Fig. 5. Program SINK. f lag1 := 0; f lag2 := 0;               while 1 ( true ) do 2 f lag1 := 1 3 turn := 2 while 4 ( f lag2 = 0 ∧ turn = 1 ) do BUSY WAIT 5 CRITICAL SECTION 6 f lag1 := 0                             while 1 ( true ) do 2 f lag2 := 1 3 turn := 1 while 4 ( f lag1 = 0 ∧ turn = 2 ) do BUSY WAIT 5 CRITICAL SECTION 6 f lag2 := 0               Fig. 6. Program PETERSON (Peterson's Algorithm).
Example 9. Let us consider the program SINK in Figure 5 and the recurrence property ♦x = 0. At each iteration of the outer loop, the value of the variable x is reset by the non-deterministic assignment x := ?; then, the inner loop decreases or increases the value of x until it becomes equal to zero. Note that the program features unbounded non-determinism due to the assignment x := ?. The recurrence property is clearly satisfied, however the number of execution steps between two occurrences of the desirable state x = 0 is unbounded. Our prototype (parameterized by intervals and ordinal-valued ranking functions) is able to prove it as, at program control point 1, it finds a ranking function defined everywhere; its value is ω+8, meaning that the number of execution steps between two occurrences of the desirable state x = 0 is unbounded but finite. ⊓ ⊔ Example 10. Let us consider the program PETERSON, Peterson's algorithm for mutual exclusion, in Figure 6. Note that weak fairness assumptions are required in order to guarantee bounded bypass (i.e., a process cannot be bypassed by any other process in entering the critical section for more than a finite number of times). Since at the moment our prototype is not able to directly analyze concurrent programs, we have modeled the algorithm as a fair non-deterministic sequential program which interleaves execution steps from both processes while enforcing 1-bounded bypass (i.e., a process cannot be bypassed by any other process in entering the critical section for more than once). Our prototype is able to prove that both processes are allowed to enter their critical section infinitely often. ⊓ ⊔

These and additional examples are available from FuncTion web interface.

Related Work

In the recent past, a large body of work has been devoted to proving liveness properties of (concurrent) programs.

A successful approach for proving liveness properties is based on a transformation from model checking of liveness properties to model checking of safety properties [START_REF] Biere | Liveness Checking as Safety Checking[END_REF]. The approach looks for and exploits lasso-shaped counterexamples. A similar search for lasso-shaped counterexamples has been used to generalize the model checking algorithm IC3 to deal with liveness properties [START_REF] Bradley | An Incremental Approach to Model Checking Progress Properties[END_REF]. However, in general, counterexamples to liveness properties in infinite-state systems are not necessarily lasso-shaped. Our approach is not counterexample-based and is meant for proving liveness properties directly, without reduction to safety properties.

In [START_REF] Podelski | Transition Predicate Abstraction and Fair Termination[END_REF], Podelski and Rybalchenko present a method for the verification of liveness properties based on transition invariants [START_REF] Podelski | Transition Invariants[END_REF]. The approach, as in [START_REF] Vardi | Verification of Concurrent Programs: The Automata-Theoretic Framework[END_REF], reduces the proof of a liveness properties to the proof of fair termination by means of a program transformation. It is at the basis of the industrial-scale tool Terminator [START_REF] Cook | Proving that Programs Eventually do Something Good[END_REF]. By contrast, our method is meant for proving liveness properties directly, without reduction to termination. Moreover, it avoids the cost of explicit checking for the well-foundedness of the transition invariants.

A distinguishing aspect of our work is the use of infinite height abstract domains, equipped with (dual) widening. We are aware of only one other such work: in [START_REF] Massé | Property Checking Driven Abstract Interpretation-Based Static Analysis[END_REF], Massé proposes a method for proving arbitrary temporal properties based on abstract domains for lower closure operators. A small analyzer is presented in [START_REF] Massé | Abstract Domains for Property Checking Driven Analysis of Temporal Properties[END_REF] but the approach remains mainly theoretical. We believe that our framework, albeit less general, is more straightforward and of practical use.

An emerging trend focuses on proving existential temporal properties (e.g., proving that there exists a particular execution trace). The most recent approaches [START_REF] Beyene | Solving Existentially Quantified Horn Clauses[END_REF][START_REF] Cook | Reasoning About Nondeterminism in Programs[END_REF] are based on counterexample-guided abstraction refinement. Our work is designed for proving universal temporal properties (i.e., valid for all program execution traces). We leave proving existential temporal properties as part of our future work.

Finally, to our knowledge, the inference of sufficient preconditions for guarantee and recurrence program properties, and the ability to provide upper bounds on the wait before a program reaches a desirable state, is unique to our work.

Conclusion and Future Work

In this paper, we have presented an abstract interpretation framework for proving guarantee and recurrence temporal properties of programs. We have systematically derived by abstract interpretation new sound static analysis methods to effectively infer sufficient preconditions for these temporal properties, and to provide upper bounds on the wait before a program reaches a desirable state.

It remains for future work to express and handle fairness properties. We also plan to extend the present framework to the full hierarchy of temporal properties [START_REF] Manna | A Hierarchy of Temporal Properties[END_REF] and more generally to arbitrary (universal and existential) liveness properties.

Fig. 1 .

 1 Fig. 1. Program SIMPLE.

Fig. 3 .

 3 Fig. 3. Example of Dual Widening.

1 c := 1 ;Fig. 4 .

 14 Fig. 4. Program COUNT-DOWN.

For simplicity, this assumption remains valid throughout the rest of the paper.

A ⇀ B is the set of partial maps from a set A to a set B.

⋆ The research leading to these results has received funding from the ARTEMIS Joint Undertaking under grant agreement no. 269335 (ARTEMIS project MBAT) (see Article II.9. of the JU Grant Agreement).


Ph F Claveau
email: fabien.claveau@mines-nantes.fr

L Chevrel

Mourad

Non-Linear Control of a Narrow Tilting Vehicle

Keywords: Narrow Tilting Vehicle (NTV), Vehicle Dynamics, Flat Systems, Non-Linear State Feedback I

Narrow Tilting Vehicles (NTVs) are the convergence of a car and a motorcycle. They are expected to be the new generation of city cars considering their practical dimensions and lower energy consumption. But considering their height to breadth ratio, in order to maintain lateral stability, NTVs should tilt when cornering. Unlike the motorcycle's case, where the driver tilts the vehicle himself, the tilting of an NTV should be automatic. Two tilting systems are available; Direct and Steering Tilt Control, the combined action of these two systems being certainly the key to improve considerably NTVs dynamic performances. Focusing on the lateral dynamic of NTVs, multivariable control strategies based on linear robust control theory, were already proposed in the literature, assuming decoupling with the longitudinal dynamic. In this paper a 4 DoF model of the main longitudinal and lateral dynamics is considered, and its differential flatness is demonstrated. The three flat outputs have furthermore a particular physical meaning, making possible the design of a simple external control loop complying with the driver demands.

INTRODUCTION

new generation of cars is currently being studied which will be more practical and efficient in relation to traffic congestion and parking problems in urban areas. These cars are small narrow commuter vehicles, hence saving energy, and are approximately half as wide as a conventional car (less than 1 m). Considering their geometry (approximately 2.5 m long, 1 m wide and 1.5 m high), these cars are characterized by a high centre of gravity, which makes roll stability an issue. To reduce this risk, they may have to lean into corners like twowheeled vehicles. Some three-and four-wheels NTV projects have already been proposed by several companies. The Ford Gyron is one of the earliest prototypes while General Motors developed the Lean Machine, with a manual lean system controlled by the driver. More recently, Brink Dynamics developed the Carver, a three-wheeled car with a rotating body but a non-tilting rear engine, while the manufacturer Lumeneo proposed the Smera. Two mechanical systems are available to tilt the vehicle [START_REF] Rajamani | Dynamics of narrow tilting vehicles[END_REF]- [START_REF] So | Active dual mode tilt control for narrow ground vehicles[END_REF]: Direct Tilt Control (DTC) and Steering Tilt Control (STC), see Fig. 1: -the DTC system is based on a dedicated actuator mounted on the longitudinal axis of the NTV, providing a torque (M t ) to tilt the vehicle. -the STC actuator requires a Steer-by-Wire system: the steering angle (δ driv ) applied by the driver is modulated by the STC system (δ c ) to control the tilt angle using countersteering. The tilting strategy is therefore directly inspired by the action of a bicycle or motorcycle rider. STC systems are not well suited for low longitudinal speeds (e.g. less than 8 m.s -1 [START_REF] So | Active dual mode tilt control for narrow ground vehicles[END_REF]), demanding a large counter-steering to tilt the vehicle, which deviates it significantly from its trajectory. In contrast, the STC system may be more efficient than the DTC one at high speed, as a large torque is required by the DTC when entering a bend if the tilting torque occurs a little late. To benefit from the complementary advantages of both systems, several projects have involved the STC and DTC systems working together [START_REF] So | Active dual mode tilt control for narrow ground vehicles[END_REF]- [START_REF] Roquiero | Sliding mode controller and flatness based set-point generator for a three wheeled narrow vehicle[END_REF].

Considering only the DTC actuator, the STC one, or both, several control strategies can be found in the literature; most of them are based on SISO control strategies such as PD / PID controllers as in [START_REF] Piyabongkarn | Active Direct Tilt Control for stability enhancement of a narrow commuter vehicle[END_REF]- [START_REF] Kidane | A fundamental investigation of tilt control systems for narrow commuter vehicles[END_REF], [START_REF] Roberston | Path following performance of narrow tilting vehicles equipped with active steering[END_REF], [START_REF] Chiou | Modeling and verification of a diamond shape narrow tilting vehicle[END_REF], tuned potentially thanks to a LQ criterion [START_REF] Piyabongkarn | Active Direct Tilt Control for stability enhancement of a narrow commuter vehicle[END_REF], but assuming a natural decoupling between the roll dynamic of the NTV and the other ones (yaw, longitudinal velocity…). Recent results proposed by Mourad et al. [START_REF] Mourad | Active lateral acceleration control of a narrow tilting vehicle[END_REF], [START_REF] Mourad | Direct and steering tilt robust control of narrow vehicles[END_REF] provide multivariable controllers to control the lateral dynamics of SDTC (STC+DTC) vehicles, design thanks to the H 2 control theory. A gain-scheduling strategy is also implemented to make the control law robust to longitudinal velocity variations. In fact, few papers take into consideration the coupling between the longitudinal and the lateral dynamics of these vehicles, and more generally the intrinsic non-linear behavior of NTVs. Considering only the roll dynamic of a DTC vehicle, Piyabongkaran et al. in [START_REF] Piyabongkarn | Active Direct Tilt Control for stability enhancement of a narrow commuter vehicle[END_REF] provide a first non-linear controller (feedback linearization), A and most recent results provided by Roquiero et al. (see e.g. [START_REF] Roquiero | Sliding mode controller and flatness based set-point generator for a three wheeled narrow vehicle[END_REF]) lead to an interesting non-linear control strategy based on sliding mode, dealing both with the roll and the longitudinal dynamic of a STC narrow vehicle.

Motivated by the fact that non-linear control strategies can potentially reach better solution than the linear ones, it is demonstrated in this paper that a 4 Degrees of Freedom, DoF, non-linear model of a SDTC narrow vehicle has flatness properties, and more precisely it can be linearized thanks to a static state feedback [START_REF] Conte | Algebraic methods for nonlinear control system[END_REF]- [START_REF] Martin | Flat systems, equivalence and trajectory generation[END_REF]. Such non-linear systems are quite interesting, as once linearized, one can implement linear control strategy on the new input / output mapping. Furthermore, flat outputs can be found, with interesting physical meanings (Huygens oscillation center [START_REF] Martin | Flat systems, equivalence and trajectory generation[END_REF], [START_REF] Martin | A different look at output tracking: control of a VTOL aircraft[END_REF]), making easier the design of the external tracking loop. This work can be seen as a generalization of results proposed by Fuchshumer et al. [START_REF] Fuchshumer | Nonlinear vehicle dynamics control -a flatness based approach[END_REF] demonstrating that the non-linear longitudinal -lateral so-called bicycle model is flat.

The paper is organized as follows: Section 2 presents the SDTC NTV 4 DoF model and the associated assumptions. Section 3 makes some reminders on the definition and the properties of flat systems, used in Section 4 to demonstrate the flatness property of the NTV model. The linearizing state feedback is defined in Section 5, as well as the external loop based on a simple trajectory generator and PI/PD controllers. Results obtained in simulation are shown in Section 6. The conclusion and perspectives are presented in Section 7.

II. 4 DOF NON-LINEAR NTV MODEL

A. 4 DoF Model of the Longitudinal-Lateral Dynamics

Several NTV models were proposed in the literature; see e.g. [START_REF] So | Active dual mode tilt control for narrow ground vehicles[END_REF], [START_REF] Roberston | Path following performance of narrow tilting vehicles equipped with active steering[END_REF]- [START_REF] Chiou | Modeling and verification of a diamond shape narrow tilting vehicle[END_REF], [START_REF] Maakaroun | Modeling and Simulation of a Two wheeled vehicle with suspensions by using Robotic Formalism[END_REF] or [START_REF] Mourad | Active lateral acceleration control of a narrow tilting vehicle[END_REF], [START_REF] Mourad | Direct and steering tilt robust control of narrow vehicles[END_REF] for a short survey of the different models. The University of Minnesota has proposed several non-linear and linear models [START_REF] Rajamani | Dynamics of narrow tilting vehicles[END_REF], [START_REF] Piyabongkarn | Active Direct Tilt Control for stability enhancement of a narrow commuter vehicle[END_REF], [START_REF] Kidane | Road bank angle considerations in modeling and tilt stability controller design for narrow commuter vehicles[END_REF], [START_REF] Kidane | A fundamental investigation of tilt control systems for narrow commuter vehicles[END_REF], in particular a 3 DoF non-linear model to study the lateral dynamics of NTVs. In this paper a 4 DoF model is proposed, based on the nonlinear 3 DoF model of the lateral dynamics of a NTV [START_REF] Rajamani | Dynamics of narrow tilting vehicles[END_REF], considering the longitudinal speed of the vehicle as a parameter of the model, and the so-called 3 DoF "bicycle" model modeling the lateral and longitudinal dynamics of the vehicle. As depicted in Fig. 2, the 4 DoF are the longitudinal and lateral position (x,y) of the vehicle, the tilt angle θ, and the yaw angle ψ. In the absolute reference (XYZ), the reference (xyz) is attached to the centre of gravity G of the vehicle, with (xy) the horizontal plane, (x) being parallel with the longitudinal axis of the vehicle. The reference (x'y'z') is also attached to the centre of gravity, but leans with the chassis, i.e. (x) and (x') are the same. The reference (x v y v z v ) is also linked to G, but the axis (x v ) is collinear to the longitudinal speed of the vehicle v, and (z v ) is collinear to (Z). The 4 DoF model was build under the following assumptions: 1-the vehicle is considered a mass point at its centre of gravity; 2-vertical reaction forces on the right and left wheels are considered identical; 3-gyroscopic effects due to the rotation of the wheels and road bank angle are neglected; 4-many mechanical parts that would have an impact on the vehicle's dynamics are not represented (e.g. dampers). Nevertheless, this simplified model can still be used for control, as long as the control law has some robustness. All this leads to the non-linear model ( )

, x f x u = , with the state vector T x v β ψ θ θ ⎡ ⎤ = ⎣
⎦ , and the control input signals

[ ] T l t u F M δ = 2 2 1 ( sin( ) cos( ) sin( ) cos( )) ( cos sin ) sin 1 ( cos( ) sin( ) cos( ) sin( )) 1 ( cos sin )cos
( cos sin ) sf lf sr lr sf lf sr lr f r sf lf s v F F F F m h h r F F F F mv h h v l l r F F F J J θ θ θ θ β ψ δ δ - = -+ + + - - = -+ -- -+ - - - = = + 2 2 2 2
( cos sin ( cos sin ) cos sin )

( s i n ) r sf l f s r s t x mh F F F h hF M ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ - - + + + + ⎪ = ⎪ + ⎩ (1)
All the signals and parameters are defined in Table 1.

lr l F F γ = , ( )
1 lf l F F γ = - , [ ] 0,1 γ ∈
meaning that the motor or braking force can be supplied to the front and the rear wheel with a given transmission ratio (all-wheel driven vehicle). γ is assumed to be a constant value in this paper, to fit with the reality of NTVs (most being characterized by the ratio γ = 1).

The other control inputs are the steering angle of the front wheel δ and the tilting torque M t , i.e. the NTV is equipped of both a DTC and STC system.

B. Rear and Front Lateral Tire Forces

Several models of the lateral tire forces F sf and F sr can be found in the literature, see e.g. [START_REF] Bakker | A new tire model with an application in vehicle dynamics studies[END_REF]. One common assumption is that these lateral tire forces can be expressed as functions of the side-slip angles α f and α r of the wheels:

1 1 sin sin tan , tan cos cos f r f r v l v l v v β ψ β ψ α δ α β β - - + ⎛ ⎞ - ⎛ ⎞ = - = - ⎜ ⎟ ⎜ ⎟ ⎝ ⎠ ⎝ ⎠ (2)
and also of the tilt angle θ of the vehicle through the camber stiffness of the tires. Considering the small angle approximation tan φ ≈ φ, the lateral tire forces models are, ( )

( ) sin , , , 2 2 , cos sin
, , 2 2 .

cos

f sf f f r sr r r v l F v r C v v l F v r C v β ψ δ β δ λ θ β β ψ β λ θ β ⎧ + ⎛ ⎞ = - + ⎪ ⎜ ⎟ ⎪ ⎝ ⎠ ⎨ - ⎛ ⎞ ⎪ = + ⎜ ⎟ ⎪ ⎝ ⎠ ⎩ (3)
Notice however that, as suggested in [START_REF] Fuchshumer | Nonlinear vehicle dynamics control -a flatness based approach[END_REF], in the flatness analysis of the non-linear model ( 1)-( 3), the detailed expression of the lateral tire forces F sf (δ,v,β,r) and F sr (v,β,r) are not necessary. Assuming them as smooth functions is a sufficient technical condition to make easier the mathematical manipulations.

C. Control Objectives in Terms of Lateral Stability of NTVs

As said in the introduction, the objective is to ensure the lateral stability of the NTV faced with lateral acceleration when cornering, by tilting its chassis thanks to the DTC and STC systems. In particular, the lateral acceleration at the center of gravity G is of importance. Definition 1: Perceived acceleration a per a per denotes the resultant acceleration at the center of gravity G, along the axis (y') (cf. Fig. 2), i.e. perpendicular to the chassis of the vehicle. It is linked to other variables by: ( )

cos sin cos sin per lat a a h g y V h g θ θ θ ψ θ θ θ = + - = + + - (4)
The terminology "perceived" (or measured) acceleration was introduced in [START_REF] Rajamani | Dynamics of narrow tilting vehicles[END_REF]. This would be the acceleration measured by an accelerometer positioned at the center of gravity whose lateral axis is in the lateral vehicle direction, and also the lateral acceleration perceived by the driver in the cabin of the vehicle, impacting the comfort. Fundamentally, the lateral stability of the NTV is ensured if a per = 0. To reach this objective, the literature classically reformulates the lateral control problem as an angular position tracking problem, regulating the tilting angle θ around the reference angle θ ref , estimated on line by inverting equation (4) (with more or fewer approximations) [3]- [START_REF] Hibbard | Twenty first century transportation system solutions-A new type of small, relatively tall and narrow active tilting commuter vehicle[END_REF], [START_REF] Berote | Dynamics and control of a tilting three wheeled vehicle[END_REF]- [START_REF] Chiou | Modeling and verification of a diamond shape narrow tilting vehicle[END_REF]. There are pros and cons for such control strategy as discussed in [START_REF] Mourad | Direct and steering tilt robust control of narrow vehicles[END_REF], compared to the direct regulation of a per as proposed by the authors e.g. in [START_REF] Mourad | Active lateral acceleration control of a narrow tilting vehicle[END_REF], [START_REF] Mourad | Direct and steering tilt robust control of narrow vehicles[END_REF]. As it will be detailed in Section 5, the tilt angle control strategy will be applied in this paper, to be consistent with the physical meaning of the chosen flat outputs. Concretely, our fundamental control objective is defined by the following equation

1 cos tan 0 ref rv g β θ θ θ -⎛ ⎞ - = - = ⎜ ⎟ ⎝ ⎠ . ( 5
)
The other control objectives will be to ensure the trajectory planning and regulation to satisfy the driver's desires, express through the throttle/brake pedal, traduced as a desired longitudinal traction force F l-driv , and the steering wheel angle δ driv . A first simple solution is also provided in Section 5.

D.

Available Measurements Practically, tilting cars generally include a tilt angle sensor and an Inertial Measurement Unit (IMU), which provide the state values v, θ, θ , ψ and a per . Lastly, the steering angle δ and its derivative are assumed to be can be measured, and the side-slip angle β available through an estimator (e.g. [START_REF] Stephant | Virtual sensor, application to vehicle sideslip angle and transversal forces[END_REF]).

III. FLATNESS PROPERTY AND STATIC STATE FEEDBACK LINEARIZATION

A. Flatness property

The main objective in this paper is to demonstrate, in the same spirit as in [START_REF] Fuchshumer | Nonlinear vehicle dynamics control -a flatness based approach[END_REF], that the longitudinal / lateral 4 DoF model of a NTV equipped with a SDTC system can be linearized by a static non-linear state feedback. To prove such a result, 3 flat outputs associated to the 3 control inputs, will be first exhibited. To begin with, some reminders about the flatness property are proposed hereafter.

Definition 1: Flat system [START_REF] Fliess | Flatness and defect of nonlinear systems: introductory theory and examples[END_REF] Consider a non-linear system ( )

, x f x u = , n x ∈ , m u ∈ .
Such system is said to be a "flat system", if and only if one can find:

an output vector ( )

n m r m R R R + Π × → , with rank m, o : ( ) m r n R R Ω → , with rank n, o 1 : ( ) m r m R R + Ξ → ,
⎧ = = Π ⎪ ⎨ = Ω = Ξ ⎪ ⎩ (6)
In fact, a system verifying the flatness property is such that all its state and input signals can be expressed as functions of some specific output signals hence named flat outputs. In other words, these outputs "sum up" all the dynamic characteristics of the system.

Definition 2: Relative degree Consider a non-linear system

( ) ( ) ( ) ( ) ( ) 1 1 , , , , m m x f x u x f x u y h x y h x y h x ⎧ = ⎧ = ⎪ ⎪ ⇔ ⎨ ⎨ = = = ⎪ ⎪ ⎩ ⎩ … (7)
0 i r i y u ∂ ≠ ∂
is the relative degree of the output y i .

Property 1: Flat outputs Consider the non-linear system [START_REF] Hibbard | Twenty first century transportation system solutions-A new type of small, relatively tall and narrow active tilting commuter vehicle[END_REF]. If one can find a change of coordinates ( )

z x = Φ such that: - ( ) . Φ
is a diffeomorphism, and the new state n z ∈ is composed of the m outputs y i and their derivatives until the (r i -1) degree, i.e.

( ) ( )

1 1 1 1 1 1 m T r r m m m z y y y y y y - - ⎡ ⎤ = ⎣ ⎦ , (8)
-the decoupling matrix M is full rank, rank(M) = m, ( )

1 , 1 j r j i i m j m y M u ≤ ≤ ≤ ≤ ⎡ ⎤ ∂ ⎢ ⎥ = ∂ ⎢ ⎥ ⎣ ⎦ (9)
then ouputs y i are flat outputs of the system. , defined as the solution of

B. Input / State

( ) ( ) ( ) ( ) ( ) ( )
⎧ = ⎪ = ⎪ ⎨ ⎪ ⎪ = ⎩ (10)
such that the closed-loop is equivalent to the linear time invariant system [START_REF] Berote | Dynamics and control of a tilting three wheeled vehicle[END_REF] based on m chains of integrators

1 2 1 1 1 2 2 1 1 2 1 1 1 1 1 1 2 2 1 1 1 1 1 1 2 1 1 0 0 0 0 0 0 0 0 0 0 0 0 m m m m z rr rr z r r r z r r z m m r z r r z z r r r z m m r z A B B A z z B A C y C z y C ω × × × × × × × × × × × × ⎧ ⎡ ⎤ ⎡ ⎤ ⎪ ⎢ ⎥ ⎢ ⎥ ⎪ ⎢ ⎥ ⎢ ⎥ = + ⎪ ⎢ ⎥ ⎢ ⎥ ⎪ ⎢ ⎥ ⎢ ⎥ ⎪ ⎢ ⎥ ⎢ ⎥ ⎪ ⎣ ⎦ ⎣ ⎦ ⎨ ⎡ ⎤ ⎪ ⎢ ⎥ ⎡ ⎤ ⎪ ⎢ ⎥ ⎢ ⎥ ⎪ = ⎢ ⎥ ⎢ ⎥ ⎪ ⎢ ⎥ ⎢ ⎥ ⎪ ⎣ ⎦ ⎢ ⎥ ⎪ ⎣ ⎦ ⎩ (11) with matrices i z A , i z B , i z C of dimensions i i r r × , 1 i r × , 1 i r × , ( ) ( ) 0 1 0 0 1 0 0 i z A ⎡ ⎤ ⎢ ⎥ ⎢ ⎥ = ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ , 0 0 1 i z B ⎡ ⎤ ⎢ ⎥ ⎢ ⎥ = ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ , [ ]
1 0 0 i z C = .

IV. FLATNESS PROPERTY OF THE NTV MODEL

Considering the previous definitions and properties, some flat outputs are proposed in this section, demonstrating that the 4 DoF model of NTVs in (1) can be linearized, under few assumptions, thanks to a static state feedback.

A. Main Results

Proposition 1 Let's consider that the lateral tire forces F sf (δ,v,β,r) and F sr (v,β,r) are arbitrary smooth functions. Let's define the smooth function

( ) ( ) ( ) 2 ( , , ) ( , , , , cos , , sin ) cos f r r sr sr f f v sr f l l J T v r v F v r F v r ml ml J v F v r v ml β β β β β β β β + = ∂ + ∂ + ∂ - (12)
with the notation

F F ω ω ∂ ∂ = ∂ .
Then under the conditions T(v,β,r) ≠ 0, v ≠ 0, the non-linear system (1) is differentially flat. Furthermore, this system is exact input / state linearizable via a static feedback. In particular, the 3 outputs ( 13) are available flat outputs with relative degrees (1,2,2).

⎡ ⎤ ⎢ ⎥ ⎡ ⎤ ⎡ ⎤ ⎢ ⎥ ⎢ ⎥ - + ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ + ⎢ ⎥ ⎢ ⎥ = Φ ⇔ = = = ⎢ ⎥ - ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎢ ⎥ ⎢ ⎥ ⎣ ⎦ ⎢ ⎥ ⎣ ⎦ . (14) ( ) x Φ is a diffeomorphism as long as det(J) ≠ 0, 1 , 1 ( ) i i n j j n x J x ≤ ≤ ≤ ≤ ⎡ ⎤ ∂Φ = ⎢ ⎥ ∂ ⎣ ⎦
. This is equivalent to the condition T(v,β,r) ≠ 0. Moreover, the decoupling matrix

δ Μ δ Μ δ Μ ⎛ ⎞ ∂ ∂ ∂ ⎜ ⎟ = ∂ ∂ ∂ ⎜ ⎟ ⎜ ⎟ ⎜ ⎟ ∂ ∂ ∂ ⎝ ⎠ (15)
remains of full rank for T(v,β,r) ≠ 0 and v ≠ 0. This proves the flatness of y (13) (see Property 1).

B. Physical Meaning of the Proposed Flat Outputs

The chosen flat outputs in [START_REF] Chiou | Modeling and verification of a diamond shape narrow tilting vehicle[END_REF] have some physical meaning of interest to build the external tracking loop. Defining the point G', projection on the vehicle's longitudinal axis of the center of gravity G along the axis (z'), we define in Fig. 3 the new reference (x s y s z s ) linked to G': it is the translation of reference (xyz) in Fig. 2 from G to G'. Let's define the specific points ( )

/ ,0,0 f J lm Σ - and ( ) ' / , sin , cos f J ml h h θ θ
∑in this reference (x s y s z s ). Considering this new reference and the two specific points Σ and Σ', one can observe that: y 1 is the longitudinal speed of any point located on the vehicle's longitudinal axis (x s ), y 2 is the lateral speed of Σ' in (x s y s z s ), y 3 is the tilting angle of the vehicle.

Remark: Huyghens center of oscillation

As in [START_REF] Fuchshumer | Nonlinear vehicle dynamics control -a flatness based approach[END_REF], the specific point Σ' can be linked to the Huyghens center of oscillation, define in a general manner for Lagrangian systems underactuated by one control, such as the PVTOL position control in [START_REF] Martin | A different look at output tracking: control of a VTOL aircraft[END_REF]. V.

CONTROL DESIGN

A. Design of the static state linearizing feedback According to Property 2, the 4 DoF NTV model controlled by the ad hoc non-linear feedback depicted in Fig. 4 is equivalent to the linear one defined by equations ( 10), [START_REF] Berote | Dynamics and control of a tilting three wheeled vehicle[END_REF], under restriction [START_REF] Roquiero | Sliding mode controller and flatness based set-point generator for a three wheeled narrow vehicle[END_REF]. The analytic expression not presented here by lack of place, is available however in [START_REF] Mourad | Active lateral acceleration control of a narrow tilting vehicle[END_REF]-prop. 6.3.

state feedback t M δ l F x ⇔ 1 y 3 y 2 y ( , ) x f x u = 1 ω 2 ω 3 ω 1 y 3 y 2 y ∫ ∫ ∫ ∫ ∫ 1 ω 2 ω 3 ω Fig. 4. Equivalent closed-loop system

B. Design of the tracking controller and trajectory generation

Finally, we have to regulate y (see equation ( 13)) around some trajectories that 1/ ensure the lateral stability of the vehicle, 2/ interpret and satisfy the driver's desires. His demand is made through the steering wheel angle and the throttle / break pedal. This is still partly an open research topic. δ driv the steering wheel angle reference, and F l-driv the required longitudinal force are considered here as the new input left at the disposal of the driver. Fig. 5 depicts the solution proposed at this first stage, involving the three reference signals: Three PD controllers are implemented to drive the error signals

F y v v v m F y v v v m rv y g δ δ δ δ β θ - - - - - ⎧ ⎛ ⎞ ⎪ ⎜ ⎟ = = = + ⎜ ⎟ ⎪ ⎝ ⎠ ⎪ ⎪ ⎛ ⎞ ⎪ ⎜ ⎟ = = = + ⎨ ⎜ ⎟ ⎪ ⎝ ⎠ ⎪ ⎛ ⎞ ⎪ = = ⎜ ⎟ ⎪ ⎝ ⎠ ⎪ ⎩ ∫ ∫ (
d i i i
e y y = -, i = 1,2,3. A PI is also used to generate the control signal ω 2, to control the error signal e δ = δδ driv .

Finally, it leads to, ( )

( ) 2 2 2
, 1,3

P D i i i i I P D P i K K s e i K K K s e K e s δ δ δ ω ω ⎧ = + = ⎪ ⎪ ⎨ ⎛ ⎞ = + + + ⎪ ⎜ ⎟ ⎜ ⎟ ⎪ ⎝ ⎠ ⎩ (17)

VI. RESULTS

The performances of the proposed control strategy are now evaluated by simulating the non-linear model [START_REF] Rajamani | Dynamics of narrow tilting vehicles[END_REF]. The scenario is defined as follows: the driver requires a constant acceleration (F l-driv assumed to be constant), and the steering wheel angle δ driv (see Fig. 6) entails a first bend followed by a circular trajectory (medium sized roundabout). This trajectory is quite difficult compared to the ones proposed e.g. in [START_REF] Piyabongkarn | Active Direct Tilt Control for stability enhancement of a narrow commuter vehicle[END_REF] or [START_REF] Hibbard | Twenty first century transportation system solutions-A new type of small, relatively tall and narrow active tilting commuter vehicle[END_REF]. The PDs and PI controllers considered were tuned to:

-PD 1 : . The simulation results are compared with the ones obtained with the LPV controller proposed in [START_REF] Mourad | Direct and steering tilt robust control of narrow vehicles[END_REF], designed by solving a H 2 control problem based on the linearized model of the lateral dynamic of the NTV, considering as controlled output the lateral acceleration a per , and made robust to the longitudinal velocity variation thanks to a gain-scheduling solution. Fig. 6 firstly shows that the gap between the desired steering angle δ driv and the one applied by the non-linear controller δ through the STC system is not intrusive.

Considering the traction force, F l is identical to the desired one F l-driv in a straight trajectory, but is reduced in bend, so as to ensure a better trajectory tracking. Even if it can be seen as a driving assistance, such behavior can be disturbing for the driver and should be studied in more depth in the future. However, results in Fig. 7 and Fig. 8 show that the proposed non-linear control strategy associated to the rudimentary trajectory generation system [START_REF] Martin | Flat systems, equivalence and trajectory generation[END_REF] ensures the lateral stability of the vehicle: in particular, the perceived acceleration a per reaches acceptable values (max. 0.6 m/s²), compared to most of the results in the literature. The LPV controller still reaches better performances, with a tilting torque M t divided by a factor 2 and a lateral acceleration a per 3 times smaller. However we are convinced that a more sophisticated external loop should improve the performances.

VII. CONCLUSION AND PERSPECTIVES

Based on a 4 DoF model of a Narrow Tilting Vehicle equipped both of a DTC and STC system, inspired from the well-known bicycle model and the 3 DoF model of the lateral dynamic of NTVs [START_REF] Rajamani | Dynamics of narrow tilting vehicles[END_REF], we showed that NTVs verify the differential flatness property. Furthermore, they present some interesting characteristics. First, based on few assumptions on the tire forces model, the longitudinal-lateral dynamics of NTV can be linearized thanks to a static state feedback. Secondly, three flat outputs with a concrete physical meaning associated to the Huyghens oscillation center, can be defined. To validate the proposed linearizing feedback, a first control strategy based on a rudimentary trajectory generation system and PD/PI control loops was also proposed. It has been demonstrated that such simple external loops already reach quite satisfactory performance.

These first results call for some motivating perspectives: a classic state feedback was design here, leading to three decoupled integrator chains. Such strategy has the weakness to "erase" the original dynamics of the system. We believe that methods inspired by [START_REF] Franco | Robust feedback linearization without full state information[END_REF] will bring more robustness; a linearizing feedback leading to a closed-loop system sharing structural properties with the tangent linear models of the original system. On this basis, we then plan to make use of the optimal control strategy proposed in [START_REF] Mourad | Direct and steering tilt robust control of narrow vehicles[END_REF] for the external loop synthesis, thus bypassing the gain-scheduling design step while getting an improved performance.

Fig. 1 .

 1 Fig. 1. Tilting actuators: DTC (left) and STC (right) systems

Fig. 2 .

 2 Fig. 2. Four DoF of the tilting vehicle: top view (left) and rear view (right)

  Proof: see[START_REF] Mourad | Active lateral acceleration control of a narrow tilting vehicle[END_REF]-chap.6 for the detailed proof. At first, the relative degree of the 3 outputs y 1 , y 2 , y 3 can be easily verified by computing derivatives ( )

Fig. 3 .

 3 Fig. 3. Top view (left) and Front view (right) of the vehicle: definition of the point Σ' ( ) / , sin , cos f J ml h h θ θ

16 )

 16 The two first reference signals make possible the control of the lateral and longitudinal speeds. The third is the tilting reference θ ref , classically computed as proposed in the literature about NTVs (see subsection II.C).

Fig. 5 .

 5 Fig. 5. Trajectory generation tracking applied to each decoupled wi→yi.

Fig. 6 .

 6 Fig. 6. Longitudinal velocity of the NTV (Non-Linear and LPV solution), steering, desired steering angle δdriv and traction force Fl-driv, and the ones calculated by the complete non-linear controller, δ , Fl.

Fig. 7 .

 7 Fig. 7. Tilting angle, tilting torque of the DTC system, and lateral perceived acceleration obtained by the non-linear (NL) and the LPV controller.

Fig. 8 .

 8 Fig. 8. NTV Trajectory considering the non-linear (NL) controller and the LPV one.

Table 1 .

 1 Parameters of The 3 DoF Model: See[START_REF] Rajamani | Dynamics of narrow tilting vehicles[END_REF],[START_REF] Mourad | Active lateral acceleration control of a narrow tilting vehicle[END_REF] For Numerical Values

		v			longitudinal speed of the vehicle	g	gravitational constant
		β		side-slip deviation angle	m	total mass
	ψ	, r	=	ψ	yaw angle and speed	h	position of the center of gravity G on the z' axis
		, θ θ		tilt angle and speed	Iz	vehicle yaw moment of inertia
		Mt		tilting torque provided by the DTC actuator	Ix	vehicle roll moment of inertia
		δ		steering angle of the front wheels	lf	distance from center of gravity to front axle
		Fl		global longitudinal force	lr	distance from center of gravity to rear axle
		αf, αr	front and rear tire side-slip angle	Cf, Cr	front and rear cornering stiffness
	Flf, Flr	front and rear longitudinal force	λf, λr	front and rear camber stiffness
	Fsf, Fsr	front and rear lateral force

  with rank m, such as one can write:

	y	1 ( , ,..., ) 2 m y y y		( , , ,..., x u u u	( ) r	),
	x	( , ,..., y y	y	( 1) r -	),	u	( , ,..., y y	y	( ) r	).

ACKNOWLEDGMENT

The authors wish to thank C. H. Moog for the fruitful discussions we had together.