Adnane Saoud

Antoine Girard

Laurent Fribourg

Contract Based Design of Symbolic Controllers for Interconnected Multiperiodic Sampled-Data Systems*

This paper deals with the synthesis of symbolic controllers for interconnected sampled-data systems where each component has its own sampling period. A compositional approach based on continuous-time assume-guarantee contracts is used. We provide sufficient conditions guaranteeing for a sampled-data system, satisfaction of an assume-guarantee contract and completeness of trajectories. Then, compositional results can be used to reason about interconnection of multiperiodic sampled-data systems. We then show how discrete abstractions and symbolic control techniques can be applied to enforce the satisfaction of contracts and ensure completeness of trajectories. Finally, theoretical results are applied to a vehicle platooning problem on a circular road, which show the effectiveness of our approach.

I. INTRODUCTION

The use of symbolic models for the control of continuous and hybrid systems has attracted considerable attention in the past decade (see [START_REF] Tabuada | Verification and control of hybrid systems: a symbolic approach[END_REF] and the references therein). A symbolic model (also called discrete abstraction) is a dynamical system with a finite number of states and related to the original system by some formal behavioral relationship (e.g. simulation, bisimulation and their alternating/approximate versions), which makes it possible to refine a symbolic controller, designed for the abstraction, into a concrete one that can be used on the original system. Symbolic controllers can be synthesized using techniques developed in the areas of supervisory control of discrete event systems [START_REF] Cassandras | Introduction to discrete event systems[END_REF] and algorithmic game theory [START_REF] Bloem | Synthesis of reactive (1) designs[END_REF]. Symbolic models are often obtained through discretization of the state-space and of the time (if the original system is continuous-time), see e.g. [START_REF] Girard | Approximately bisimilar symbolic models for incrementally stable switched systems[END_REF], [START_REF] Reißig | Computing abstractions of nonlinear systems[END_REF].

Due to discretization of the state-space, these abstraction techniques suffer from the curse of dimensionality (the number of symbolic states increases exponentially with respect to the state-space dimension). For large systems made of interconnected components, a way to tackle the lack of scalability is to develop compositional methods for abstraction or symbolic controller synthesis (see e.g. [START_REF] Tazaki | Bisimilar finite abstractions of interconnected systems[END_REF], [START_REF] Dallal | On compositional symbolic controller synthesis inspired by small-gain theorems[END_REF], [START_REF] Kim | Compositional controller synthesis for vehicular traffic networks[END_REF], [START_REF] Le Coënt | Distributed synthesis of state-dependent switching control[END_REF], [START_REF] Pola | Symbolic models for networks of control systems[END_REF], [START_REF] Meyer | Compositional abstraction and safety synthesis using overlapping symbolic models[END_REF], [START_REF] Saoud | Compositional abstraction-based synthesis for cascade discrete-time control systems[END_REF]). The authors in [START_REF] Tazaki | Bisimilar finite abstractions of interconnected systems[END_REF] proposed a compositional abstraction based on the notion of interconnectioncompatible approximate bisimulation. In [START_REF] Mallik | Compositional abstraction-based controller synthesis for continuous-time systems[END_REF], the notion of *This work has been supported by Labex DigiCosme (project ANR-11-LABEX-0045-DIGICOSME) operated by ANR as part of the program "Investissement d'Avenir" Idex Paris Saclay (ANR-11-IDEX-0003-02). (approximate) disturbance simulation was used for compositional abstraction of continuous-time systems, where the states of the neighbouring components were modeled as disturbance signals. The results in [START_REF] Pola | Symbolic models for networks of control systems[END_REF] provide compositional constructions of approximately bisimilar finite abstractions for networks of discrete-time control systems under some incremental stability properties and using a small-gain type conditions.The authors in ( [START_REF] Dallal | On compositional symbolic controller synthesis inspired by small-gain theorems[END_REF], [START_REF] Le Coënt | Distributed synthesis of state-dependent switching control[END_REF], and [START_REF] Meyer | Compositional abstraction and safety synthesis using overlapping symbolic models[END_REF]) use assumeguarantee reasoning and contract based design to provide compositional synthesis.

Existing approaches assume that sampling periods of all components are equal. In this paper, we use a compositional approach to symbolic controller synthesis, based on continuous-time assume-guarantee contracts [START_REF] Benveniste | Contracts for systems design: Theory[END_REF], which makes it possible to reason on the interconnection of sampled-data systems (such as those synthesized using symbolic control techniques) where we have different components with different sampling periods (multiperiodic sampling). We rely on a notion of strong satisfaction of such assume-guarantee contracts introduced in [START_REF] Saoud | On the composition of discrete and continuous-time assume-guarantee contracts for invariance[END_REF], which allows us to deal with cascade and feedback compositions. We first provide a simple criteria for a sampled-data system to strongly satisfy an assume-guarantee contract and ensure the completeness of maximal trajectories. We then show how symbolic control techniques can be applied to enforce those criteria. We illustrate our approach with several numerical experiments on a vehicle platooning problem [START_REF] Ioannou | Autonomous intelligent cruise control[END_REF].

The paper is organized as follows. In Section II, we briefly present the general framework introduced in [START_REF] Saoud | On the composition of discrete and continuous-time assume-guarantee contracts for invariance[END_REF], for compositional reasoning using assume-guarantee contracts. Then, we instantiate this framework to reason about multiperiodic interconnections of sampled-data systems. In Section III we show how symbolic control techniques can be used to enforce the specified assume-guarantee contracts and ensure completeness of trajectories. In Section IV, we apply the theoretical framework to a vehicle platooning problem. The proofs for the lemmas, propositions and theorems can be found in the appendix.

Notations: R, R + 0 , R + denote the set or reals, nonnegative reals and positive reals respectively. The set of continuous-time domains is

I(R + 0 ) = {[0, a], a ∈ R + 0 } ∪ {[0, a), a ∈ R + } ∪ {R + 0 }. For I ∈ I(R + 0
) and a metric space X, C(I, X) denote the set of continuous functions from I to X. N denote the set of nonnegative integers. Given two sets A and B, a set-valued map f : A ⇒ B is a map from A to the set of subsets of B, its domain is

dom(f ) = {a ∈ A| f (a) = ∅}. For x ∈ R n , x denotes the Euclidean norm of x. For ε ∈ R + , A ⊆ R n the ε-expansion of A is B ε (A) = {y ∈ R n | ∃x ∈ A, x -y ≤ ε}.

II. CONTRACTS FOR SAMPLED-DATA SYSTEMS A. Systems and contracts

In this paper, we deal with sampled-data systems consisting of continuous-time systems with periodic controllers. In this section, we present a broader class of systems and associated assume-guarantee contracts, introduced in [START_REF] Saoud | On the composition of discrete and continuous-time assume-guarantee contracts for invariance[END_REF], which will allow us to reason on interconnection of sampleddata systems, even when components have different sampling periods. The results are stated without proofs, which can be found in [START_REF] Saoud | On the composition of discrete and continuous-time assume-guarantee contracts for invariance[END_REF].

1) Systems and interconnections: Definition 1: A system is a tuple Σ = (W, X, Y, T ) where

• W ⊆ R m , X ⊆ R n and Y ⊆ R p
, are the sets of external inputs, states, and outputs; • T is a set of trajectories (w, x, y) :

I → W × X × Y
where I ∈ I(R + 0 ) and y ∈ C(I, Y ). Given two trajectories (w, x, y) : (w,x,y) is said to be a prefix of (w , x , y ) if I ⊆ I and for all t ∈ I, w(t) = w (t), x(t) = x (t) and y(t) = y (t). A trajectory (w, x, y) ∈ T is said to be maximal if there does not exist any trajectory (w , x , y ) ∈ T such that (w , x , y ) = (w, x, y) and (w, x, y) is a prefix of (w , x , y ). A trajectory (w, x, y) :

I → W × X × Y and (w , x , y ) : I → W × X × Y in T ,
I → W × X × Y in T is said to be complete if I = R + 0 .
We consider elementary interconnections of systems that can be described using cascade and feedback compositions and formally defined as follows.

Definition 2:

Let Σ 1 = (W 1 , X 1 , Y 1 , T 1 ) and Σ 2 = (W 2 , X 2 , Y 2 , T 2 ) be two systems, with Y 1 ⊆ W 2 . The cascade composition of Σ 1 and Σ 2 is the system Σ 1 || c Σ 2 = (W 1 , X 1 × X 2 , Y 2 , T c ), such that (w 1 , (x 1 , x 2 ), y 2 ) : I → W 1 × (X 1 × X 2 ) × Y 2 belongs to T c if and only if there exist (w 1 , x 1 , y 1 ) : I 1 → W 1 × X 1 × Y 1 in T 1 , and (w 2 , x 2 , y 2 ) : I 2 → W 2 ×X 2 ×Y 2 in T 2 such that I = I 1 ∩I 2
and for all t ∈ I, y 1 (t) = w 2 (t). Definition 3: Let Σ = (W, X, Y, T ) be a system with Y ⊆ W . The feedback composition of Σ is the system Σ f = ({0}, X, {0}, T f ), such that (0, x, 0) : I → {0} × X × {0} belongs to T f if and only if there exists (w, x, y) :

I → W × X × Y in T such that y = w.
Note that systems obtained by feedback composition have trivial null inputs and outputs. Hence, with an abuse of notation, we will denote Σ f = (X, T f ) and x ∈ T f , with x : I → X. Other system interconnections considered in this paper are defined using cascade and feedback compositions as shown in Figure 1.

2) Assume-guarantee contracts: Contracts make it possible to reason about the interconnection of systems based on properties of its components [START_REF] Benveniste | Contracts for systems design: Theory[END_REF]. In this paper, we consider the following type of contracts: Definition 4: Let Σ = (W, X, Y, T ) be a system, an assume-guarantee contract for Σ is a tuple C = (A W , G X , G Y ) where:

Σ 1 Σ 2 Σ 1 || c Σ 2 y 1 = w 2 w 1 y 2 Σ Σ f y = w Σ 1 Σ 2 y 1 = w 2 Σ 3 y 2 = w 3 y 3 = w 1 (Σ 1 || c Σ 2 || c Σ 3 ) f
Fig. 1. Cascade, feedback compositions and an example of interconnection of systems

• A W ⊆ W is a set of assumptions; • G X ⊆ X and G Y ⊆ Y are sets of guarantees, where G Y is closed.
We say that Σ strongly satisfies contract C, denoted Σ |= s C if for all trajectories (w, x, y) :

I → W × X × Y in T : • y(0) ∈ G Y ; • for all t ∈ I, such that for all s ∈ [0, t], w(s) ∈ A W , we have -for all s ∈ [0, t], x(s) ∈ G X ; -there exists δ > 0, such that for all s ∈ [0, t+δ]∩I, y(s) ∈ G Y .
An assume-guarantee contract states that if the system's input belongs to A W up to a time instant t, then the system's state belongs to G X at least until t, and the system's output belongs to G Y until t + δ with δ > 0 (or δ = 0 in case of weak satisfaction, see [START_REF] Saoud | On the composition of discrete and continuous-time assume-guarantee contracts for invariance[END_REF]).

3) Compositional reasoning: We now provide results allowing to reason about cascade and feedback compositions of systems:

Theorem 1 (Contracts under cascade composition):

Let Σ i = (W i , X i , Y i , T i ), i = 1, 2 be systems with Y 1 ⊆ W 2 . Let C i = (A Wi , G Xi , G Yi ) be assume-guarantee contracts for Σ i , i = 1, 2 with G Y1 ⊆ A W2 , and let C c = (A W1 , G X1 × G X2 , G Y2 ). If Σ 1 |= s C 1 and Σ 2 |= s C 2 , then Σ 1 || c Σ 2 |= s C c . Theorem 2 (Contracts under feedback composition): Let Σ = (W, X, Y, T ) be a system with Y ⊆ W and let Σ f = (X, T f ). Let C = (A W , G X , G Y ) be an assume- guarantee contract for Σ with G Y ⊆ A W . If Σ |= s C then, for all trajectories x : I → X in T f , we have for all t ∈ I, x(t) ∈ G X .
Remark 1: While weak satisfaction of assume-guarantee contracts is sufficient to reason about cascade composition, strong satisfaction as given in Definition 4 is critical to reason about feedback composition.

B. Sampled-data systems

In this section, we introduce the class of sampled-data systems and show that these can be embedded in the framework presented above. We then provide sufficient conditions for

ẋ = f (x, u, w) u k ∈ g(x(τ k )) sampler ZOH u w x Σ y = h(x) y
Fig. 2. Sampled-data system sampled-data systems to satisfy assume-guarantee contracts and ensure completeness of maximal trajectories. Definition 5: A sampled-data system is a tuple Σ = (W, X, Y, U, f, g, h, τ ) where

• W ⊆ R m , X ⊆ R n and Y ⊆ R p ,
are the sets of external inputs, states, and outputs;

• U ⊆ R q is the set of internal inputs; • f : X × U × W → R n is a map, g : X ⇒ U is a set valued-map, and h : X → Y is a continuous map; • τ ∈ R + is the sampling period.
A pictural representation of a sampled-data system is shown in Figure 2. In this paper, we make the following assumption:

Assumption 1: For all x 0 ∈ dom(g), u ∈ g(x 0 ), w ∈ C([0, τ ], W ), there exists a unique solution x : [0, τ ] → X to the differential equation: ẋ(t) = f (x(t), u, w(t)), x(0) = x 0 . (1)
We use the notation x = χ(., x 0 , u, w) to denote to the solution of (1).

Let us remark that f need not be continuous, so we consider solutions of differential equations in the Caratheodory sense (see e.g. [START_REF] Filippov | Differential Equations with Discontinuous Righthand Sides[END_REF]).

The sequence of sampling instants (τ k ) k∈N is given by τ k = kτ , for k ∈ N. The initial sampling instant τ 0 coincides with the initial time 0. Sampled-data systems can be seen as systems in the sense of Definition 1 where a trajectory in T is a triple (w, x, y) : I → W ×X ×Y , where I = [0, τ l+1 ] with l ∈ N or l = +∞ (then I = R + 0 ), w and y are continuous, x is absolutely continuous, and for all k ∈ N with k ≤ l, x(τ k ) ∈ dom(g), and there exists

u k ∈ g(x(τ k )) such that ẋ(t) = f (x(t), u k , w(t)), for almost all t ∈ [τ k , τ k+1 ] y(t) = h(x(t)), for all t ∈ [τ k , τ k+1 ]
Let us remark that in particular, x(0) = x(τ 0 ) ∈ dom(g). Assumption 1 guarantees that trajectories of Σ are welldefined between the sampling instants: given x(τ k ) ∈ dom(g), u k ∈ g(x(τ k )), and values of w on [τ k , τ k+1 ], x and y can be defined on [τ k , τ k+1 ]. Then, it follows that maximal trajectories of Σ are either complete (i.e. l = +∞) or incomplete (i.e. l ∈ N) with x(τ l+1 ) / ∈ dom(g). Cascade and feedback composition of sampled systems are defined according to Definitions 2 and 3. Let us remark that components have generally different sampling periods, and thus interconnection of sampled systems may not be definable in the formalism of Definition 5.

Remark 2: In this paper, it is assumed that all sampled systems have the same initial sampling time τ 0 = 0. This restriction is made for the sake of simplicity and the following results could be generalized to interconnections of sampled systems with an initial clock drift (τ 0 ∈ [0, τ )).

An assume-guarantee contract C = (A W , G X , G Y ) for sampled-data systems is given by Definition 4. The following result, gives sufficient conditions for strong satisfaction of contracts:

Proposition 1: Let Σ = (W, X, Y, U, f, g, h, τ ) be a sampled-data system satisfying Assumption 1, and let C = (A W , G X , G Y ) be an assume-guarantee contract for Σ with h(G X ) ⊆ G Y and dom(g) ⊆ G X . Let us assume that there exists ε > 0 such that for all x 0 ∈ dom(g), u ∈ g(x 0 ) and w ∈ C([0, τ ], W ), x = χ(., x 0 , u, w) satisfies:

(∀t ∈ [0, τ ], w(t) ∈ A W ) =⇒ (∀t ∈ [0, τ ], x(t) ∈ G X );
(2)

(∀t ∈ [0, τ ], w(t) ∈ B ε (A W ) =⇒ (∀t ∈ [0, τ ], h(x(t)) ∈ G Y ). (3)
Then, Σ |= s C.

The following result complements the previous one by providing sufficient conditions for the existence of complete trajectories of a sampled-data system:

Proposition 2: Let Σ = (W, X, Y, U, f, g, h, τ ) be a sampled-data system satisfying Assumption 1, and let C = (A W , G X , G Y ) be an assume-guarantee contract for Σ. Let us assume that for all x 0 ∈ dom(g), u ∈ g(x 0 ) and w ∈ C([0, τ ], W ), x = χ(., x 0 , u, w) satisfies:

(∀t ∈ [0, τ ], w(t) ∈ A W ) =⇒ (x(τ ) ∈ dom(g)). (4)
Then, all maximal trajectories (w, x, y) : I → W × X × Y in T such that for all t ∈ I, w(t) ∈ A W , are complete (i.e. I = R + 0 ). Propositions 1 and 2 provide simple criteria guaranteeing for a sampled-data system, strong satisfaction of an assume-guarantee contract and completeness of trajectories. Intuitively, Proposition 1 gives conditions on the behavior between the sampling instants, while Proposition 2 gives conditions on the behavior at the sampling instants. Then, Theorems 1 and 2 allow us to reason about interconnection of sampled-data systems.

Given a sampled data system and an assume-guarantee contract, in the following we show how symbolic control techniques can be used to enforce the strong satisfaction of such contract while ensuring the completeness of the maximal trajectories. Hence, the design problem can be formulated as follows:

Problem 1: For sampled-data system Σ = (W, X, Y, U, f, g, h, τ ), and τ > 0, and for assume-

guarantee contract C = (A W , G X , G Y ) with h(G X ) ⊆ G Y , design a control map g : X ⇒ U such that Σ |= s C
and all maximal trajectories (w, x, y) : I → W × X × Y of Σ such that for all t ∈ I, w(t) ∈ A W , are complete.

In the following, we provide a solution to Problem 1, based on conditions given by Propositions 1 and 2 and symbolic control techniques.

III. SYMBOLIC CONTROL DESIGN

In this section, we design a control map g : X ⇒ U , which is a solution to Problem 1.

A. Symbolic model

In this part, we show how to compute a symbolic abstraction, which guarantees by design the fulfilment of the conditions of Proposition 1 for strong satisfaction of the assume-guarantee contracts.

Our symbolic abstraction is given by a transition system A = (X d , U d , ∆) where X d and U d are finite sets of states and inputs, and ∆ :

X d × U d ⇒ X d is a transition relation.
1) Discretization: Our approach is based on a discretization of the state-space and input sets. We discretize the set of inputs U into n u ≥ 2 values, the discrete input set is given by: U d = u | = 0, . . . , n u -1 . We discretize the state-space into n x ≥ 1 using a finite partition X d of the set G X given by: X d = x | = 0, . . . , n x -1 . We define the quantizer Q X d : G X → X d associated to the partition X d as follows: for x ∈ G X and q ∈ X d , Q X d (x) = q if and only if x ∈ q.

For a state of the abstraction q ∈ X d , we denote the set of enabled inputs by enab ∆ (q) = {u ∈ U d | ∆(q, u) = ∅}. We denote the set of non-blocking states by nb ∆ = {q ∈ X d | enab ∆ (q) = ∅}.

2) Transition relation: We define the reachable set of (1) from a set of initial states X 0 ⊆ X at s ∈ R + 0 under the constant control input u ∈ U and a subset of disturbance inputs W * ⊆ W by: R s (X 0 , u, W * ) = {χ(s, x 0 , u, w) x 0 ∈ X 0 , w : [0, s] → W * } Similarly the reachable set of (1) from a set of initial states X 0 ⊆ X on [0, t] ⊆ R + 0 under the constant control input u ∈ U and a subset of disturbance inputs W * ⊆ W is given by: R [0,t] (X 0 , u, W

* ) = s∈[0,t] R s (X 0 , u, W * ).
We suppose that we are able to compute an overapproximation of the reachable set denoted R (several methods exist for the computation of over-approximation of reachable sets for linear systems [START_REF] Guernic | Reachability analysis of linear systems using support functions[END_REF], monotone systems [START_REF] Ramdani | Computing reachable sets for uncertain nonlinear monotone systems[END_REF] or general nonlinear systems [START_REF] Reissig | Feedback refinement relations for the synthesis of symbolic controllers[END_REF]).

The transition relation ∆ : X d × U d ⇒ X d , abstracting the dynamics of the sampled-data system Σ = (W, X, Y, U, f, g, h, τ ) is formally defined as follows.

Let ε > 0 arbitrarily small, q ∈ X d and u ∈ U d , q ∈ ∆(q, u) if and only if:

R [0,τ ] (q, u, A W ) ⊆ G X ; h(R [0,τ ] (q, u, B ε (A W ))) ⊆ G Y ; (5) q ∩ R τ (q, u, A W ) = ∅.
Let us remark that for q ∈ X d , u ∈ enab ∆ (q) if and only if the first two conditions of the transition relation ( 5) hold.

The parameter ε used in this construction of the transition relation can be freely chosen but is critical to ensure the strong satisfaction of the contract using the criterion of Proposition 1.

The following Lemma establishes the formal behavioral relationship between the dynamics of A and Σ: Lemma 1: Let Σ and C be as in Problem 1. Let A = (X d , U d , ∆) be constructed as in Section III-A . Let q ∈ nb ∆ , x 0 ∈ q, u ∈ enab ∆ (q), w ∈ C([0, τ ], W ) such that for all t ∈ [0, τ ], w(t) ∈ A W , and x = χ(., x 0 , u, w). Then, there exists q ∈ ∆(q, u) such that x(τ ) ∈ q .

Intuitively, the previous Lemma shows that A relates formally to the uncontrolled (i.e. with g(x) = U for all x ∈ U ) dynamics of Σ at sampling times with external inputs constrained in A W by an alternating simulation relation [START_REF] Tabuada | Verification and control of hybrid systems: a symbolic approach[END_REF].

The next proposition provides a simple condition relating the control map g to be designed to the symbolic abstraction A, which guarantees the strong satisfaction of assume-guarantee contracts:

Proposition 3: Let Σ and C be as in Problem 1. Let A = (X d , U d , ∆) be constructed as in Section III-A. If the control map g : X ⇒ U satisfies: dom(g) ⊆ G X and ∀x ∈ G X , g(x) ⊆ enab ∆ (Q X d (x)), (6)
then, Σ |= s C.

B. Symbolic controller synthesis

In this section, we show how to design the control map g : X ⇒ U , solving Problem 1. We state the main result of this section: Theorem 3: Let Σ and C be as in Problem 1. Let A = (X d , U d , ∆) be constructed as in Section III-A. Let the discrete controller Θ : X d ⇒ U d for the abstraction A satisfying:

∀q ∈ X d , Θ(q) ⊆ enab ∆ (q), (7) ∀q ∈ domΘ, ∀u ∈ Θ(q), ∆(q, u) ⊆ dom(Θ), (8)
Let the control map g : X ⇒ U of Σ defined by:

dom(g) ⊆ G X and ∀x ∈ G X , g(x) = Θ(Q X d (x)) (9)
Then, Σ |= s C and all maximal trajectories (w, x, y) :

I → W × X × Y of Σ such that for all t ∈ I, w(t) ∈ A W , are complete.
The previous result establishes the conditions that the setvalued map Θ : X d ⇒ U d has to satisfy in order to solve Problem 1. Let us remark that these conditions actually state that Θ is a discrete safety controller for the abstraction A keeping the trajectories of A in nb ∆ . Thus, Θ can be synthesized by computing the maximal controlled invariant of A in nb ∆ , which can be done by a maximal fixed point computation (see e.g. [START_REF] Tabuada | Verification and control of hybrid systems: a symbolic approach[END_REF]).

IV. VEHICLE PLATOONING EXAMPLE

A. Model description

In the following, we consider a platoon where each vehicle is modeled as a nonlinear and nonsmooth control system. We shall adapt the model from [START_REF] Ioannou | Autonomous intelligent cruise control[END_REF]:

M v = α(F, v) = F -f 0 -f 1 v -f 2 v 2 if v > 0 max(F -f 0 , 0) if v = 0 (10
) where M > 0 represent the mass of the vehicle, v its velocity, F is the net engine torque applied to the wheels and the term f 0 + f 1 v + f 2 v 2 include the rolling resistance and aerodynamics (f 0 , f 1 , f 2 ∈ R + ). In this equation, F is the control input and satisfies F ∈ [F min , F max ], where F min < 0 < F max .

Contrarily to [START_REF] Ioannou | Autonomous intelligent cruise control[END_REF], we have added the second equation to eliminate the unrealistic behaviour where the vehicle is moving backward (i.e v(t) ≥ 0 for all t ∈ R + 0 ). In this paper, we deal with a platoon of m vehicles in a circular road (see Figure 3). The dynamic of each vehicle i ∈ {1, . . . , m} is given by:

ḋi = v i-1 -v i M vi = α(F i , v i ). (11)
with the convention that v 0 = v m , where d i ≥ 0 represents the relative distance between vehicle i and the preceding vehicle i -1, v i its velocity and F i its control input. We can see that the dynamic of the vehicle is not continuous, however it can be easily shown that we have the existence and uniqueness of solution and Assumption 1 is satisfied.

Remark 3: We assume that all vehicles are identical only to keep notations simple. However, our approach can be extended directly to heterogeneous vehicles with α i depending on the vehicle parameters (M i , f 0i , f 1i , f 2i ).

B. Problem formulation and solution strategy

Our goal is to synthesize controllers, giving values of input F i , for all vehicles of a platoon such that the velocity of each vehicle remains between 0 and v max , and the relative distance between two vehicles remains larger than d min ≥ 0:

∀i ∈ {1, . . . , m}, ∀t ∈ R + 0 , v i (t) ∈ [0, v max ] and d i (t) ∈ [d min , +∞) (12)
Since, we are using symbolic control techniques, the dynamics of vehicle i can then be described by a sampleddata system Σ i = (W, X, Y, U, f, g i , h, τ i ) where the external input w i = v i-1 , the state x i = (d i , v i ) T , the output y i = v i , the dynamic of the vehicle f is given by ( 11) and

W = R + 0 , X = R × R + 0 , Y = R + 0 , U = [F min , F max ].
Then, the dynamics of the vehicle platoon on a cyclic road is given by the feedback-cascade composition (Σ 1 || c . . . || c Σ m ) f . Therefore, in view of Theorems 1 and 2, the control objective ( 12) can be achieved by assigning a suitable contract C to each vehicle in the platoon and resolving Problem 1 for the system Σ i and the contract C.

We assign the assume-guarantee contracts C

= (A W , G X , G Y ) to systems Σ i where A W = G Y = [0, v max ] and G X = [d min , +∞) × [0, v max ].
We use the symbolic approach presented in Section III-A to construct an abstraction A of Σ i which guarantees by design the strong satisfaction of the contract C. Then, a safety controller Θ is synthesized for the abstraction A and refined into a controller g : X ⇒ U for the system Σ i ensuring the completeness of maximal trajectories, using the approach presented in III-B. First, we explain the partitioning technique used for this problem.

C. Abstraction

Given the state space G X and let d > d min , we have that 4. Using n v and n d as abstraction parameters for velocity and distance axis respectively, partitions of S 1 , S 2 and S 3 are constructed as follows:

G X = S 1 ∪ S 2 ∪ S 3 , where: S 1 = [d , +∞) × (0, v max ], S 2 = [d min , d ] × (0, v max ] and S 3 = [d min , +∞) × {0}, as shown in figure
• We use unbounded regions for the partition of the set S 1 . Let us remark that this is necessary to cover the unbounded set G X with a finite number of subsets; • We construct a partition of S 2 using a uniform grid;

• We use regions with empty interior (flat symbols) for the set S 3 . This is necessary to discriminate the case when the velocity is 0 from the case when it belongs to (0, v max ]. For instance, if the leading vehicle stops and remains motionless, it is necessary to stop the following vehicle. Not being able to discriminate the case when the velocity is 0 from the case when it is (even slightly) positive would result in uncontrollable symbolic abstraction. Moreover, the partition of the set S 3 contains an unbounded region corresponding to [d , +∞) × {0}.

Remark 4: We can see that our partition differs from the classical partitions used in the literature. Indeed the problem cannot be solved using a uniform partition for the reasons stated above. This constraints are specific to this particular problem. The approach of the paper can also be applied to other systems for which a simple uniform partition can be used.

The input space U = [F min , F max ] is uniformly discretized into n u values. The transition relation is constructed based on [START_REF] Reißig | Computing abstractions of nonlinear systems[END_REF] where we used the monotonicity of the system to construct an overapproximation of the reachable set.

D. Numerical results

In this section, we illustrate our results using numerical simulations. We use the numerical values from [START_REF] Nilsson | Preliminary results on correct-by-construction control software synthesis for adaptive cruise control[END_REF] for the vehicle parameters. These values as well as the contract parameters are shown in Table I. We compute the symbolic abstraction A using the approach described in Section III-A, with the partition technique presented in Section IV-C. For discrete controller synthesis, the maximal fixed point computation allows us to determine the most permissive safety controller. The controller Θ is obtained after determinization of the most permissive safety controller by selecting the maximal safe input. Intuitively, it means that the vehicles drive as fast as possible while guaranteeing satisfaction of assume-guarantee contracts.

Figure 5 The choice of the abstraction parameters is important, of course the larger n u , n d and n v , the more accurate the abstraction. In particular, small values of these parameters may lead to uncontrollable abstractions (i.e. the maximal controlled invariant of A is empty). The choice of parameter d also has an influence, if d too close to the value d min , then the vehicles will not be able to drive at maximal speed.

On Figure 5, we see that if we modify and set d = 50, n d = 50, then the vehicles speed will never exceed 13m/s.

For numerical simulations, we consider a platoon of 20 vehicles. We consider identical vehicles, with parameters given by Table I, to emphasize the effect of the sampling periods. However the same approach can be applied even if we have heterogeneous vehicles.

1) Periodic sampling: We consider that all the vehicles have the same sampling period τ = 0.5, and the same abstraction parameters. Note that these parameters are the same as the ones used for computing the controller shown on Figure 5.

Figure 6 shows the simulation results for given initial conditions. One can check that distances between vehicles are always greater than 10 m and that velocities remain between 0 and 15 m/s at all time, so the overall objective is satisfied. It is interesting to remark that after a transient period, the vehicles distribute themselves uniformly on the road (i.e. the distances between vehicles are all equal) and drive at almost constant speed. Figure 7 shows the simulation results. One can check that distances between vehicles are always greater than 10 m and that velocities remain between 0 and 15 m/s at all time, so the overall objective is satisfied despite multiperiodic sampling. Similar to the periodic sampling case, we remark that after a transient period, the vehicles drive at almost constant speed. However, it is interesting to note that the final speed is smaller than in the periodic sampling case. An even more significant difference is seen on the inter-vehicle distances. Indeed, the vehicles do not distribute uniformly on the road. On this simulation, one can see that the vehicles with larger sampling period need to keep a larger distance to the front vehicle, which can be explained by the fact, that they need more time to react.

V. CONCLUSION

In this paper, we have presented a compositional approach to the design of interconnected sampled-data systems, based on a notion of continuous-time assume-guarantee contracts. This approach makes it possible to deal with heterogeneous components with different sampling periods. Synthesis of the sampled-data controller is addressed using discrete abstraction and symbolic controller synthesis. This approach has been applied to the design of controllers for vehicle platooning and numerical results show the effectiveness of the approach and reveal some interesting behaviours of these vehicle platoons. In future work, we will develop more general contracts, which may include dynamical models of external inputs and study their composition. These contracts will be applied to vehicle platooning where a model of the front vehicle can be taken into account during controller synthesis. We will also extend the results from cascade and feedback interconnections, to different types of interconnections.

Fig. 3 .

 3 Fig. 3. A platoon of 4 vehicles on a circular road

1 Fig. 4 .

 14 Fig. 4. Partition of G X = [d min , +∞) × [0, vmax] with n d = 5 and nv = 3.

  represents the resulting controller g for sampling period τ = 0.5, parameter of the construction of the transition relation ε = vmax 1000 and the following values of abstraction parameters: n u = 10, d = 70, n d = 70, n v = 30. The computation time for generating the symbolic abstraction and synthesizing the controller is about 1 minute (implementation in MATLAB, Processor 2.7 GHz Intel Core i5, Memory 8 GB 1867 MHz DDR3).

Fig. 5 .

 5 Fig. 5. Synthesized control map g.

2 )

 2 Multiperiodic sampling: We consider 20 vehicles with different sampling periods, where 7 vehicles have the sampling periods in [0.5, 0.62], 6 vehicles have the sampling periods in [1.3, 1.4] and 7 vehicles have their sampling periods in [2, 2.12].

Fig. 6 .

 6 Fig. 6. Simulation results of a platoon of 20 vehicles on a circular road with the same sampling period: inter-vehicle distance (top), velocities (bottom).

Fig. 7 .

 7 Fig. 7. Simulation results of a platoon of 20 vehicles on a circular road with different sampling periods: inter-vehicle distance (top), velocities (bottom)(red: vehicles with different sampling periods in [0.5, 0.62], purple: vehicles with different sampling periods in [1.3, 1.4], blue: vehicles with different sampling periods in [2, 2.12]).

APPENDIX

Proof of Proposition 1

Proof: Let (w, x, y) : I → W × X × Y be a trajectory of Σ. We have h(x 0 ) ∈ h(dom(g)) ⊆ h(G X ) ⊆ G Y .

Let t ∈ I, such that for all s ∈ [0, t], w(s) ∈ A W , let m ∈ N such that τ m ≤ t < τ m+1 .

For k ∈ {0, . . . , m -1}, τ k ∈ I, x(τ k ) ∈ dom(g) and there exists u k ∈ g(x(τ k )) such that for almost all s ∈ [τ k , τ k+1 ], ẋ(s) = f (x(s), u k , w(s)). Then, by [START_REF] Cassandras | Introduction to discrete event systems[END_REF], since for all s ∈ [τ k , τ k+1 ], w(s) ∈ A W , we have for all s ∈ [τ k , τ k+1 ], x(s) ∈ G X . By (3), we get that for all s ∈ [τ k , τ k+1 ], y(s) = h(x(s)) ∈ G Y . We also have τ m ∈ I, for which we consider two distinct cases.

If I = [0, τ m ], then t = τ m , and it follows from above that for all s ∈ [0, t], x(s) ∈ G X and for any δ > 0, for all

∈ dom(g) and there exists u m ∈ g(x(τ m )) such that for almost all s ∈ [τ m , τ m+1 ], ẋ(s) = f (x(s), u m , w(s)). We have for all s ∈ [τ m , t], w(s) ∈ A W . Let us start by proving the guarantee on the state. Let w : [τ m , τ m+1 ] → W given by w(s) = w(s) for s ∈ [τ m , t] and w(s) = w(t) for s ∈ [t, τ m+1 ]. w is continuous and since for all s ∈ [τ m , t], w(s) ∈ A W , we have for all s ∈ [τ m , τ m+1 ], w(s)

Then, by (2), we have for all s ∈ [τ m , τ m+1 ], x(s) ∈ G X . Moreover, by Assumption 1, it follows that x(s) = x(s) for all s ∈ [τ m , t]. Hence, for all s ∈ [0, t], x(s) ∈ G X . For the guarantee on the output, using the fact that for all s ∈ [τ m , t], w(s) ∈ A W , from the continuity of w and for ε > 0, there exists δ > 0 such that for all s ∈ [τ m , t+δ], w(s) ∈ B ε (A W ). We suppose without loss of generality that δ < τ m+1t. Let w * : [τ m , τ m+1 ] → W given by w * (s) = w(s) for s ∈ [τ m , t + δ] and w * (s) = w(t + δ) for s ∈ [t + δ, τ m+1 ]. w * is continuous and since for all s ∈ [τ m , t+δ], w(s) ∈ B ε (A W ), we have for all s ∈ [τ m , τ m+1 ], w * (s) ∈ B ε (A W ). Then, using a similar reasoning to the guarantee on the states, we have for all s ∈ [τ m , t

Proof of Proposition 2

Proof: Let us consider a maximal trajectory (w, x, y) : I → W ×X ×Y in T such that for all t ∈ I, w(t) ∈ A W , and let us assume that (w, x, y) is not complete (i.e. I = [0, τ l+1 ] with l ∈ N). Then, x(τ l ) ∈ dom(g), u l ∈ g(x(τ l )) and for almost all t ∈ [τ l , τ l+1 ], ẋ(t) = f (x(t), u l , w(t)); it follows from (4) that x(τ l+1 ) ∈ dom(g). Then, let:

• w : [0, τ l+2 ] → W be a continuous function such that for all t ∈ [0, τ l+1 ], w(t) = w(t); • x : [0, τ l+2 ] → X be an absolutely continuous function such that for all t ∈ [0, τ l+1 ], x(t) = x(t), and for all t ∈ [τ l+1 , τ l+2 ], ẋ(t) = f (x(t), u l+1 , w(t)), for a u l+1 ∈ g(x(τ l+1 )), such a function exists by Assumption 1;

Then, it is clear that ( w, x, ȳ) ∈ T and that (w, x, y) is a prefix of ( w, x, ȳ) which contradicts the maximality of (w, x, y). Hence, necessarily, (w, x, y) is complete.

Proof of Lemma 1

Proof: Let q ∈ nb ∆ , x 0 ∈ q, u ∈ enab ∆ (q) and w ∈ C([0, τ ], W ) such that for all t ∈ [0, τ ], w(t) ∈ A W . We have x(τ ) = χ(τ, x 0 , u, w) ⊆ R τ (q, u, A W ) ⊆ R [0,τ ] (q, u, A W ) ⊆ G X . Hence, using the definition of the transition relation ∆ there exists q ∈ ∆(q, u) satisfying x(τ ) ∈ q .

Proof of Proposition 3

Proof: We prove the strong satisfaction of the contract using Proposition 1.

Let us remark that dom(g) ⊆ G X . Then, let x 0 ∈ dom(g), u ∈ g(x 0 ), w ∈ C([0, τ ], W ) and x = χ(., x 0 , u, w). By [START_REF] Tazaki | Bisimilar finite abstractions of interconnected systems[END_REF], u ∈ enab ∆ (q 0 ) where q 0 = Q X d (x 0 ). First, let us suppose that for all t ∈ [0, τ ], w(t) ∈ A W , we have for all t ∈ [0, τ ], x(t) = χ(t, x 0 , u, w) ∈ R t (q 0 , u, A W ) ⊆ R [0,τ ] (q 0 , u, A W ) ⊆ G X , where the second inclusion comes from the first condition in the definition of the transition relation. Now, let ε > 0 be as in the definition of transition relation [START_REF] Reißig | Computing abstractions of nonlinear systems[END_REF] and assume that for all t ∈ [0, τ ], w(t) ∈ B ε (A W ).

We have for all

where the second inclusion comes from the second condition of the definition of the transition relation. Hence, we can conclude that Σ |= s C.

Proof of Theorem 3

Proof: Let us remark that ( 9) and ( 7) imply that g satisfies the condition [START_REF] Tazaki | Bisimilar finite abstractions of interconnected systems[END_REF]. Then, Σ |= s C. To prove the second part of the theorem, we show that condition (4) in Proposition 2 holds. Let x 0 ∈ dom(g), u ∈ g(x 0 ), w ∈ C([0, τ ], W ), and x = χ(., x 0 , u, w). By (9), u ∈ Θ(q 0 ) where q 0 = Q X d (x 0 ). By [START_REF] Dallal | On compositional symbolic controller synthesis inspired by small-gain theorems[END_REF], u ∈ enab ∆ (q 0 ) and by Lemma 1, there exists q ∈ ∆(q, u) such that x(τ ) ∈ q . Then, [START_REF] Kim | Compositional controller synthesis for vehicular traffic networks[END_REF] gives that q ∈ dom(Θ), which in turn implies by (9) that x(τ ) ∈ dom(g).