Antoine Girard
email: antoine.girard@l2s.centralesupelec.fr

Gregor Gössler

Safety Synthesis for Incrementally Stable Switched Systems using Discretization-Free Multi-Resolution Abstractions

Keywords: Multi-resolution abstraction, Simulation and bisimulation, Switched systems, Safety synthesis

Control of continuous and hybrid systems using discrete abstractions often suffers from scalability issues, due to the use of state space partitions as symbolic states. In this paper, for incrementally stable switched systems, we introduce a class of abstractions that do not rely on state space partitions but use mode sequences as symbolic states. Our approach differs from existing works by the possibility of considering sequences of varying length, giving the possibility to adjust locally the resolution of the abstraction. Temporal constraints on the switching signal can also be taken into account. We thus define multi-resolution bisimilar abstractions that enjoy interesting properties that can be used to design specific algorithms to synthesize safety controllers. These algorithms need not compute the full abstraction that is built incrementally during controller synthesis, exploring finer resolutions only when the specification cannot be enforced at the coarser level. We illustrate the approach by a numerical example inspired by road traffic regulation.

Introduction

Abstraction-based control is a computational approach to systems design where continuous dynamics are approximated by finite state dynamical systems, called discrete or symbolic abstractions (see e.g. [START_REF] Tabuada | Verification and control of hybrid systems -a symbolic approach[END_REF][START_REF] Belta | Formal methods for discrete-time dynamical systems[END_REF] and the references therein). The main advantage of using discrete abstractions is that they allow to leverage a set of algorithmic techniques for synthesizing controllers enforcing various specifications such as safety and reachability [START_REF] Maler | Control from computer science[END_REF] or those described by finite state automata [START_REF] Ramadge | Supervisory control of a class of discrete event processes[END_REF] or temporal logic formula [START_REF] Pnueli | On the synthesis of a reactive module[END_REF][START_REF] Piterman | Synthesis of reactive (1) designs[END_REF]. When the continuous dynamics and the discrete abstraction can be related by some formal behavioral relationship such as simulation, bisimulation and their alternating or approximate versions [START_REF] Tabuada | Verification and control of hybrid systems -a symbolic approach[END_REF][START_REF] Girard | Approximation metrics for discrete and continuous systems[END_REF][START_REF] Reissig | Feedback refinement relations for the synthesis of symbolic controllers[END_REF], controllers designed using the abstraction can be refined into controllers for the original system with formal guarantees of correctness. Most of the existing approaches for computing discrete abstractions are based on partitions or discretizations of the continuous state space [START_REF] Lunze | Qualitative modelling of linear dynamical systems with quantized state measurements[END_REF][START_REF] Caines | Hierarchical hybrid control systems: A lattice theoretic formulation[END_REF][START_REF] Raisch | Discrete approximation and supervisory control of continuous systems[END_REF][START_REF] Alur | Discrete abstractions of hybrid systems[END_REF][START_REF] Koutsoukos | Supervisory control of hybrid systems[END_REF][START_REF] Tabuada | Linear time logic control of discrete-time linear systems[END_REF][START_REF] Yordanov | Formal analysis of discrete-time piecewise affine systems[END_REF][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][START_REF] Zamani | Symbolic models for nonlinear control systems without stability assumptions[END_REF][START_REF] Liu | Finite abstractions with robustness margins for temporal logic-based control synthesis[END_REF][START_REF] Coogan | Finite abstraction of mixed monotone systems with discrete and continuous inputs[END_REF]. As these typically scale exponentially in the state space dimension, it is clear that these approaches, applied naively, are only suitable for low dimensional dynamics.

In the recent years, people have extensively worked on novel abstraction techniques that would allow to improve the scalability of the approach. For systems that consist of interconnected components, compositional techniques have been developed that first compute discrete abstractions of the components that can be composed to compute an abstraction of the full system [START_REF] Pola | Symbolic models for networks of control systems[END_REF][START_REF] Majumdar | Compositional synthesis of finite state abstractions[END_REF][START_REF] Hussien | Abstracting partially feedback linearizable systems compositionally[END_REF][START_REF] Meyer | Compositional abstraction and safety synthesis using overlapping symbolic models[END_REF][START_REF] Kim | Constructing control system abstractions from modular components[END_REF][START_REF] Swikir | Compositional synthesis of finite abstractions for networks of systems: A small-gain approach[END_REF] or that can be used to synthesize controllers for the components, e.g. using assume-guarantee contracts that enforce a correct behavior at the system level [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] Pola | Decentralized supervisory control of networks of nonlinear control systems[END_REF][START_REF] Saoud | Contract based design of symbolic controllers for interconnected multiperiodic sampled-data systems[END_REF]. Other works have explored the efficient encoding of discrete abstractions, e.g. using binary decision diagrams and the associated algorithms [START_REF] Rungger | Scaling up controller synthesis for linear systems and safety specifications[END_REF][START_REF] Bulancea | Nonuniform abstractions, refinement and controller synthesis with novel BDD encodings[END_REF], or exploiting sparsity in the continuous dynamics [START_REF] Gruber | Sparsity-aware finite abstraction[END_REF]. Multi-resolution, multi-scale and multi-layered abstractions, which can adapt locally the precision of the approximation have been developed in several works [START_REF] Tazaki | Discrete-state abstractions of nonlinear systems using multiresolution quantizer[END_REF][START_REF] Cámara | Synthesis of switching controllers using approximately bisimilar multiscale abstractions[END_REF][START_REF] Hsu | Multi-layered abstraction-based controller synthesis for continuous-time systems[END_REF] and are often used in combination with lazy controller synthesis algorithms that build the abstraction on-the-fly and adapt the precision to the level required for enforcing the specification [START_REF] Rungger | On-the-fly model abstraction for controller synthesis[END_REF][START_REF] Pola | Integrated design of symbolic controllers for nonlinear systems[END_REF][START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF][START_REF] Hsu | Lazy abstraction-based control for safety specifications[END_REF]. Finally, alternative abstraction techniques, which do not require the discretization of the state space but use input sequences as symbolic states, have been developed for systems enjoying an incremental stability property [START_REF] Corronc | Mode sequences as symbolic states in abstractions of incrementally stable switched systems[END_REF][START_REF] Girard | Approximately bisimilar abstractions of incrementally stable finite or infinite dimensional systems[END_REF][START_REF] Zamani | Symbolic models for stochastic switched systems: A discretization and a discretization-free approach[END_REF].

In this work, we present an approach that combines three features mentioned above. For incrementally stable switched systems, we develop an abstraction technique that does not need to discretize the state space. In our approach, symbolic states coincide with input sequences. However, unlike in [START_REF] Corronc | Mode sequences as symbolic states in abstractions of incrementally stable switched systems[END_REF][START_REF] Girard | Approximately bisimilar abstractions of incrementally stable finite or infinite dimensional systems[END_REF][START_REF] Zamani | Symbolic models for stochastic switched systems: A discretization and a discretization-free approach[END_REF], the length of the input sequences is not fixed and can be adapted. This results in multi-resolution bisimilar abstractions where longer or shorter input sequences correspond to finer or coarser resolutions, respectively. Temporal constraints on the switching signal can easily be taken into account in our approach. Then, for safety properties, we develop two controller synthesis algorithms that make it possible to compute the abstraction on-the-fly and only partially, by staying at the coarsest resolution required to enforce the specification. The first algorithm allows to recover the same controller as if the abstraction had been built exhaustively, while the second algorithm gives a less permissive controller but is much more efficient. Remarkably, the set of controllable initial states are the same using both algorithms.

Our synthesis approach has connections with the lazy safety synthesis approach developed in [START_REF] Hsu | Lazy abstraction-based control for safety specifications[END_REF] for multi-layered partition-based abstractions introduced in [START_REF] Hsu | Multi-layered abstraction-based controller synthesis for continuous-time systems[END_REF]: both approaches are sound and complete and the synthesized controllers give priority to transitions leading to coarser resolutions. However, in [START_REF] Hsu | Lazy abstraction-based control for safety specifications[END_REF] controllers are defined algorithmically, while we first provide mathematical characterizations of controllers and then present algorithms for their computation. Moreover, while the synthesis algorithm in [START_REF] Hsu | Lazy abstraction-based control for safety specifications[END_REF] is based on backward reachability computations our algorithms take advantage of the determinism of our abstractions to use forward reachability computations. This makes it possible to limit the exploration of the abstraction dynamics to states that are reachable from a specified set of initial states. On the flipside we focus on safety properties in this article, whereas [START_REF] Hsu | Multi-layered abstraction-based controller synthesis for continuous-time systems[END_REF] also considers reachability and generalized Büchi objectives.

The paper is organized as follows. In Section 2, we introduce the notions of multi-resolution transition systems and of multi-resolution abstraction. In Section 3, we instantiate these notions in the context of incrementally stable switched systems. In Section 4, we propose specific controller synthesis algorithms, which exploit the properties of multi-resolution abstractions, for safety properties. Finally, in Section 5, we show an application of our approach to a variant of the road traffic model from [START_REF] Corronc | Mode sequences as symbolic states in abstractions of incrementally stable switched systems[END_REF].

Notations

Z, Z + 0 , Z + , R, R + 0 and R + denote the sets of integers, nonnegative integers, positive integers, real numbers, non-negative real numbers and positive real numbers, respectively. Given two sets S 1 , S 2 and a relation R ⊆ S 1 × S 2 , we define the inverse relation as

R -1 = {(s 2 , s 1 ) ∈ S 2 × S 1 | (s 1 , s 2 ) ∈ R}; we denote R(s 1 ) = {s 2 ∈ S 2 | (s 1 , s 2 ) ∈ R} and for S 1 ⊆ S 1 , R(S 1 ) = s1∈S 1 R(s 1

Multi-resolution abstraction

In this section, we briefly present the general modeling formalism of transition systems and the associated abstraction framework based on (bi)simulation.

Then, we introduce the new notion of multi-resolution abstraction that we deal with in the paper.

Transition systems and (bi)simulation

Definition 1 A transition system is a tuple T = (X, U, ∆, X 0 ) consisting of:

a set of states X; -a set of inputs U ; -a transition relation ∆ ⊆ X × U × X; -a set of initial states X 0 ⊆ X.

The transition (x, u, x ) ∈ ∆ will be denoted x ∈ ∆(x, u); this means that the system can evolve from state x to state x under the input u. An input u ∈ U belongs to the set of enabled inputs at state x, denoted enab ∆ (x), if ∆(x, u) = ∅. The transition system is said to be non-blocking if for all x ∈ X, enab ∆ (x) = ∅. The transition system is said to be deterministic if for all x ∈ X and u ∈ enab ∆ (x), there exists a unique x ∈ ∆(x, u); in that case, we shall write with a slight abuse of notation x = ∆(x, u). In this paper, for the sake of simplicity, we only consider non-blocking and deterministic transition systems.

A trajectory of the transition system is a finite or infinite sequence of transitions, σ = (x 0 , u 0 )(x 1 , u 1 )(x 2 , u 2 ) . . . where u i ∈ enab ∆ (x i ), and x i+1 = ∆(x i , u i ), for all i = 0, 1, . . . ; it is initialized if x 0 ∈ X 0 . A state x ∈ X is reachable if there exists an initialized trajectory reaching x; the set of reachable states of T is denoted reach(T ).

In the following, we will consider abstraction relationships between transition systems in the sense of (bi)simulation [START_REF] Tabuada | Verification and control of hybrid systems -a symbolic approach[END_REF]:

Definition 2 Let T i = (X i , U i , ∆ i , X 0 i ), i = 1, 2
, be non-blocking and deterministic transition systems; R ⊆ X 1 × X 2 is said to be a simulation relation from T 1 to T 2 , if for all (x 1 , x 2 ) ∈ R,

∀u 1 ∈ enab ∆1 (x 1 ), ∃u 2 ∈ enab ∆2 (x 2 ), such that (x 1 , x 2 ) ∈ R where x 1 = ∆ 1 (x 1 , u 1 ), x 2 = ∆ 2 (x 2 , u 2 ).
R is said to be a bisimulation relation between T 1 and T 2 if R is a simulation relation from T 1 to T 2 and R -1 is a simulation relation from T 2 to T 1 . We say that T 2 simulates T 1 , denoted T 1 T 2 , if there exists a simulation relation R from

T 1 to T 2 such that X 0 1 ⊆ R -1 (X 0 2
). The transition systems T 1 and T 2 are said to be bisimilar, denoted

T 1 ∼ T 2 , if if there exists a bisimulation relation R between T 1 and T 2 such that X 0 1 ⊆ R -1 (X 0 2 ) and X 0 2 ⊆ R(X 0 1 ).
The notion of simulation relation leads to the following approximation result that is stated without proof, which is a straightforward consequence of Definition 2:

Proposition 1 Let T i = (X i , U i , ∆ i , X 0 i ), i = 1, 2
, be non-blocking and deterministic transition systems such that T 1 T 2 ; then for any initialized trajectory of T 1 , σ 1 = (x 0 1 , u 0 1 )(x 1 1 , u 1 1 ) . . . , there exists an initialized trajectory of

T 2 , σ 2 = (x 0 2 , u 0 2 )(x 1 2 , u 1
2 ) . . . , such that (x i 1 , x i 2 ) ∈ R, for all i = 0, 1, . . . Let us note that for bisimilar transition systems a symmetrical result holds as well (all trajectories of T 2 can be matched by trajectories of T 1 ).

Remark 1 We consider transition systems without outputs. If the transition systems are observed over a common set of outputs Y through output maps Θ i : X i → Y , i = 1, 2, notions of exact and approximate (bi)simulation relations [START_REF] Tabuada | Verification and control of hybrid systems -a symbolic approach[END_REF][START_REF] Girard | Approximation metrics for discrete and continuous systems[END_REF] can be recovered by adding the following conditions, respectively:

-If for all (x 1 , x 2 ) ∈ R, Θ 1 (x 1 ) = Θ 2 (x 2 ), then R is an exact (bi)simulation relation; -If for all (x 1 , x 2 ) ∈ R, d(Θ 1 (x 1 ), Θ 2 (x 2 )) ≤ ε where d is a metric on Y and ε ∈ R + 0 , then R is an approximate (bi)simulation relation. Remark 2
We consider deterministic transition systems for the sake of simplicity and because non-deterministic systems are not needed for the application to incrementally stable switched systems, which are considered in this paper. However, results presented in the paper can be extended to non-deterministic systems by resorting to the notion of alternating (bi)simulation relations [START_REF] Tabuada | Verification and control of hybrid systems -a symbolic approach[END_REF].

Multi-resolution abstraction

We now introduce the notion of multi-resolution abstraction, which we will deal with in the paper: Definition 3 Let T = (X, U, ∆, X 0 ) be a non-blocking and deterministic transition system, T is a multi-resolution transition system if X is equipped with a partial order X such that:

for all x ∈ X, u ∈ enab ∆ (x) and x = ∆(x, u), for all z, z ∈ X

(z X x) ∧ (x X z ) =⇒ ∃v ∈ enab ∆ (z), z = ∆(z, v).
for all x ∈ X 0 , for all z ∈ X, x X z =⇒ z ∈ X 0 .

Let us provide some discussion on the previous definition: x X z means that states x and z are related states at different resolutions (finer for x, coarser for z). Intuitively, the previous definition states that it is always possible to move from finer to coarser scales. The first item of the definition states that a transition can be matched by a transition starting from any related states at finer resolutions, and ending at any related states at coarser resolutions, as illustrated on Figure 1. The second item of the definition states that for all initial states, the related states at coarser resolutions are also initial. -T 1 is a multi-resolution transition system, and

Definition 4 Let T i = (X i , U i , ∆ i , X 0 i ), i = 1,
-T 1 T 2 or T 1 ∼ T 2 where the (bi)simulation relation R ⊆ X 1 × X 2 satisfies for all x, z ∈ X 1 , x X1 z =⇒ R(x) ⊆ R(z).
Hence, in a multi-resolution abstraction, the (bi)simulation relation R is consistent with the partial order X1 . In that case, x X1 z means that the abstract state x represents a subset of concrete states R(x), which is a subset of the concrete states R(z) represented by z. Hence, finer or coarser resolutions of T 1 correspond to more or less precise abstractions of T 2 , respectively.

In the next section, we will give a construction of bisimilar multi-resolution abstractions for a class of incrementally stable switched systems. Then, in Section 4, we will show how such abstractions can be used for efficient safety synthesis.

Multi-resolution abstractions of switched systems

In this section, we provide a construction of multi-resolution bisimilar abstractions for a class of switched systems, enjoying an incremental stability property.

In the following, a continuous function α : R + 0 → R + 0 is said to belong to class K if it is strictly increasing, and α(0) = 0. It is of class K ∞ if it is of class K and α(r) → +∞ when r → +∞. A continuous function β : R + 0 × R + 0 → R + 0 is said to belong to class KL if for all fixed s, the map r → β(r, s) belongs to class K and for all fixed r > 0, the map s → β(r, s) is strictly decreasing and β(r, s) → 0 when s → +∞.

Incrementally stable switched systems

We first introduce the class of switched systems under consideration, which is similar to that in [START_REF] Girard | Approximately bisimilar symbolic models for incrementally stable switched systems[END_REF].

Definition 5 A switched system is a quadruple Σ = (R n , P, P, F ), consisting of:

a state space R n ;

a finite set of modes P = {1, . . . , m}; -a set of switching signals P ⊆ S(R + 0 , P ), which denotes the set of piecewise constant functions from R + 0 to P , continuous from the right and with a finite number of discontinuities on every bounded interval of R + 0 ; -a collection of smooth vector fields F = {f p : R n → R n | p ∈ P }.

A continuous function x : R + 0 → R n is said to be a trajectory of Σ if there exists a switching signal p ∈ P such that, at each t ∈ R + 0 where the function p is continuous, x is continuously differentiable and satisfies:

ẋ(t) = f p(t) (x(t)).
We make the assumption that the vector fields f p are such that for all initial conditions x ∈ R n , for all switching signals p ∈ P, there exists a unique trajectory of Σ, denoted x(., x, p) or by x(., x, p) if p is constantly equal to p ∈ P .

The results presented in this section apply to switched systems satisfying the incremental stability property [START_REF] Angeli | A Lyapunov approach to incremental stability properties[END_REF][START_REF] Girard | Approximately bisimilar symbolic models for incrementally stable switched systems[END_REF]: Definition 6 A switched system Σ is incrementally globally uniformly asymptotically stable (δ-GUAS) if there exists a KL function β such that for all t ∈ R + 0 , for all x 1 , x 2 ∈ R n , for all switching signals p ∈ P, the following condition is satisfied:

x(t, x 1 , p) -x(t, x 2 , p) ≤ β( x 1 -x 2 , t).
Intuitively, a switched system is incrementally stable if the distance between trajectories associated with the same switching signal converges asymptotically to zero independently of their initial condition. This property is quite strong but can be found in several applications of interest such as power converters [START_REF] Girard | Approximately bisimilar symbolic models for incrementally stable switched systems[END_REF], thermal dynamics in buildings [START_REF] Pola | Decentralized supervisory control of networks of nonlinear control systems[END_REF] or road traffic networks [START_REF] Corronc | Mode sequences as symbolic states in abstractions of incrementally stable switched systems[END_REF]. Moreover, feedback control may be used to enforce incremental stability on other systems [START_REF] Zamani | Backstepping design for incremental stability[END_REF]. As shown in [START_REF] Girard | Approximately bisimilar symbolic models for incrementally stable switched systems[END_REF], incremental stability of a switched system can be characterized using Lyapunov functions:

Definition 7 A smooth function V : R n × R n → R +
0 is a common δ-GUAS Lyapunov function for Σ if there exist K ∞ functions α, α and κ ∈ R + such that for all x 1 , x 2 ∈ R n , and for all p ∈ P :

α( x 1 -x 2 ) ≤ V (x 1 , x 2 ) ≤ α( x 1 -x 2 ); (1) ∂V ∂x1 (x 1 , x 2 )f p (x 1 ) + ∂V ∂x2 (x 1 , x 2 )f p (x 2 ) ≤ -κV (x 1 , x 2 ). (2)
Theorem 1 [14] Consider a switched system Σ = (R n , P, P, F ) with a common δ-GUAS Lyapunov function, then Σ is δ-GUAS.

Let us remark that V given by

V (x 1 , x 2 ) = V (x 1 , x 2 ) + V (x 2 , x 1
) is also a δ-GUAS Lyapunov function. Hence, there is no loss of generality in assuming that V (x 1 , x 2 ) = V (x 2 , x 1 ), for all x 1 , x 2 ∈ R n . We would also like to point out that in Definition 7, V actually needs to be differentiable only at (

x 1 , x 2 ) ∈ R n × R n with x 1 = x 2 . Similarly, (2) needs to hold only for x 1 = x 2 .
Remark 3 For switched systems with affine dynamics (i.e. f p (x) = A p x + b p ), it is convenient to seek for δ-GUAS Lyapunov functions of the form

V (x 1 , x 2 ) = (x 1 -x 2 ) M (x 1 -x 2 ) (3)
where M is a symmetric positive definite matrix. Indeed, functions of that form can be computed by solving a set of linear matrix inequalities [START_REF] Girard | Approximately bisimilar symbolic models for incrementally stable switched systems[END_REF]. For non-affine dynamics, the problem of computing δ-GUAS Lyapunov functions becomes more involved. Theoretical tools such as matrix measures [START_REF] Maidens | Reachability analysis of nonlinear systems using matrix measures[END_REF] or contraction metrics [START_REF] Aylward | Stability and robustness analysis of nonlinear systems via contraction metrics and sos programming[END_REF] can help to obtain (state-dependent) linear matrix inequalities for incremental stability that are similar to those for affine dynamics.

In the case of polynomial dynamics of moderate dimension, such inequalities may be solved using sum of squares programming.

In the following sections, we will make the supplementary assumption on the δ-GUAS Lyapunov function that there exists

γ ∈ R + , γ ≥ 1, such that for all x 1 , x 2 , x 3 ∈ R n |V (x 1 , x 2 ) -V (x 1 , x 3 )| ≤ γV (x 2 , x 3 ). ( 4
)
Remark 4 Equation ( 4) can be interpreted as a relaxed triangular inequality, which needs to be satisfied by V . It should be noted that if V is of the form (3), then (4) holds with γ = 1, which coincides with the traditional triangular inequality. Otherwise, if the first order derivatives of V are bounded, since we will be working on compact domains C ⊆ R n , there is no loss of generality (see e.g. [START_REF] Girard | Approximately bisimilar symbolic models for incrementally stable switched systems[END_REF]) to assume that for all

x 1 , x 2 , x 3 ∈ C, |V (x 1 , x 2 ) -V (x 1 , x 3 )| ≤ γ x 2 -x 3 .
Then, assuming that for all r ∈ [0, r], α(r) ≥ c α r, where r = max x,y∈C xy , it follows that for all

x 1 , x 2 , x 3 ∈ C, |V (x 1 , x 2 ) -V (x 1 , x 3 )| ≤ γ c α V (x 2 , x 3 ).
Let Σ = (R n , P, P, F ) be a switched system where P = S(R + 0 , P ). We assume in the following that Σ is δ-GUAS and that there exists a common δ-GUAS Lyapunov function V satisfying (4).

Definition 8 Let τ ∈ R + be a time sampling parameter, the sampled dynamics of the switched system Σ is described by the transition system T τ (Σ) = (X, P, ∆ X , X 0 ) where:

the set of states is X = R n ; -the set of inputs is the set of modes P ; -the transition relation is given for x ∈ X, p ∈ P by x ∈ ∆ X (x, p) if and only if x = x(τ, x, p) i.e. the switched system moves from state x to state x by applying constant mode p for duration τ ; -the set of initial states is X 0 ⊆ R n .

T τ (Σ) is non-blocking and deterministic and its state space is uncountable. The set of initial states is intentionally left unspecified and will be subject of further discussions later.

Construction of the abstraction

We now describe the construction of symbolic abstractions approximating the transition system T τ (Σ). Our approach uses finite mode sequences as symbolic states as in [START_REF] Corronc | Mode sequences as symbolic states in abstractions of incrementally stable switched systems[END_REF][START_REF] Zamani | Symbolic models for stochastic switched systems: A discretization and a discretization-free approach[END_REF]. A noticeable difference with those work is that we consider sequences of variable length, as opposed to sequences of fixed length. Each length corresponding to a specific resolution of the abstraction, longer sequences corresponding to finer resolutions.

The symbolic states consist of mode sequences of varying length. Let N 1 , N 2 ∈ Z + , such that N 1 ≤ N 2 be the resolution parameters. In the following, we assume for simplicity that N 1 ≥ 2. Similar results hold for the case N 1 = 1 though technical proofs are slightly different. Let P [1,N2] = k=N2 k=1 P k denote the set of mode sequences of length smaller than or equal to N 2 . Let P [N1,N2] = k=N2 k=N1 P k denote the set of mode sequences of length ranging from N 1 to N 2 , clearly P [N1,N2] ⊆ P [1,N2] .

For w = (p 1 , . . . , p k ) ∈ P [1,N2] , let |w| = k denote the length of the sequence w, and let p w be the switching signal defined on the time interval [0, kτ ) by

p w (t) = p k-i , ∀t ∈ [iτ, (i + 1)τ ), i = 0, . . . , k -1.
Let us remark that the mode sequence w is applied backward in the switching signal p w : p k is applied first while p 1 is applied last.

Let x s ∈ R n be a source state, then let y : P [1,N2] → X be given by

y(w) = x(|w|τ, x s , p w ). (5)
Hence, y(w) is the unique state reached at time |w|τ , from the source state x s , by applying switching signal p w . In the abstraction, the symbolic state w will actually represent a set of concrete states defined as a neighborhood of y(w), which contains all the states that can be reached by the switched system from the source state x s , by applying any switching sequence, of any length, ending with p w . Formally, the symbolic abstraction is given by the transition system T

N 1 ≤ l ≤ min(k + 1, N 2 ) -the set of initial states is W 0 ⊆ P [N1,N2] .
As an illustration, a partial view of the transition relation of T

[N1,N2] τ (Σ) is shown in Figure 2. T [N1,N2] τ
(Σ) is non-blocking and deterministic and its state space is finite. Moreover, for all w ∈ W , (p, l)

∈ enab ∆ W (w) and w = ∆ W (w, (p, l)) it holds |w | = l and N 1 ≤ l ≤ min(|w| + 1, N 2 ).
Let us remark that the choice of the set of initial states remains open and will be discussed later.

(1, 1) (0, 0) (0, 1) (1, 0)

(0, 0, 1) (0, 1, 0) (1, 0, 1) (1, 1, 0) (0, 1, 0, 1) (1, 1, 0, 1) (0, 2) (0, 3) (0, 2) (0, 3) (0, 4) (1, 2) (1, 3) (1, 2) (1, 3) (1, 4) Fig. 2 Symbolic states of T [2,4] τ
(Σ) with P = {0, 1}; transitions initiating from the states (0, 1) and (1, 0, 1).

Bisimulation relation

In this section, we establish the existence of a bisimulation relation between the symbolic model T

[N1,N2] τ (Σ) and T τ (Σ).
Theorem 2 Let us assume that the switched system Σ admits a common δ-GUAS Lyapunov function V satisfying (4). Let us consider time sampling parameter τ ∈ R + , source state x s ∈ R n and resolution parameters

N 1 , N 2 ∈ Z + , with 2 ≤ N 1 ≤ N 2 . Let R ⊆ W × X be given by R = (w, x) ∈ W × X | V (x, y(w)) ≤ e -(|w|-N1)κτ 1 -e -κτ γη N1 (x s ) (6)
where

η N1 (x s ) = max w∈P N 1 ,p∈P V x(τ, y(w), p), y(∆ W (w, (p, N 1 ))) . (7)
Then, R is a bisimulation relation between T 2) and ( 6) that

V x , y(w ) = V x(τ, x, p), x(τ, y(w), p) ≤ e -κτ V x, y(w) ≤ e -κτ e -(|w|-N1)κτ 1 -e -κτ γη N1 (x s ) = e -(|w |-N1)κτ 1 -e -κτ γη N1 (x s ). ( 8
)
Then, (w , x ) ∈ R. Case 2: If |w | < |w| + 1, then w = (p, p 1 , . . . , p j ) with N 1 -1 ≤ j ≤ k -1. Let w i = (p, p 1 , . . . , p i ) for i = j, . . . , k, then w = w j and from (4)

V x , y(w ) = V x , y(w j ) ≤ V x , y(w k ) + γ k i=j+1
V y(w i ), y(w i-1 ) .

Since y(w k ) = x(τ, y(w), p), we get

V x , y(w ) ≤ V x(τ, x, p), x(τ, y(w), p) + γ k i=j+1 V y(w i ), y(w i-1 ) .
By ( 2) and ( 6) we get

V x , y(w ) ≤ e -κτ e -(|w|-N1)κτ 1 -e -κτ γη N1 (x s ) + γ k i=j+1
V y(w i ), y(w i-1 ) . ( 9)

By ( 2) and ( 7), we have for all i = j + 1, . . . , k, V y(w i ), y(w i-1 ) ≤ e -κ(i-N1)τ η N1 (x s ).

Hence, [START_REF] Coogan | Finite abstraction of mixed monotone systems with discrete and continuous inputs[END_REF] gives

V x , y(w ) ≤ e -(|w|+1-N1)κτ 1 -e -κτ γη N1 (x s ) + γ k i=j+1 e -κ(i-N1)τ η N1 (x s ). ≤ e -(|w|+1-N1)κτ 1 -e -κτ γη N1 (x s ) + e -(j+1-N1)κτ -e -(k+1-N1)κτ 1 -e -κτ γη N1 (x s ) ≤ e -(j+1-N1)κτ 1 -e -κτ γη N1 (x s ) = e -(|w |-N1)κτ
1e -κτ γη N1 (x s ).

Then, (w , x ) ∈ R. Thus, we have shown that for all (w, x) ∈ R, p ∈ P , x ∈ ∆ X (x, p) and w ∈ ∆ W (w, (p, l)), it holds (w , x ) ∈ R. Hence, it follows that R is a bisimulation relation between T [N1,N2] τ (Σ) and T τ (Σ).

Let us remark that when N 1 = N 2 , our approach encompasses those presented in [START_REF] Corronc | Mode sequences as symbolic states in abstractions of incrementally stable switched systems[END_REF][START_REF] Zamani | Symbolic models for stochastic switched systems: A discretization and a discretization-free approach[END_REF]. The concrete system T τ (Σ) and the abstract system T [N1,N2] τ (Σ) do not have output functions. Intuitively, the symbolic state w ∈ W is meant to represent all concrete states belonging to R(w) where R is given by [START_REF] Caines | Hierarchical hybrid control systems: A lattice theoretic formulation[END_REF]. Let us remark that R(w) is actually a neighborhood of the concrete state y(w) = x(|w|τ, x s , p w ), defined by level-sets of the δ-GUAS Lyapunov function V . The properties of the δ-GUAS Lyapunov function V are instrumental for the proof of Theorem 2 since they allow us to bound the set of reachable states from the neighborhoods R(w) as done e.g. in [START_REF] Girard | Approximately bisimilar symbolic models for incrementally stable switched systems[END_REF]. It is noticeable that the size of the neighborhoods, and thus the precision of approximation, is not uniform over all symbolic states but depends on |w|: shorter or longer sequences correspond to coarser or finer approximation resolutions respectively. The degree of precision that is gained when using longer sequences is directly related to the parameter κ, which quantifies the decay rate of the δ-GUAS Lyapunov function. Then, it appears that computing a good δ-GUAS Lyapunov function with decay rate as large as possible is important.

Remark 5

The precision also depends linearly on η N1 (x s ). Let us first investigate the dependency on parameter N 1 . For w = (p 1 , . . . , p N1 ) ∈ P N1 and p ∈ P , ∆ W (w, (p, N 1 )) = w = (p, p 1 , . . . , p N1-1 ). Then, by (2), we have that

V x(τ, y(w), p), y(∆ W (w, (p, N 1 ))) = V x(N 1 τ, x(τ, x s , p N1 ), p w ), x(N 1 τ, x s , p w ) ≤ e -N1κτ V x(τ, x s , p N1 ), x s .
It then follows that

η N1 (x s ) ≤ e -N1κτ η 0 (x s ) where η 0 (x s ) = max p∈P V x(τ, x s , p), x s . (10)
Hence, η N1 (x s ) can be made arbitrarily small, and thus the approximation arbitrarily precise (even at the coarsest level) by choosing N 1 large enough. Finally, the precision also depends on the choice of the source state x s : it can be optimized by minimizing η N1 (x s ) or η 0 (x s ) given by equations ( 7) and [START_REF] Dallal | On compositional symbolic controller synthesis inspired by small-gain theorems[END_REF], respectively (note that these are minimax optimization problems).

The systems T

[N1,N2] τ (Σ) and T τ (Σ) are approximately bisimilar if their sets of initial states can be related through R:

Corollary 1 Under the assumptions of Theorem 2, let us assume that

X 0 ⊆ R(W ). Let W 0 = R -1 (X 0 ), then T [N1,N2] τ (Σ) ∼ T τ (Σ).
Proof By definition W 0 ⊆ R -1 (X 0 ). Let x ∈ X 0 , it follows from X 0 ⊆ R(W ) that there exists w ∈ W such that (x, w) ∈ R. Then,

W 0 = R -1 (X 0 ) gives that w ∈ W 0 . Hence, X 0 ⊆ R(W 0 ). Therefore, T [N1,N2] τ (Σ) ∼ T τ (Σ).
The previous corollary provides constraints on the set of initial states of T τ (Σ) so that we can choose an adequate set of initial states for T [N1,N2] τ (Σ) and ensure approximate bisimilarity of the two systems. If these constraints are not met, one can always provide the following asymptotic approximation result:

Proposition 2 Under the assumptions of Theorem 2, for all trajectories of T τ (Σ), σ 1 = (x 0 , p 0 )(x 1 , p 1 ) . . . and all trajectories of T [N1,N2] τ (Σ), σ 2 = (w 0 , (p 0 , l 0 ))(w 1 , (p 1 , l 1 )) . . . , it holds for all i = 0, 1, . . .

V x i , y(w i ) ≤ e -(|w i |-N1)κτ 1 -e -κτ γ N1 η(x s ) + γe -iκτ V x 0 , y(w 0 ) .
Proof Consider the trajectory of T τ (Σ), σ1 = (x 0 , p 0 , ỹ0 1 )(x 1 , p 1 , ỹ1 1 ) . . . where x0 = y(w 0 ). Then, it follows from (2) that

V x i , xi ≤ e -iκτ V x 0 , x0 . (11)
Moreover, we have V x0 , y(w 0 ) = 0, which gives (w 0 , x0 ) ∈ R. From the proof of Theorem 2, it follows that (w i , xi ) ∈ R for all i = 0, 1, . . . . Then, from (4):

V x i , y(w i ) ≤ γV x i , xi + V xi , y(w i )
which, with ( 11) and ( 6), leads to the conclusion.

Prefix order and multi-resolution property

In this section, we show that T [N1,N2] τ (Σ) is a multi-resolution bisimilar abstraction in the sense of Definition 4. Let us define the partial order on W = P [N1,N2] defined by w W w if and only if w is a prefix of w: i.e. w = (p 1 , . . . , p k ) and w = (p 1 , . . . , p k ) and with k ≤ k.

Lemma 1 Under the assumptions of Theorem 2, with R given by ( 6), for all w, w ∈ P [N1,N2] , if w W w, then R(w) ⊆ R(w).

Proof Let w, w with w W w, then w = (p 1 , . . . , p j ) and w = (p 1 , . . . , p j ) with j ≤ j. If j = j , then w = w and the conclusion is obvious. If j < j, let x ∈ R(w) and w i = (p 1 , . . . , p i ) for j ≤ i ≤ j. Then from ( 4) and ( 6), we have V x, y(w) = V x, y(w j ) ≤ V x, y(w j ) + γ j i=j +1

V y(w i ), y(w i-1 )

≤ V x, y(w) + γ j i=j +1 V y(w i ), y(w i-1 ) ≤ e -(|(w|-N1)κτ 1 -e -κτ γη N1 (x s ) + γ j i=j +1
V y(w i ), y(w i-1 ) . ( 12)

By ( 2) and ( 7), we have for all i = j + 1, . . . , j, V y(w i ), y(w i-1 ) ≤ e -κ(i-N1-1)τ η N1 (x s ).

Hence, [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF] gives

V x, y(w) ≤ e -(|(w|-N1)κτ 1 -e -κτ γη N1 (x s ) + γ j i=j +1
e -κ(i-N1-1)τ η N1 (x s ).

≤ e -(|w|+1-N1)κτ 1 -e -κτ γη N1 (x s ) + e -(j -N1)κτ -e -(j-N1)κτ 1 -e -κτ γη N1 (x s ) ≤ e -(j-N1)κτ 1 -e -κτ γη N1 (x s ) = e -(|w|-N1)κτ
1e -κτ γη N1 (x s ).

Then, from ( 6), x ∈ R(w).

An interpretation of the previous result can be given as follows. Intuitively, the symbolic state w represents the set of states that are reachable by the switched system from the source state x s by applying any switching sequences ending with p w . Thus, if w W w, a switching sequence ending with p w also ends with p w , it is therefore consistent that states represented by symbolic state w are also represented, at a different scale by w, and hence R(w) ⊆ R(w). Let us remark that properties of the δ-GUAS Lyapunov function are again instrumental for the proof of Lemma 1.

Theorem 3 Under the assumptions of Theorem 2 and Corollary 1, T

[N1,N2] τ (Σ) is a multi-resolution bisimilar abstraction of T τ (Σ).
Proof Firstly, it is straightforward to check from the definition of ∆ W that the first item of Definition 3 holds. Then, let w ∈ W 0 = R -1 (X 0 ), then R(w) ∩ X 0 = ∅. Then, for all w ∈ W such that w W w we have by Lemma 1 that R(w) ⊆ R(w) and hence R(w) ∩ X 0 = ∅, which gives w ∈ W 0 . Thus, the second item of Definition 3 holds as well and T The properties of the symbolic abstraction stated in Theorem 2, Lemma 1 and Theorem 3 are illustrated in Figure 3 3.5 Switched systems with constrained switching In this section, we show how to consider constraints on the set of admissible switching signals of the switched system. Particularly, we focus on infinite switching sequences generated by a transition system A = (Q, P, ∆ Q , Q 0 ) where the set of states Q is finite and the set of inputs is the set of modes P .

(0, 1) y(0, 0) y(0, 0, 1)

y(1, 0) y(1, 0, 1)

Symbolic states

Concrete states

(0, 0) (1, 0) (0, 0, 1) (1, 0, 1) (0, 2) (1, 2) (0, 3) (1, 3) y(0, 1) ∆ X (x, 0) ∆ X (x, 1)
x Fig. 3 Illustration of the different properties of the symbolic abstraction T

[2,3] τ (Σ) with P = {0, 1}. Left: symbolic transitions initiating from symbolic state (0, 1); Right: corresponding transitions in the concrete state space, the neighborhoods are related to symbolic states of the same color. If x ∈ R(0, 1), then ∆ X (x, 0) ∈ R(0, 0, 1) ⊆ R(0, 0) and

∆ X (x, 1) ∈ R(1, 0, 1) ⊆ R(1, 0).
The sampled dynamics of switched system Σ where switching sequences are constrained by transition system A can then be described by the composed transition system T τ (Σ)||A = (X ×Q, P, ∆ X×Q , X 0 ×Q 0 ) where the transition relation is formally given for (x, q), (x , q ) ∈ X × Q, p ∈ P by (x , q ) ∈ ∆ X×Q ((x, q), p) ⇐⇒ x ∈ ∆ X (x, p) ∧ q ∈ ∆ Q (q, p).

Similarly, we can define the composition of the symbolic abstraction T [N1,N2] τ

(Σ) with transition system A as the composed transition system T

[N1,N2] τ (Σ)||A = (W × Q, P , ∆ W ×Q , W 0 × Q 0 )
where the transition relation is formally given for (w, q), (w , q ) ∈ W × Q, (p, l) ∈ P by (w , q ) ∈ ∆ W ×Q ((w, q), (p, l)) ⇐⇒ w ∈ ∆ W (w, (p, l)) ∧ q ∈ ∆ Q (q, p).

The partial order on W can be naturally lifted to W × Q as follows:

(w, q) W ×Q (w, q) ⇐⇒ w W w ∧ q = q.

Let us remark that if q = q, then the states (w, q) and (w, q) are incomparable.

Then, the following result is a direct consequence of Theorems 2 and 3 and Corollary 1:

Corollary 2 Under the assumptions of Theorem 2 and Corollary 1, let R ⊆ W × Q × X × Q be given by R = {(w, q 1 , x, q 2 ) ∈ W × Q × X × Q | (w, x) ∈ R ∧ q 1 = q 2 } . Then, R is a bisimulation relation between T [N1,N2] τ (Σ)||A and T τ (Σ)||A. T [N1,N2] τ (Σ)||A is a multi-resolution bisimilar abstraction of T τ (Σ)||A.

Safety synthesis using multi-resolution abstractions

In this section, we show how multi-resolution abstractions can be used for safety synthesis. For efficiency, we do not explore nor compute the abstract transition relation exhaustively but adaptively during controller synthesis. The exploration should favor abstract states at coarser resolutions in order to keep the number of explored states as small as possible. Abstract states at finer resolutions are only explored when all related states at coarser resolutions are unsafe.

Problem formulation

Let T i = (X i , U i , ∆ i , X 0 i ), i = 1, 2, be non-blocking and deterministic transition systems such that T 1 is a multi-resolution abstraction of T 2 . Let R ⊆ X 1 × X 2 be the (bi)simulation relation between T 1 and T 2 , and let

X s 2 ⊆ X 2 denote a subset of safe states of T 2 . Let X s 1 = {x 1 ∈ X 1 | R(x 1 ) ⊆ X s 2 }
be the associated set of safe states of T 1 . Let us remark that by Definition 4, we have

∀x ∈ X s 1 , ∀z ∈ X 1 , z X1 x =⇒ z ∈ X s 1 . (13)
In the rest of the section, we only deal with transition system T 1 , so to simplify the notation the index will be dropped:

T 1 = T = (X, U, ∆, X 0 ), X s 1 = X s and X1 = X . For a subset X ⊆ X, the set of maximal elements of X is given by max (X ) = X \ {x ∈ X | ∃x ∈ X , x ≺ x }. The lower sets of X are given by low (X ) = {x ∈ X | ∃x ∈ X , x x } and low ≺ (X ) = {x ∈ X | ∃x ∈ X , x ≺ x }. Definition 9 X ⊆ X s is a safe invariant set of T if ∀x ∈ X , ∃u ∈ enab ∆ (x), such that x ∈ X where x = ∆(x, u). ( 14
)
Starting from an initial state x 0 ∈ X , one can then generate infinite trajectories of T , σ = (x 0 , u 0 )(x 1 , u 1 ) . . . , such that x i ∈ X , for all i ≥ 0.

Maximal safe invariant

There exists in general several safe invariant sets, however, it is well known that there exists one that is maximal (see e.g. [START_REF] Ramadge | Supervisory control of a class of discrete event processes[END_REF][START_REF] Tabuada | Verification and control of hybrid systems -a symbolic approach[END_REF]):

Lemma 2 There exists a unique safe invariant set X * ⊆ X s such that for all safe invariant sets X ⊆ X s , X ⊆ X * .

X * is called the maximal safe invariant set of T . The computation of the maximal safe invariants set generally requires the full exploration of the transition relation. However, a partial exploration is possible by exploiting the multiresolution property of transition system T . Let us consider the set X # ⊆ X given by:

X # = max X (X * ). ( 15
)
Then, the following result holds:

Lemma 3 X # is a safe invariant set of T .

Proof Firstly, we have X # ⊆ X * ⊆ X s . Secondly, let x ∈ X # , then x ∈ X * and since X * is a safe invariant set, there exists u ∈ enab ∆ (x) such that x ∈ X * where x = ∆(x, u). From ( 15), there exists z ∈ X # , such that x X z (note that we may have x = z ). Then, from Definition 3, there exists v ∈ enab ∆ (x) such that z = ∆(x, v). Hence, equation ( 14) holds.

The following result shows that the maximal safe invariant set X * can be easily obtained from X # :

Theorem 4 X * = low X (X # ).
Proof Firstly, by definition of maximal elements and lower sets and by [START_REF] Gruber | Sparsity-aware finite abstraction[END_REF], the following inclusions hold:

X * ⊆ low X (max X (X * )) = low X (X # ).
Let us now show that low X (X # ) is a safe invariant set. Let z ∈ low X (X # ), then there exists x ∈ X # such that z X x. Since x ∈ X # ⊆ X s , by ( 13), we get that z ∈ X s . By Lemma 3, there exists u ∈ enab ∆ (x), such that x ∈ X # where x = ∆(x, u). From Definition 3, there exists v ∈ enab ∆ (z) such that x = ∆(z, v). Hence, equation ( 14) holds. Therefore, low X (X # ) is a safe invariant set. By maximality of X * , it follows that low X (X # ) ⊆ X * . Thus, one can see that to compute the maximal safe invariant set X * , it is actually sufficient to compute X # . Let us now define the controlled transition system T # = (X # , U, ∆ # , X 0# ) where the set of initial states is given by X 0# = X 0 ∩ X # , and the transition relation is given for all x ∈ X # and u ∈ U by

u ∈ enab ∆ # (x) ⇐⇒ (u ∈ enab ∆ (x) ∧ ∆(x, u) ∈ X # )
and for all u ∈ enab ∆ # (x), ∆ # (x, u) = ∆(x, u). We then have Proposition 3 The transition system T # satisfies the following properties:

-All trajectories of T # are trajectories of T ; -The set of reachable states reach(T # ) is a subset of the safe invariant X # ; -T # is non-blocking and deterministic.

Proof The first two items are direct consequence of the definition of T # . Moreover T # is deterministic because T is deterministic. Finally, since X # is a safe invariant set of T , it follows from Definition 9 and the definition of the transition relation ∆ # that for all x ∈ X # , there exists u ∈ enab ∆ # (x). Hence, T # is non-blocking.

Hence T # allow generating safe and infinite trajectories of T . Let us remark that to characterize T # it is not necessary to compute X # , it is actually sufficient to compute reach(T # ). Let us remark that reach(

T # ) = X # if X 0 = X. (0, 0) (0, 0, 0) (0, 0 , 1) (0, 1, 0) (1, 3)
(0, 2) (0, 2) (0, 2) (0, 3) (0, 3) (0, 2) (0, 3) (0, 3) (1, 3) (1, 0, 0) (1, 3) (0, 3) (0, 0) (0, 1, 0) (1, 3) (0, 2) (0, 2)
(1, 0, 0) (0, 3) Fig. 4 Illustration of the different notions of invariants for symbolic abstraction T [2,3] τ (Σ) with P = {0, 1} and safety specification X s = {(0, 0), (0, 0, 0), (0, 0, 1), (0, 1, 0), (1, 0, 0), (1, 1, 0)}. Top: maximal safe invariant X * and associated safe transitions (note that (1, 1, 0) / ∈ X * ); Bottom: safe invariant X # , the four transitions belong to ∆ # , only the three plain transitions belong to ∆ .

Maximal coarsest safe invariant

In this section, we consider further complexity reduction. Let us assume that X is equipped with a total pre-order X ⊆ X × X which is consistent with the partial order X in the sense that for all x, z ∈ X such that x X z we have x X z. Intuitively, while x X z means that states x and z are related at finer and coarser resolutions, x X z means that x lies at a finer resolution than z but they don't need to be related. For instance, for symbolic states given by sequences of variables length, as in our construction, x X z means that z is a prefix of x, while x X z means that the z is shorter than x.

Let us now define the transition system T , obtained by selecting transitions of T # that end at the coarsest possible scale. Formally, T = (X # , U, ∆ , X 0# ) where the transition relation is given for all x ∈ X # and u ∈ U by

u ∈ enab ∆ (x) ⇐⇒ u ∈ enab ∆ # (x)∧ ∀v ∈ enab ∆ # (x), ∆(x, v) X ∆(x, u)
and for all u ∈ enab ∆ (x), ∆ (x, u) = ∆(x, u). By construction, T inherits the properties of T # stated in Proposition 3. Let us remark also that to characterize T it is not necessary to compute X # , it is actually sufficient to compute reach(T ).

The different notions of invariants presented in this section are illustrated in Figure 4. In the next section, we present algorithms for the computation of reach(T # ) and reach(T ).

Algorithms

The synthesis problems we consider are thus: given a (concrete) state space X 2 , a safe set X s 2 ⊆ X 2 , a multi-resolution transition system T = (X, U, ∆, X 0 ) with partial order relation X ⊆ X × X, and a bisimulation relation R ⊆ X × X 2 as in Definition 4, -synthesize the safe invariant set reach(T # ); -synthesize the coarsest safe invariant set reach(T ).

The synthesis algorithm for the reachable states reach(T # ) (if coarse = false) and reach(T ) (if coarse = true) is shown in Algorithm 1. It calls function explore in Algorithm 2 for the initial states X 0 , starting from the coarsest level, and keeps refining each state x as long as it has neither found to be controllable (that is, explore returned false) nor unsafe (line 9). At each call to explore, the set of states visited so far is contained in

X c ∪ X u1 ∪ low X (X u2 ) ∪ X v
, where X c is the set of controllable states. X u1 is a set of uncontrollable states of type 1, for which some related states at finer resolutions may be controllable. X u2 is a set of uncontrollable states of type 2, for which all related states at finer resolutions are uncontrollable. Hence, it is sufficient to store only the maximal elements among the uncontrollable states of type 2. Finally, X v is the set of states visited along one path from some initial state in X 0 to (excluding) the current state x.

The function call explore(x, X v ) returns whether state x is controllable. A state x is controllable if it has an immediate controllable successor x (line 18 of Algorithm 2), in that case x and all states in X v are added recursively to X c (line 20); or Algorithm 1: Computation of reach(T # ) or of reach(T ) it has already been found to be controllable (i.e., x ∈ X c ), or it has been visited along the current path X v (i.e. x ∈ X v ) (line 3) -hence, lying on a cyclic path of safe states, in that case all states in X v are added recursively to X c .

Input: transition system T = (X, U, ∆, X 0 ), safe set X s 2 ⊆ X 2 , partial order X ⊆ X × X, bisimulation relation R ⊆ X × X 2 Output: controllable states X c ⊆ X 1 Global variables: X c , X u 1 , X u 2 ⊆ X 2 Local variable: todo ⊆ X (set of states to be explored) 3 Invariant I: ∀x ∈ X c ∀x ∈ X : x ≺ x =⇒ x ∈ X u 1 4 begin 5 (X c , X u 1 , X u 2 , todo) := (∅, ∅, ∅, max X 0 ) ; 6 for x ∈ todo do 7 todo := todo \ {x} ; 8 if ¬explore(x, ∅) then 9 todo := todo ∪ max X X 0 ∩ low≺ X ({x}) \ low X (X u 2 ) 10 return X c f oundSucc := false ; 12 todo := u∈U ∆(x, u) \ low X (X u 2 ) ∪ X u 1 ; 13 while todo = ∅ ∧ ¬(coarse ∧ f oundSucc) do
In contrast, x is determined to be uncontrollable if

it has been found to be uncontrollable before (line 5), or if R(x) intersects (type 1) or is contained (type 2) in the unsafe set (line 8); or -all its successors are uncontrollable. Refinement is needed (type 1) if some successor x of x is itself in X u1 (line 29); otherwise it is added to X u2 (line 31).

Hence, at the end of each call to explore, the sets X c , X u1 and low X (X u2 ) contain all the controllable states, states that are uncontrollable or to be refined, and unsafe states, respectively, that have been explored. Let us remark that explore involves some computation in the concrete state space (only at lines 7 and 8). In the case of switched systems, these two tests involve checking containment or intersection of the level sets of the δ-GUAS Lyapunov functions with the safe set X s 2 . In particular, if the δ-GUAS Lyapunov function is of the form (3) and X s 2 is a polytope or an ellipsoid, these operations can be performed efficiently. It is also possible to perform these tests conservatively using over-approximations of R(x). In this case, the algorithm remains sound (it computes a safe invariant), however the relation to the maximal safe invariant may be lost.

Proposition 4 Given a symbolic multi-resolution abstraction T # , the result of Algorithm 1 is reach(T # ) if coarse = false and reach(T ) otherwise. Algorithm 1 is guaranteed to terminate if T # (resp. T ) is finite.

Proof Let T = (X, U, ∆, X 0 ) be a symbolic multi-resolution abstraction with safe states X s .

We first show that X c is a safe invariant with respect to X s . For all x ∈ X c , safety with respect to X s follows from the fact that condition R(x) ⊆ X s 2 holds in line 20. Invariance of safety under ∆ is ensured by the fact that a state is added to X c in line 20 only if it has a successor in X c ∪ X v .

Next we prove invariance of I as defined in line 3 of Algorithm 1. Clearly, I holds by vacuity after the initialization in line 5 of Algorithm 1. Let x ∈ X c . The loops of Algorithm 2 (lines 13 and 16) explore trajectories through the successor states x of x under all inputs, provided that x has not been recognized as unsafe yet, visiting maximal successors first (line 16). Whenever a state x is safe but not controllable, the next finer abstraction is explored. Hence, if x ∈ X c then all strictly coarser states x with x ≺ x have been explored and added to X u1 (line 29) as none of them is controllable.

We now show, for coarse = false, that X c is the maximal safe invariant of T # , that is, X c = reach(T # ). Since in Algorithm 1, function explore is called on the initial states in max (X 0 ) with increasing refinement until each initial state is either found to be controllable, uncontrollable, or unsafe, it follows [START_REF] Alur | Discrete abstractions of hybrid systems[END_REF] with invariant I that X c ⊆ X # and (2) that X c is the maximal reachable set satisfying this condition. Therefore, X c = reach(X # ).

The proof that X c = reach(T ), for coarse = true, is similar, with explore being called only if no coarser controllable successor has been found before (line 13). The claim then follows from the unicity of X .

If X is finite, termination follows from the fact that the body of explore (lines 11 to 25) is executed at most once for each element x of X.

Application to a Road Traffic Model

We apply our approach to a variant of the road traffic model from [START_REF] Corronc | Mode sequences as symbolic states in abstractions of incrementally stable switched systems[END_REF]. The model Σ of a road, divided in 5 sections with 3 entrances and 2 exits, is illustrated in Fig. 5. The entrances to sections 1 and 4 are controlled by traffic lights f 1 and f 2 respectively, that enable (green light) or not (red light) the vehicles to pass. In Σ, the dynamic we want to observe is the density of traffic ϕ i , given in vehicles per section, for each section i of the road. The state of Σ is the 5-dimensions vector x = (ϕ 1 , ϕ 2 , ϕ 3 , ϕ 4 , ϕ 5 ) and its set of modes is P = {0, 1, 2, 3} where:

mode 0 means both lights red; -mode 1 means f 1 green and f 2 red; -mode 2 means f 1 red and f 2 green; -mode 3 means both lights green. Let l i be the length of section i in kilometers (km) and v i be the flow speed of the vehicles in kilometers per hour (km/h). Inspired by the work of [START_REF] De | Graph constrained-CTM observer design for the Grenoble south ring[END_REF], the model of a simple section (sections 3 and 5) is described by: φi

= - v i l i ϕ i + v i-1 l i-1 ϕ i-1
For sections 1 and 4 add the number of vehicles that can enter, and for section 2 subtract the number of vehicles that can exit. For equal section lengths l and speed v in all sections, the system dynamics in mode p are given by φ = A p ϕ + b p where One can find a δ-GUAS Lyapunov function V for Σ of the form (3) where the corresponding matrix is The results of our algorithm for several specifications are summarized in Table 1. Specifications are a conjunction of an upper bound on the traffic density of the form ∀i : x i ≤ b and a behavioral specification. The behavioral specification "lights red ≤ 1 t.u." means that mode 0 (resp. mode 1, mode 2) must be followed immediately by mode 3 (resp. mode 2 or 3, mode 1 or 3). The columns "lengths" indicate the effective lengths, contained in [N 1 , N 2 ], of mode sequences in X # and X , respectively. All computations were performed on an Intel Core i7-4770 with 16GB RAM. We are interested in extracting, from the cycles in T , schedules that satisfy some optimality criterion. We consider two measures. Let γ = (p 1 , ..., p kγ ) be the sequence of modes labeling some cycle and let θ i (γ) = kγ j=1 c i (p j )/k γ be the average throughput at entrance i ∈ {1, 2}, where c j (p) indicates whether lights of entrance j are green in mode p, that is, c 1

A 0 = A 1 = A 2 = A 3 =     -v l 0 0 0 0 v l -v l 0 0 0 0 r 3 × v l -v l 0 0 0 0 v l -v l 0 0 0 0 v l -v l     and b 0 = [r 0 0 0 0 0] , b 1 = [r 0 + r 1 0 0 0 0] , b 2 = [r 0 0 0 r 4 0] ,
M =    
(0) = c 2 (0) = c 1 (2) = c 2 (1) = 0 and c 1 (1) = c 2 (2) = c 1 (3) = c 2 (3) = 1.
Thus, the total average throughput during cycle γ is C 1 (γ) = θ 1 (γ) + θ 2 (γ) and the worst average throughput over both entrances is C 2 (γ) = min{θ 1 (γ), θ 2 (γ)}. Table 2 exhibits, for each of the specifications of Table 1, a cycle maximizing C 1 and C 2 , respectively, and its cost.

Among the synthesized maximal coarsest safe invariant sets, the best average throughput is obtained with the schedule (1, 2, 3, 2, 1, 2, 3, 2, 1, 2) and the best minimal throughput with schedule (1, 2). Figure 6 shows the traffic densities for the former schedule. Let us now apply our approach to a higher-dimensional model, a circular peripherial highway divided in 20 segments, as illustrated in Figure 7. The road has 4 entrances, each controlled by traffic lights, and 4 exits.

The state of the model is given by a 20-dimensional vector x = (ϕ 1 , ϕ 2 , ..., ϕ 20 ) of traffic densities and the set of modes is P = {0, 1, ..., 15} where each mode is the binary encoding of the states of the traffic lights:

mode 0 means (red, red, red, red); -mode 1 means (red, red, red, green); -mode 15 means (green, green, green, green).

As above, the dynamics for a simple segment i without entrance or exit is given by φi = - For the segments with an entrance add the number of vehicles that can enter, and for the segments with an exit subtract exit flow. We assume the relative exit rates of the four exits to be 0.2, 0.5, 0.3, and 0.1, respectively. For equal segment lengths i = 100m and speed v i = 70km/h in all segments, the system dynamics in mode p are given by φ = A p x + b p where A 0 = A 1 = ... = A 15 = (a ij ) ∈ R 20×20 where [START_REF] Alur | Discrete abstractions of hybrid systems[END_REF][START_REF] Kim | Constructing control system abstractions from modular components[END_REF] 0 otherwise

v i l i ϕ i + v i-1 l i-1 ϕ i-1
a ij =    -v i / i if i = j v i / i × (1 -out j ) if j = i -1 ∨ (i, j) =
where out 1 = 0.2, out 4 = 0.5, out 11 = 0.3, out 14 = 0.1, and out i = 0 for i / ∈ {1, 4, 11, 14}. Furthermore let b i = 3600 × bin(i) where bin i is the binary representation of i with bin(0) = (0 0 0 0), bin(1) = (0 0 0 1), ..., bin(15) = (1 1 1 1), modeling the rate of each entrance as 1 vehicle per second when the lights are green.

Again one can find a δ-GUAS Lyapunov function V of the form (3) for our model. Following Remark 5 we determine the source point as x s = [9.78, 10.40, ..., 9.78]. We take [N 1 , N 2 ] = [START_REF] Belta | Formal methods for discrete-time dynamical systems[END_REF][START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF] and require the specification consisting of an upper bound of 14 on the traffic density in each segment, and a behavioral specification modeling progress and fairness. More precisely, we forbid mode 0 in which all lights are red; furthermore, none of the traffic lights must stay red during more than one time unit. The controller synthesis of X converges in 3.9 s, yielding 10413 controllable states of lengths in [START_REF] Bulancea | Nonuniform abstractions, refinement and controller synthesis with novel BDD encodings[END_REF][START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF], from which two optimal cycles with respect to the criteria discussed above can be extracted: (green, green, red, green), (red, red, green, red) and (green, red, red, green), (red, green, green, red) . For the same parameters, the computations of X * and X # did not terminate within ten minutes.

Conclusion

In this paper we presented an approach for safety synthesis for a class of switched systems. The main contributions can be summarized as follows. Firstly, we introduced general notions of multi-resolution transition systems and of multi-resolution (bi)similar abstractions. Secondly, we have shown how such abstractions can be computed for incrementally stable switched systems, possibly with constrained switching signals. Thirdly, we have shown that the multi-resolution structure can be exploited to define two particular safety controllers, which keep the state of the abstraction at the coarsest possible resolution, and that are as good as the maximal safety controller in term of controllable initial states. Algorithms to synthesize these controllers are presented, where the abstractions need not be computed a priori but are generated on the fly during the synthesis: transitions to finer resolutions are only computed when safety cannot be ensured at the coarser level. Examples inspired by road traffic regulation show the effectiveness of the approach.

In future work, we will work towards the development of synthesis algorithms for non-deterministic abstractions, as the algorithms presented in Section 4.2 exploit the determinism of the abstraction. Extending such approaches beyond safety properties, e.g. for reachability or properties that can be expressed in linear temporal logic, are also a challenging problem that requires further research.

2 ,Fig. 1

 21 Fig.1Properties of the transition relation in a multi-resolution system: existence of the solid transition implies the existence of the dashed transitions.

[

  N1,N2] τ (Σ) = (W, P , ∆ W , W 0 ) where the set of states is W = P [N1,N2] ; -the set of inputs is the set of modes P = P × {N 1 , . . . , N 2 }; -the transition relation is given for w = (p 1 , . . . , p k ) ∈ W , (p, l) ∈ P by w ∈ ∆ W (w, (p, l)) if and only if w = (p, p 1 , . . . , p l-1 ) and

[

  N1,N2] τ (Σ) and T τ (Σ). Proof Let (w, x) ∈ R, with w = (p 1 , . . . , p k ), p ∈ P , and let x ∈ ∆ X (x, p) and w ∈ ∆ W (w, (p, l)). We consider two different cases depending on the value of l and thus of |w |. Let us recall that N 1 ≤ |w | ≤ min(|w| + 1, N 2 ). Case 1: If |w | = |w|+1, then w = (p, p 1 , . . . , p k ) and y(w ) = x(τ, y(w), p). It follows from (

[

  N1,N2] τ (Σ) is a multiresolution transition system. Secondly, from Theorem 2 and Corollary 1, we have T [N1,N2] τ (Σ) ∼ T τ (Σ), which together with Lemma 1 gives that the second item of Definition 4 holds.

14 m 25 needRef := true 26 if foundSucc then 27 return true 28 if needRef then 29 X 31 X

 142526282931 := max X (todo) ; 15 needRef := false; 16 for x ∈ m do17todo := todo \ {x } ; 18 if explore(x , X v ∪ {x}) then 19 todo := todo \ low X ({x }) ; 20 X c := X c ∪ {x} ; 21 f oundSucc := true 22 else if x ∈ low X (X u 2 ) then 23 todo := todo \ low X ({x }) 24 else if x ∈ X u 1 then u 1 := X u 1 ∪ {x} 30 else u 2 := X u 2 ∪ {x} 32 return false

Fig. 5

 5 Fig.5Model Σ of a road divided into 5 sections with 2 entrances and 2 exits.

and b 3 =

 3 [r 0 + r 1 0 0 r 4 0] . Take r 3 = 0.5 and r 0 = r 1 = r 4 = 5000 (in vehicles per hour).

Fig. 6

 6 Fig.6Traffic densities (solid blue) and upper bound (dashed red) on the five road segments for schedule (1, 2, 3, 2, 1, 2, 3, 2, 1, 2).

Fig. 7

 7 Fig. 7 Model Σ of a road divided into 20 segments with 4 entrances and 4 exits.

  (ii) for all s 1 , s 2 , s 3 ∈ S, s 1 s 2 and s 2 s 3 implies s 1 s 3 ; (iii) for all s 1 , s 2 ∈ S, s 1 s 2 or s 2 s 1 .

). Given a set S, a relation ⊆ S × S, is a partial order if and only if: (i) for all s ∈ S, s s; (ii) for all s 1 , s 2 , s 3 ∈ S, s 1 s 2 and s 2 s 3 implies s 1 s 3 ; (iii) for all s 1 , s 2 ∈ S, s 1 s 2 and s 2 s 1 implies s 1 = s 2 . s 1 s 2 and s 1 = s 2 is denoted s 1 ≺ s 2 . A relation ⊆ S × S is a total pre-order if and only if: (i) for all s ∈ S, s s;

  As for the choice of the source point x s as discussed in Remark 5, we use the fminimax Matlab function that providesx s = [26.7857 26.7857 13.3929 22.3214 22.3214] .

	4.4295 1.6556 1.4513 0.1861 -0.1101 
	1.6556 1.8611 0.9576 0.2494 -0.1414 1.4513 0.9576 2.6822 0.7420 -0.4135   0.1861 0.2494 0.7420 1.4219 -0.2338 
	-0.1101 -0.1414 -0.4135 -0.2338 1.1296

Table 1

 1 Results for N 1 = 5, N 2 = 10.

		specification		X #			X
	b	behavior	states	lengths time states lengths time
	23	any	14 876	[8,10]	<1s	331	8	<1s
	24	any	22 265	[8,10]	1.1s	799	8	<1s
	30	mode 0 forbidden	78 549	[6,10]	3.5s	745	[6,10]	<1s
	32	mode 0 forbidden	120 506	[5,10]	2.5s	191	[5,10]	<1s
	32 lights red ≤ 1 t.u.	177 853	[5,10]	2.9s	270	[5,9]	<1s

Table 2

 2 Optimal schedules extracted from X .

		specification	best total throughput	best worst-case thr.
	b	behavior	cycle γ	C 1 (γ)	cycle γ	C 2 (γ)
	23	any	(0)	0	(0)	0
	24	any	(2, 0, 0, 0)	0.25	(0)	0
	30	mode 0 forbidden	(1, 2, 2)	1	(1, 2, 2)	0.333
	32	mode 0 forbidden	(1, 2, 3, 2, 1, 2, 3, 2, 1, 2)	1.2	(1, 2)	0.5
	32 lights red ≤ 1 t.u.	(1, 2)	1	(1, 2)	0.5

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).

Algorithm 2: explore(x, X v ) Parameter : coarse ∈ B, true for maximal coarsest safe invariant Input: state x ∈ X, visited states X v ⊆ X Output: true if and only if x is controllable