W A Apaza-Perez

A Girard

C Combastel

A Zolghadri

Symbolic observer-based controller for uncertain nonlinear systems*

Symbolic control is an approach to the control of continuous or hybrid systems with specifications expressed in a logic form. This approach is based on the use of symbolic models describing the dynamical system behavior with a finite description of the transition relation between its states. In the literature, many results using this approach assume the availability of full and exact information about the system states to compute the control actions. In this paper, we consider a more realistic scenario where only partial information about the plant states is available. This paper proposes an abstraction that makes it possible to synthesize output-feedback controllers. The presence of disturbances and output noise is also considered. A direct path between observer designs in the classical theory and control synthesis in formal methods is established and a numerical example is provided to illustrate the results.

I. INTRODUCTION

Over the last decades, the problem of control design for systems with complex specifications has spurred on substantial research efforts that have been developing along several major lines. One appealing direction takes advantage of the socalled formal methods and is based on symbolic models. These models are abstractions which are related to the dynamics of the system by some formal behavioral relationship such as alternating simulations [START_REF] Tabuada | Verification and Control of Hybrid Systems[END_REF] or feedback refinement relations [START_REF] Reissig | Feedback refinement relations for the synthesis of symbolic controllers[END_REF]. This allows to capture aspects of the system being analyzed explaining how the results of analysis/design for the symbolic model can be used in the system, see for example [START_REF] Tabuada | Verification and Control of Hybrid Systems[END_REF], [START_REF] Alur | Discrete abstractions of hybrid systems[END_REF], [START_REF] Reissig | Computing abstractions of nonlinear systems[END_REF], [START_REF] Belta | Formal Methods for Discrete-Time Dynamical Systems[END_REF]. Finite state models are especially well suited for automated analysis and offer a common language to describe an abstract view of continuous dynamics as well as the software implementation of control algorithms [START_REF] Lee | Introduction to embedded systems: A cyberphysical systems approach[END_REF]. It is, therefore, possible to formally reason about the behavior of the interconnection between continuous dynamics and software which has been one of the main thrusts behind the research area of hybrid systems. Classical control theory provides a wide range of results to control of continuous or hybrid systems where control objectives are usually aimed at satisfying specifications such as stabilization, output tracking or disturbance rejection; while symbolic control and systems allow us to consider more complex specifications expressed in some formal syntax (e.g. linear temporal logic LTL, *This project has received funding from: the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement No 725144); and the French State, managed by the French National Research Agency (ANR) in the frame of the "Investments for the future" Programme IdEx Bordeaux -SysNum (ANR-10-IDEX-03-02).

1 W.A. Apaza-Perez, A. Girard are with the Université Paris-Saclay, CNRS, CentraleSupélec, Laboratoire des signaux et systèmes, 91190, Gif-sur-Yvette, France {willy-alejandro.apaza-perez; Antoine.Girard}@l2s.centralesupelec.fr 2 C. Combastel, A. Zolghadri are with the Univ. of Bordeaux, CNRS, IMS, UMR 5218, 33405 Talence, France {christophe.combastel, ali.zolghadri}@u-bordeaux.fr computational tree logic). The use of symbolic models for control design purposes has been investigated, among many others, in the following papers: LTL specifications for linear control systems by [START_REF] Gol | Language-guided controller synthesis for linear systems[END_REF], [START_REF] Tabuada | Linear time logic control of discrete-time linear systems[END_REF], and for discrete time piecewise affine systems by [START_REF] Yordanov | Temporal logic control of discrete-time piecewise affine systems[END_REF], [START_REF] Pola | Symbolic models for networks of discrete-time nonlinear control systems[END_REF]; nonlinear control systems with general specifications in a behavioral framework by [START_REF] Tabuada | Verification and Control of Hybrid Systems[END_REF], [START_REF] Pola | On symbolic control design of discrete-time nonlinear systems with state quantized measurements[END_REF], [START_REF] Reissig | Feedback refinement relations for the synthesis of symbolic controllers[END_REF], and with specifications expressed as nondeterministic transition systems by [START_REF] Pola | Integrated design of symbolic controllers for nonlinear systems[END_REF]; nonlinear switched systems and safety and reachability specifications were considered in [START_REF] Girard | Controller synthesis for safety and reachability via approximate bisimulation[END_REF], [START_REF] Girard | Low-complexity quantized switching controllers using approximate bisimulation[END_REF]; networked nonlinear control systems and specifications expressed as nondeterministic transition systems in [START_REF] Borri | Integrated symbolic design of unstable nonlinear networked control systems[END_REF], [START_REF] Borri | Design of symbolic controllers for networked control systems[END_REF]. [START_REF] Meyer | Compositional abstraction and safety synthesis using overlapping symbolic models[END_REF] considers safety specifications and overlapping symbolic models. Along theoretical results, computational tools have also been developed to compute abstractions and control synthesis PESSOA [START_REF] Mazo | Pessoa: A tool for embedded controller synthesis[END_REF], CoSyMa [START_REF] Mouelhi | Cosyma: A tool for controller synthesis using multi-scale abstractions[END_REF], TuLiP [START_REF] Wongpiromsarn | Tulip: A software toolbox for receding horizon temporal logic planning[END_REF], SCOTS [START_REF] Rungger | Scots: A tool for the synthesis of symbolic controllers[END_REF], pFaces [START_REF] Khaled | Pfaces: An acceleration ecosystem for control[END_REF], or Mascot [START_REF] Hsu | Multi-layered abstraction-based controller synthesis for continuous-time systems[END_REF]. Apart from differences in the classes of specifications and of plants considered, the common denominator of the papers above is in assuming full information on the state of the plant for control purposes. The issue is that this assumption may become very restrictive in many real applications where only output variables, or sensor measurements of them, are available.

The aim of the paper is to overcome the crucial assumption about full and exact knowledge of the states of the system for the controller synthesis. We use observers to define an abstraction, which allows us to cover a wide class of systems (linear and nonlinear) due to the extensive literature on observer design in the classical control theory for continuous or hybrid systems [START_REF] Luenberger | An introduction to observers[END_REF], [START_REF] Shamma | Set-valued observers and optimal disturbance rejection[END_REF], and complex specifications can be considered [START_REF] Belta | Formal Methods for Discrete-Time Dynamical Systems[END_REF]. The proposed observer-based approach to synthesize symbolic controllers for systems with partial information and bounded disturbances has some important features: i) The abstraction is related to a feedback refinement relation of the system formed by the plant and the observer, ii) Computing the abstraction is solely based on the dynamics of the plant and only requires the knowledge of some bounds on the estimation error of the observer, iii) Controller refinement only requires feeding the obtained symbolic controller with the state estimate of the observer. Some recent works on observer/estimator-based abstractions for control with partial information can be found in [START_REF] Haesaert | Correct-by-design output feedback of lti systems[END_REF], [START_REF] Mickelin | Synthesis of correct-byconstruction control protocols for hybrid systems using partial state information[END_REF], [START_REF] Mizoguchi | Deadlock-free output feedback controller design based on approximately abstracted observers[END_REF], [START_REF] Pola | Symbolic control design of nonlinear systems with outputs[END_REF], [START_REF] Majumdar | On abstraction-based controller design with output feedback[END_REF]. The observer design can be realized from the initial dynamic system as it is done in [START_REF] Haesaert | Correct-by-design output feedback of lti systems[END_REF] and [START_REF] Mickelin | Synthesis of correct-byconstruction control protocols for hybrid systems using partial state information[END_REF] where discrete-time linear systems with LTL specifications, and a class of discrete-time piecewise-affine systems with a robust interpretation of LTL were considered respectively. In comparison, in the current work, the approach allows considering linear and non-linear systems with uncertainties. In another way, the estimation of the non-measurable states can also be done at the symbolic level as it has been done works [START_REF] Mizoguchi | Deadlock-free output feedback controller design based on approximately abstracted observers[END_REF], [START_REF] Pola | Symbolic control design of nonlinear systems with outputs[END_REF], [START_REF] Majumdar | On abstraction-based controller design with output feedback[END_REF] but this demands the use of more computational resources due to the handling of sets of symbolic states as estimators.

The remainder of the paper is organized as follows. Section II presents some preliminary notions. The problem is formally stated and the main results are presented in section III. In section IV, a numerical example is presented to illustrate technical results. Finally, section V concludes the paper with some remarks.

II. PRELIMINARIES

Notations. R, R >0 , R ≥0 , and N 0 denote the set of real, positive real, non negative real numbers, and non negative integers, respectively. Given a, b ∈ N 0 such that a ≤ b, we denote by [a; b] a closed interval in N 0 . Given a relation R ⊆ X ×Y and X ⊆ X, we have R(X ) = {y ∈ Y | ∃x ∈ X , (x, y) ∈ R}. Consider a vector x ∈ R n , we denote by x i the i-th component of x and by

x the Euclidean norm of x.

For ε ∈ R n ≥0 , x ∈ R n and A ⊆ R n , define the ε-expansion of A as the set N ε (A) = {y ∈ R n | ∃x ∈ A, ∀i ∈ [1; n], |y i -x i | ≤ ε i },
and a hyper rectangle with center x and radius ε as

N ε (x) = {y ∈ R n | ∀i ∈ [1; n], |y i -x i | ≤ ε i }. Given a function V : X ⊆ R n → R ≥0 and k ∈ R ≥0 , its gradient is denoted by ∇V and V -1 (≤ k) = {x ∈ X|V (x) ≤ k}. A continuous function γ : R ≥0 → R ≥0 is said to belong to class κ (resp. κ ∞ ) if it
is strictly increasing and γ(0) = 0 (and γ(r) → ∞ when r → ∞). X + denotes the set of finite sequences of elements in X.

A. Transition systems.

Abstractions are dynamical systems with finitely many states and input values, each of which symbolizes aggregates of states and inputs of the original system. Abstractions are mathematically modeled as transition systems [START_REF] Tabuada | Verification and Control of Hybrid Systems[END_REF].

Definition 1 (Transition system): A transition system S is a tuple (X,U, F), where X is a set of states, U is a set of control inputs, F ⊆ X ×U × X is a transition relation.

The notation F(x, u) = {x ∈ X|(x, u, x ) ∈ F} denotes the set of successors of x upon control input u. Since F(x, u) may be empty, we denote

U(x) = {u ∈ U|F(x, u) = / 0} . A system is called nonblocking if the set U(x) of every x ∈ X is nonempty. A transition (x, u, x ) ∈ F is also denoted by x u - → x and an infinite sequence of transitions x 0 u 0 -→ x 1 u 1 -→ x 2 u 2 -→ • • • by (x u i i ) i∈N 0 ,
where the set of all infinite sequences of transitions in X is denoted by (X × U) ω . A state-feedback control C is a partial function on non-empty sequences of states of the system

C : X × (U × X) + → 2 U (1) (x 0 , u o , x 1 , u 1 ..., u k-1 , x k ) → U k
where U k is a set of admissible inputs to be used in the subsequent k-step. The behaviour generated by a system S and a state-feedback control C is denoted as B(S,C) and consists of all infinite sequences (x

u i i ) i∈N 0 ∈ (X × U) ω that satisfies u i ∈ C(x 0 , u 0 , .., u i-1 , x i ) and x i u i -→ x i+1 for all i ∈ N 0 . Given ε ∈ R n ≥0 , the ε-expansion of B(S,C) is defined as N ε (B(S,C)) = {(y u i i ) i∈N 0 ∈ (X ×U) ω |∃ (x u i i ) i∈N 0 ∈ B(S,C) ∧ ∀i ∈ N 0 , |x i -y i | ≤ ε i }.
Consider a transition system S = (X,U, F), where X ⊆ X 1 × X 2 , and a state-feedback control C in the system S. The projection of B(S,C) over X 1 , denoted by

B X 1 (S,C), is de- fined as B X 1 (S,C) = {(x u i i ) i∈ N 0 ∈ (X ×U) ω |∃(( xi , z i ) u i ) i∈N 0 ∈ B(S,C) ∧ ∀i ∈ N 0 , x i = xi },
and the projection over X 2 is defined analogously.

Definition 2: Given two transition systems S a = (X a ,U a , F a ) and

S b = (X b ,U b , F b ) with U b ⊆ U a . A relation R ⊆ X a × X b is a feedback refinement relation from S a to S b if ∀x a ∈ X a , ∃x b ∈ X b , (x a , x b ) ∈ R and the following holds for all (x a , x b ) ∈ R: U b (x b ) ⊆ U a (x a ); (2) u ∈ U b (x b ) =⇒ R(F a (x a , u)) ⊆ F b (x b , u).
Feedback refinement relation allows the designer to work with the abstract system S b instead of the concrete system S a . Under conditions in (2), a controller for the abstract system S b can be used on the concrete system S a , see [START_REF] Reissig | Feedback refinement relations for the synthesis of symbolic controllers[END_REF].

III. PROBLEM STATEMENT

Consider the following nonlinear continuous-time system

ξ (t) = f (ξ (t), u(t), w(t)) y(t) = h(ξ (t), δ (t)) (3)
where

ξ (t) ∈ X ⊆ R n , u(t) ∈ U ⊆ R p , y(t) ∈ Y ⊆ R m denote
the state, the control input, the measured output at time t ∈ R ≥0 , respectively. The uncertainties denoted by

w(t) ∈ W ⊆ R r 1 and δ (t) ∈ D ⊆ R r 2 are bounded, i.e. there exist b 1 , b 2 ∈ R ≥0 such that ∀t ∈ R ≥0 , w(t) ≤ b 1 , δ (t) ≤ b 2 .
The problem considered in the paper can be roughly formulated as follows: how to build abstractions which take into account disturbances and partial information of the system and how to synthetize output feedback controllers.

A. Observer and discrete abstraction

Assume there exist: i) An observer for the system (3), which is expressed by ξ

(t) = g( ξ (t), u(t), y(t)), (4)
where ξ (t) ∈ X ⊆ R n . It is assumed that the observer has been synthesized by some method, e.g. [START_REF] Martinelli | Nonlinear unknown input observability: Extension of the observability rank condition[END_REF], [START_REF] Rocha-Cózatl | Dissipative design of unknown input observers for systems with sector nonlinearities[END_REF]. ii) class-κ ∞ functions α, α, class-κ functions β , γ 1 , γ 2 , and a positive-definite function V : R n → R ≥0 such that into the dynamic of the estimation error

ż(t) = G(z(t), ξ (t), u(t), w(t), δ (t)), (5)
where z(t) = ξ (t)ξ (t), the following conditions hold

α( z ) ≤ V (z) ≤ α( z ) (6)
∇V (z(t)) • G (z(t), ξ (t), u(t), w(t), δ (t)) ≤ (7) -β (V (z(t))) + γ 1 ( w(t) ) + γ 2 ( δ (t) ).
Consider the composition of system (3) and the observer (4) given by

ξ (t) = f (ξ (t), u(t), w(t)), ξ (t) = g( ξ (t), u(t), h(ξ (t), δ (t))), (8)
where forward completeness is assumed, and define the state space I as

I = {(x, x) ∈ X × X |V (x -x) ≤ β -1 (γ 1 (b 1 ) + γ 2 (b 2 ))}. (9)
Note that condition [START_REF] Gol | Language-guided controller synthesis for linear systems[END_REF] ensures that I is a forward invariant set. Since we are interested in controlling the system (3) through a digital and quantized controller, the controls are assumed piecewise constant functions from R + 0 to U such that given τ ∈ R >0 , u(t) = u(kτ) for all t ∈ [kτ, (k + 1)τ[ and k ∈ N 0 . The τ-sampled system from ( 8) is given as

S 1 = (X 1 ,U 1 , F 1 ) (10)
with state space X 1 = I, input space U 1 = U and a transition function

F 1 ((x, x), u) := {(x , x ) | ∃(ξ , ξ ) a solution of (8) with u ∈ U 1 ∧ (ξ (0), ξ (0)) = (x, x) ∧ (ξ (τ), ξ (τ)) = (x , x )}.
Consider uniform grids

ηZ n = {q ∈ R n |∃k ∈ Z n , ∀i ∈ [1; n] q i = k i η i }, µZ p = {u ∈ R p |∃k ∈ Z p , ∀i ∈ [1; p] u i = k i µ i }, with η ∈ R n >0 and µ ∈ R p >0 . Given ε ∈ R n ≥0 , define a system S 2 = (X 2 ,U 2 , F 2 ) ( 11
)
with

X 2 = 2ηZ n ∩ X, U 2 = µZ p ∩U 1 , and
F 2 (q, u) = q ∈ X 2 | N ε (F 0 (N ε+η (q), u)) ∩ N η (q ) = / 0 ,
where given a set A ⊆ X,

F 0 (A, u) := x ∈X ∃ x ∈ A, ∃ ξ a solution of (3) with u ∈ U 2 ∧ ξ (0) = x ∧ ξ (τ) = x .
The quantizer map from X to X 2 is denoted Q and defined as Q( x) = {q ∈ X 2 | x ∈ N η (q)}. The behavior of the transition relation F 2 defined in [START_REF] Pola | On symbolic control design of discrete-time nonlinear systems with state quantized measurements[END_REF] is illustrated in Figure 1. if the estimation error between ξ and ξ is included in the ε-expansion of N η (q), then its effect on the dynamics F 0 under u is included in ε-expansion of F 0 (N η+ε (q), u).

The following theorem allows us to define a feedback refinement relation between S 1 and S 2 .

Theorem 3: Consider the systems ( 10) and ( 11), then the relation

R = {((x, x), q) ∈ X 1 × X 2 | x ∈ N η (q)}, (12)
defines a feedback refinement relation from

S 1 to S 2 if V -1 (≤ β -1 (γ 1 (b 1 ) + γ 2 (b 2 ))) ⊆ N ε (0). Proof. Let ((x, x), q) ∈ R, u ∈ U 2 (q) ⊆ U 1 ((x, x)
). The proof is reduced to guarantee the following inclusion R (F 1 ((x, x), u)) ⊆ F 2 (q, u). Consider q ∈ R (F 1 ((x, x), u)), then there exists

(x , x ) ∈ F 1 ((x, x), u) such that x ∈ N η ( q), (13)
by [START_REF] Pola | Integrated design of symbolic controllers for nonlinear systems[END_REF]. As I is a forward invariant set from ( 6)-( 7), then

F 1 ((x, x), u) ⊆ I. Consequently, V (x -x ) ≤ β -1 (γ 1 (b 1 ) + γ 2 (b 2 )), which implies ∀i ∈ [1; n], |x i -x i | ≤ ε i , (14)
by

V -1 (≤ β -1 (γ 1 (b 1 ) + γ 2 (b 2 ))) ⊆ N ε (0). From (14), we obtain x ∈ N ε (F 0 (x, u)) . (15)
As ((x, x), q) ∈ R, then (x, x) ∈ I which implies xx ∈ V -1 (≤ β -1 (γ 1 (b 1 ) + γ 2 (b 2 )) by [START_REF] Yordanov | Temporal logic control of discrete-time piecewise affine systems[END_REF]. Consequently,

∀ i ∈ [1; n], |x i -xi | ≤ ε i . ( 16
)
As x ∈ N η (q), then x ∈ N ε+η (q) by ( 16), and F 0 (x, u) ⊆ F 0 (N ε+η (q), u). Thus, N ε (F 0 (x, u)) ⊆ N ε (F 0 (N ε+η (q), u)) holds. From [START_REF] Borri | Integrated symbolic design of unstable nonlinear networked control systems[END_REF], it is ensured that x ∈ N ε (F 0 (N ε+η (q), u)) which implies with (13) that N η ( q) ∩ N ε (F 0 (N ε+η (q), u)) = / 0, i.e. R(F 1 ((x, x), u)) ⊆ F 2 (q, u).

The idea behind the hyper rectangle containing the invariant set is to better manage the precision of the observer which is affected by different disturbances. If a controller can be designed satisfying some specifications based on abstraction [START_REF] Pola | On symbolic control design of discrete-time nonlinear systems with state quantized measurements[END_REF], then an output feedback controller based on chosen observer can be used to compute controls driving the initial system consistently with the specifications.

Proposition 4: Assume that conditions on Theorem 3 hold, and let C 2 : X 2 × (U 2 × X 2 ) + → U 2 be a control defined in the system [START_REF] Pola | On symbolic control design of discrete-time nonlinear systems with state quantized measurements[END_REF]. If a control C 1 :

X 1 × (U 2 × X 1 ) + → U 2 in (10) is defined as C 1 (x 0 , x0 , u 0 , x 1 , x1 , u 1 , ..., x k , xk ) := C 2 (Q( x0 ), u 0 , Q( x1 ), u 1 , ..., Q( xk )), then B X (S 1 ,C 1 ) ⊆ N ε+η (B(S 2 ,C 2 )) . ( 17
)
Proof. The proof is reduced to two claims:

Claim 1. B X (S 1 ,C 1 ) ⊆ N ε (B X(S 1 ,C 1 )). Let (x u i i ) i∈N 0 ∈ B X (S 1 ,C 1 ) then ∃ ( xu i i ) i∈N 0 ∈ ( X ×U 2 ) ω , ((x i , xi ) u i ) i∈N 0 ∈ B(S 1 ,C 1 ). (18)
From ( 18) and its projection over X, (

xu i i ) i∈N 0 ∈ B X(S 1 ,C 1 ) holds, and ∀i ∈ [1; n], | xi -x i | ≤ ε i by (8)-(9). Consequently, (x u i i ) i∈N 0 ∈ N ε (B X(S 1 ,C 1 )). Claim 2. N ε (B X(S 1 ,C 1 )) ⊆ N ε+η (B(S 2 ,C 2 )). Let (x u i i ) i∈N 0 ∈ N ε (B X(S 1 ,C 1 )), then ∃ ( xu i i ) i∈N 0 ∈ B X(S 1 ,C 1 ) such that ∀i ∈ [1; n], | xi -x i | ≤ ε i . Since control C 1 is defined from C 2
and applying the quantizer Q to the states of ( xu i i ) i∈N 0 , then there exists (q

u i i ) i∈N 0 ∈ B(S 2 ,C 2 ) such that ∀i ∈ [1; n], xi ∈ N η (q i ). Consequently (x u i i ) i∈N 0 ∈ N ε+η (B(S 2 ,C 2 ))
. Theorem 3 provides an abstraction design which is related by a feedback refinement relation of the system formed by the plant and the observer. It should be pointed out that this abstraction computation is solely based on the dynamics of the plant and only requires the knowledge of some bound ε on the estimation error of the observer, see system S 2 in [START_REF] Pola | On symbolic control design of discrete-time nonlinear systems with state quantized measurements[END_REF]. Proposition 4 allows us to refine a controller C 1 which only requires feeding the obtained symbolic controller C 2 with the state estimate of the observer through the quantizer map Q.

IV. EXAMPLE: ADAPTIVE CRUISE CONTROL

Adaptive cruise control is a driver assistance system that seeks to combine safe following distance with speed regulation. We consider a set-up with two vehicles. Vehicle 2 is following vehicle 1, the relative position of vehicle 2 w.r.t the vehicle is given by d ∈ (-∞, 0].

The dynamic of vehicle 2 is controlled while that of vehicle 1 is considered as a disturbance. Consider the following continuous-time model adapted from [START_REF] Nilsson | Correct-by-construction adaptive cruise control: Two approaches[END_REF]:

     ḋ = v 1 -v 2 ; y d = d + δ 1 ; v2 = u-h(v 2 ) M ; y v 2 = v 2 + δ 2 ; v1 = Γ(v 1 , w); (19) where h(v 2 ) = f 0 + f 1 v 2 + f 2 v 2 2
, and the function Γ as

Γ(v 1 , w) =      w if v 1 ∈ (v min 1 , v max 1 ) max(0, w) if v 1 = v min 1 min(0, w) if v 1 = v max 1 which gives v 1 (t) ∈ [v min 1 , v max 1
] for all time. The states d and v 2 are measured through the outputs y d and y v 2 , while v 1 is not measured. The control input u ∈ [u min , u max ] represents the contribution of braking and engine torque to the acceleration of vehicle 2. M > 0 represents the mass of vehicle 2, while the vector of parameters f = ( f 0 , f 1 , f 2 ) describes the road friction and vehicle aerodynamics. The disturbance w(t) ∈ [w min , w max ] represents the acceleration of vehicle 1, and δ 1 , δ 2 denote bounded disturbances in the measured variables of the system.

The problem of designing an adaptive cruise control system is considered with a time headway defined as ϑ (t) = -d(t)/v 2 (t). The requirements for adaptive cruise control are parameterized by a target velocity v * and a target time headway ϑ * . They are formulated as synthesizing a controller enforcing uniform attractivity of

X * = (d, v 2 ) ∈ R 2 | (-d/v 2 , v 2 ) ∈ Z * a ∪ Z * b , (20)
where

Z * a = {(ϑ , v 2 ) ∈ R 2 | ϑ ≥ ϑ * , v 2 = v * }, Z * b = {(ϑ , v 2 ) ∈ R 2 | ϑ = ϑ * , v 2 ≤ v * }.
Actually, this specification cannot be enforced so we aim at synthesizing a least-violating controller, according to [START_REF] Girard | Least-violating symbolic controller synthesis for safety, reachability and attractivity specifications[END_REF], enforcing the closed-loop behavior whose attractor is the closest to X * in [START_REF] Wongpiromsarn | Tulip: A software toolbox for receding horizon temporal logic planning[END_REF] with respect to the following distance function:

H(d, v 2 , v 1 ) = min (ϑ ,v 2 )∈Z * a ∪Z * b max | -d/v 2 -ϑ |, α|v 2 -v 2 |
where α > 0 is a design parameter defining the relative tolerance to deviations from the desired velocity and from the desired time headway. In addition, we specify strong safety requirements regarding collision avoidance and conformance to speed limitations. We must at all time: i) keep the distance d(t) ≤ 0, and ii)

keep velocity v 2 (t) ∈ [v min 2 , v max 2 ].
Values of parameters, compatible with empirical measurements are taken from [START_REF] Nilsson | Correct-by-construction adaptive cruise control: Two approaches[END_REF] and given in Table I.

Consider the observer which is similar to [START_REF] Mouelhi | Cosyma: A tool for controller synthesis using multi-scale abstractions[END_REF] with linear correction terms; the parameters l 1 ,..., l 6 will be designed to ensure that trajectories ( d, v2 , v1 ) converge to a neighborhood of (d, v 2 , v 1 ) (related to the considered disturbances). Defining estimation errors as

     ḋ = v1 -v2 + l 1 d -y d + l 2 ( v2 -y v 2 ) , v2 = u-h(y v 2 ) M + l 3 d -y d + l 4 ( v2 -y v 2 ) v1 = l 5 d -y d + l 6 ( v2 -y v 2 ) (21)
e d = d -d, e v 1 = v1 -v 1 , e v 2 = v2 -v 2 ,
the estimation error dynamics is defined as:

     ėd = e v 1 -e v 2 + l 1 e d + l 2 e v 2 -l 1 δ 1 -l 2 δ 2 ėv 2 = h (v 0 2 ) M δ 2 + l 3 e d + l 4 e v 2 -l 3 δ 1 -l 4 δ 2 ėv 1 = l 5 e d + l 6 e v 2 -l 5 δ 1 -l 6 δ 2 -Γ(v 1 , w) (22)
where

v 0 2 is an unknown value inside [v min 2 , v max 2 ] but |h (v 0 2 )| ≤ h = f 1 + 2 f 2 v max 2
holds (locally Lipschitz). Since the disturbances considered in the system [START_REF] Mouelhi | Cosyma: A tool for controller synthesis using multi-scale abstractions[END_REF] are bounded, there are constants

δ 1 , δ 2 , Γ ∈ R >0 such that |δ 1 | ≤ δ 1 , |δ 2 | ≤ δ 2 , |Γ(v 1 , w)| ≤ Γ are satisfied.
In matrix terms, the system ( 22) can be expressed as

ė = (A + LC) e + (LC + B 1 )∆ δ + B 2 W w, (23)
where

e = [e d , e v 2 , e v 1 ] T , ∆ = √ 3 diag(δ 1 , δ 2 , h M δ 2 ), W = Γ, A = 0 -1 1 0 0 0 0 0 0 , L = l 1 l 2 l 3 l 4 l 5 l 6 , C = 1 0 0 0 1 0 , B 1 = 0 0 0 0 0 1 0 0 0 , B 2 = 0 0 1 , δ = ∆ -1 -δ 1 -δ 2 h (v 0 1 ) M δ 2 T
, w = -W -1 Γ(v 1 , w). The disturbances in terms of δ , w allows to satisfy δ , w ≤ 1.

We propose a quadratic Lyapunov function V (e) = e T Pe for the system [START_REF] Khaled | Pfaces: An acceleration ecosystem for control[END_REF], where P ∈ R 3×3 is a positive definite matrix which will be obtained through the next matrix inequality 1 :

A T P+PA+C T Z T +ZC+λ P ∆ T (C T Z T +B T 1 P) -ρ 1 I 3 W T B T 2 P 0 -ρ 2 ≤ 0, (24)
where Z = PL, and λ , ρ 1 , ρ 2 ∈ R >0 are design parameters. The derivative of Lyapunov function along the trajectories of the system ( 23) is given by V (e(t)) = e T A T P + PA +C T Z T + ZC e+

+ 2e T (ZC + PB 1 )∆ δ + 2e T PB 2 W w ≤ -λ e T Pe + ρ 1 δ 2 + ρ 2 w 2 , from (24)
.

Thus, all trajectories of (23) converge to the invariant set

V -1 ( ≤ ρ 1 +ρ 2 λ
), which is contained in a hyper rectangle N ε (0), with ∀i ∈ [1; 3], ε i = ρ 1 +ρ 2 λ (P -1 ) i,i , see Proposition 1 in [START_REF] Guernic | Reachability analysis of linear systems using support functions[END_REF]. For the numerical results reported below the following parameters were chosen: δ 1 = δ 2 = 0.01 and notice that Γ(v 1 , w) ∈ [w min , w max ], obtaining from ( 24 The parameter ε is used to define S 2 in [START_REF] Pola | On symbolic control design of discrete-time nonlinear systems with state quantized measurements[END_REF] with the abstraction parameters η = (η d , η v 2 , η v 1 ) and µ which were chosen as:

d 0 = -100m, η d = -d 0 /100, η v 2 = (v max 2 -v min 2 )/100, η v 1 = (v max 1 -v min 1 )
/80, µ = (u maxu min )/10. Theorem 3, using ε and V (e) = e T Pe, guarantees a feedback refinement relation between the τ-sampled system of ( 19)-( 21) and S 2 . We have synthesized a least-violating controller C 2 for S 2 according to [START_REF] Girard | Least-violating symbolic controller synthesis for safety, reachability and attractivity specifications[END_REF]. It is shown in Figure 2, where the slices are computed at different values of v 1 : • The red line represents the target set X * in (20), and the white set represents the attractor of the closed-loop dynamics that is the closer to the target set as measured by distance H. All trajectories starting in this set stay there forever. • In the light grey set, all trajectories starting in this set will reach the attractor while still enforcing the strong safety requirements.

• The black set consists of the uncontrollable states from which the strong safety requirements cannot be guaranteed.

The implementation of the least-violating controller for system [START_REF] Mouelhi | Cosyma: A tool for controller synthesis using multi-scale abstractions[END_REF] is done through the controller C 1 defined in Proposition 4 which depends solely on the information of the observer. In Figure 3, we show a simulation of system (19) using the observer-based controller in the following scenario: the initial value of (d, v 2 , v 1 ) and ( d, v2 , v1 ) are (-50+ε 1 , 25+ ε 2 , 20+ε 3 ) and (-50, 25, 20), respectively. The leading vehicle (vehicle 1) drives at constant speed for the first 25s, then applies maximal deceleration until reaching minimal speed for the next 50s, and maximal acceleration until reaching maximal speed for the last 25s. The plots represent the evolution of the time headway, of the velocities of vehicle 2 and vehicle 1, the control input of vehicle 2 and estimation errors. The values of the target velocity v * and the target time headway ϑ * are represented by dashed lines in left side. Initially the time headway is greater than ϑ * so vehicle 2 regulates its speed around v * . After vehicle 1 decelerates, the time headway reduces and drops below ϑ * , then vehicle 2 stops regulating its speed to regulate its time headway around ϑ * . When vehicle 1 accelerates, the time headway increases again and becomes larger than ϑ * , then vehicle 2 restarts regulating its speed around v * . The error magnitudes never exceed their never exceed the bound values (ε 1 , ε 2 , ε 3 ), due to stability and reduce to the magnitude of the measurement noises δ 1 , δ 2 (white noise of magnitude 0.01) and the disturbance term w during the simulation. Numerically, | d(t)d(t)| ≤ 0.05, | v2 (t)v 2 (t)| ≤ 0.06, | v1 (t)v 1 (t)| ≤ 0.59 for all time. Note that the estimation error in v 1 is greater than other states, this is due to the effect of the disturbance w for which the observer cannot compensate between a time step and the next. We can see on the simulation that the system behaves as expected. The performance degradation of the observer-based controller compared to a state-based controller can be evaluated through the value ς = max t≥t s H(d(t), v 2 (t), v 1 (t)) , which is the maximal value reached by the distance function H after the trajectory reaches the attractor. In the simulation, ς = 1.8286 (observer) is reduced to 1.1 (state), which appears acceptable in view of the observer precision given by ε.

V. CONCLUSIONS

In this paper, an abstraction design which is related by a feedback refinement relation of the system formed with the plant and a chosen observer was proposed. This approach allows us to use results in the observer design from classical control theory, which covers a wide class of systems (linear and nonlinear), while being able to deal with complex specifications and disturbances. The controller refinement only requires feeding the obtained symbolic controller with the state estimate of the observer, which provides an output-feedback controller. An application to adaptive cruise control illustrates our results. Further investigations are necessary to cope with the transient behaviour of the observer before reaching the forward invariant set.

Fig. 1 .

 1 Fig.1. Transition relation F 2 defined in S 2 : if the estimation error between ξ and ξ is included in the ε-expansion of N η (q), then its effect on the dynamics F 0 under u is included in ε-expansion of F 0 (N η+ε (q), u).

Fig. 2 .

 2 Fig.2. Set of safety controllable states (white); set of states which will reach the white set (light grey); set of uncontrollable states (black).

Fig. 3 .

 3 Fig. 3. Simulated trajectories of system (19) using the observer-based controller: (left side) evolution of the time headway, of the velocities of vehicle 2 and vehicle 1 where the target time headway ϑ * and the values of the target velocity v * are represented by dashed lines; (right side) the control input of vehicle 2 and estimation errors between real and observer states.

The symbol refers to symmetric terms and I 3 is the identity matrix of dimension 3.