Antoine Girard

Directeur De Thèse

This thesis focuses on the development of efficient abstraction-based controller synthesis approaches for cyberphysical systems (CPS). While abstraction-based methods for CPS design have been the subject of intensive research over the last decades, the scalability of these techniques remains an issue. This thesis focuses on developing lazy synthesis algorithms for safety specifications. Safety specifications consist in maintaining the trajectory of the system inside a given safe set. This specification is of the utmost importance in many engineering problems, often prioritized over other performance requirements. Lazy approaches outperform the classical synthesis algorithm [Tabuada, 2009] by avoiding computations, which are non-essential for synthesis goals. Chapter 1 motivates the thesis and discusses the state of the art. Chapter 2 structures the existing lazy synthesis approaches and emphasizes three sources of efficiency: information about a priori controllable states, priorities on inputs, and non-reachable from initial set states. Chapter 3 proposes an algorithm, which iteratively explores states on the boundary of the controllable domain while avoiding exploration of internal states, supposing that they are safely controllable a priory. A closed-loop safety controller for the original problem is then defined as follows: we use the abstract controller to push the system from a boundary state back towards the interior, while for inner states, any admissible input is valid. Chapter 4 presents an algorithm that restricts the controller synthesis computations to reachable states only while prioritizing longer-duration transitions. The original system is abstracted by a symbolic model with an adaptive grid. Moreover, a novel type of time sampling is also considered. Instead of using transitions of predetermined duration, the duration of the transitions is constrained by state intervals that must contain the reachable set. Chapter 5 is dedicated to monotone transition systems. The introduced lazy synthesis approach benefits from a monotone property of transition systems and the ordered structure of the state (input) space, and the fact that directed safety specifications are considered. The considered class of specifications is then enriched by intersections of upper and lower-closed safety requirements. Chapter 6 concludes the discussion and raises new issues for future research.

First and foremost, let me express my sincere gratitude to my Ph.D. advisor Professor Antoine Girard for his guidance and support along the way. Antoine, thank you for your trust in me and your precious advice, help, and motivation.

You were always available for a discussion, and I learned so much from you. I could not have imagined having a better advisor. I mean it! Besides, I would like to extend my special gratitude to my thesis committee members: Professor Luc Jaulin, Professor Maria Prandini, Professor Anne-Kathrin Schmuck, Professor Ali Zolghadri, and Professor Cristina Maniu.

First, let me thank Professor Luc Jaulin for being part of my midterm evaluation committee and for the valuable comments he provided on this thesis. Hopefully, we will find a way to collaborate in the future! Then, I would like to thank Professor Maria Prandini for reviewing my thesis report in detail and asking deep questions during the presentation. Professor Anne-Kathrin Schmuck for the inspiration of my research on multi-scaled abstractions and a fruitful discussion after the talk. Professor Cristina Maniu for being the president of the Jury and for the support of my ideas. And Professor Ali Zolghadri for his attention to a bigger picture in addition to technical details. I also would like to thank Professor Jana Tumova for an excellent opportunity to visit the KTH Royal Institute of Technology in August 2021. I found it amazing how the RPL group is balancing theory and applications, which gave me an understanding of what I want for my future career. Let me thank Pouria Tajvar for initiating the collaboration on safe motion planners. Christian Pek for sharing his experience of managing several projects at the same time.

Also, Wei, Grace, Truls, Taras, and Alex made my visit to Stockholm unforgettable. Let me also thank Professor Dimos Dimarogonas for the possibility of giving a talk on his group's seminar.

During my stay in Paris, I have met many great people who made me feel like I belonged. Let me thank Professor Sami Tliba for giving me the opportunity to teach over the last two years. Professor Elena Panteley, Professor Antonio Loria, and Professor Luca Greco for their personal and professional support. I also want to thank Adnane Saoud for our joint work on monotone dynamical systems and my labmates: Vladimir, Kuba, Adel, Anas, Alejandro, Ralph, Vincent, Amina, and Zohra, for the inspiring discussions and the fun we have had in the last three years.

I am also thankful to Felipe, Loic, Kemal, Polina, Olga, Natasha, Sergei, Oleg, Ivan, and Murad for the days and nights we spent together climbing, traveling, and discovering France. I also would like to thank my neighbors Elisa, Belatricea, Jorge, Michaelo, and Henrique for helping me to pass through 2020. i Let me also express my special thanks to my professors and friends from Lomonosov Moscow State University.

First of all, I would like to thank Professor Pavel Tochilin for supervising my master thesis, believing in me, and inspiring me to get a Ph.D. degree. I am also thankful to my former classmates Nikita, Klava, Arthur, Lilia, Ruslan, and Sasha for being the best friends ever.

Last but not least, I would like to thank my family. My parents, Alexandra and Mikhail, my sister Natalia, both my aunts and my cousin Fedor. They have given me so much love and support that one lifetime would not be enough to pay it back. I also want to remember and thank my grandfather Gennadiy since he was a person I looked up to.

Aperçu de la thèse

Contrôleurs de sécurité pour systèmes cyber-physiques

La théorie du contrôle est un sous-domaine mathématique, dont l'objectif est de développer des approches efficaces pour contrôler des systemes afin qu'ils se comportent de la manière désirée. Ce manuscrit est dédié à la synthèse efficace de contrôleurs de sécurité pour les systèmes cyber-physiques (CPS) à l'aide d'approches basées sur l'abstraction.

Le CPS est un système où des éléments informatiques collaborent pour le contrôle et la commande d'entités physiques et la sécurité est souvent une propriété essentielle du CPS. Intuitivement, la sécurité exige que les «mauvaises» choses ne se produisent pas et elle est de la plus haute importance dans de nombreux problèmes d'ingénierie, souvent prioritaires par rapport à d'autres exigences de performance. Les pompes à insuline doivent protéger une personne diabétique de l'hyper ou de l'hypoglycémie [START_REF] Gillis | Glucose estimation and prediction through meal responses using ambulatory subject data for advisory mode model predictive control[END_REF], Hovorka et al., 2004, Kushner et al., 2019]. Les assistants du régulateur de vitesse adaptatif doivent garder une voiture à une distance de sécurité du véhicule précédent [START_REF] Alam | Guaranteeing safety for heavy duty vehicle platooning: Safe set computations and experimental evaluations[END_REF], Ames et al., 2017, Darbha, 1997]. Le contrôle du climatiseur doit maintenir la température dans un bâtiment intelligent dans la plage souhaitable [Meyer et al., 2013, Thavlov andBindner, 2015]. Dans toutes ces applications pratiques, le comportement du système contrôlé doit satisfaire aux exigences de sécurité. De plus, une spécification de sécurité apparaît souvent comme une sous-tâche d'un problème plus complexe [START_REF] Chen | Safe platooning of unmanned aerial vehicles via reachability[END_REF], comprenant des objectifs de contrôle donnés par un automate hybride [START_REF] Nilsson | Correct-by-Construction Adaptive Cruise Control: Two Approaches[END_REF] ou une formule de logique temporelle linéaire [START_REF] Tajvar | Safe Motion Planning for an Uncertain Non-Holonomic System with Temporal Logic Specification[END_REF].

Contrôle symbolique

La solution étudiée dans cette thèse pour résoudre ce problème de contrôle est basée sur des méthodes symboliques. Le principe de ces méthodes est de créer une abstraction purement discrète du système original que l'on représentera sous la forme d'un système de transitions fini et non-déterministe pour lequel un contrôleur est plus facile à synthétiser grâce aux méthodes du domaine du contrôle discret. Si une relation comportementale (simulation, bisimulation, leurs versions alternées et approchées ou une relation de raffinement de rétroaciii tion [Tabuada, 2009, Reissig et al., 2017]) entre l'abstraction et le modèle original peut être prouvée, cela signifie que tous comportements du système original peuvent être reproduits dans l'abstraction. La relation de simulation alternée implique également qu'un contrôleur discret synthétisé sur l'abstraction peut être transformé en un contrôleur du modèle original satisfaisant les mêmes spécifications. Nous parlons ainsi de contrôle hybride puisqu'un contrôleur discret est appliqué à un système continu (ou hybride). Il faut noter que ce nom ne veut pas forcément dire que cette approche ne s'utilise que pour les systèmes hybrides : elle peut être intéressante pour tous systèmes dont les dynamiques sont trop complexes pour être contrôlées avec les méthodes classiques. Le nom de méthodes symboliques s'explique par la première étape de la création de l'abstraction discrète, consistant en une partition de l'espace d'état : chaque élément de cette partition peut être vu comme un symbole représentant tous les états continus qu'il contient. Les transitions de l'abstraction symbolique sont ensuite obtenues à l'aide d'une analyse d'atteignabilité pour laquelle on prend une approximation de l'ensemble des états continus qui peuvent être atteints (avec une version échantillonnée du système de départ) à partir de ceux contenus dans un symbole.

Motivation et contributions principales

Le principal inconvénient des approches de synthèse basées sur l'abstraction est la faible évolutivité. En effet, les modèles symboliques sont couramment obtenus par discrétisation d'espaces d'état et d'entrée. Des abstractions plus précises nécessitent des paramètres d'échantillonnage plus précis et donnent lieu à des modèles symboliques avec de nombreux états et entrées. Par conséquent, la construction d'abstractions précises requises pour une synthèse réussie est souvent difficilement calculable. De plus, la complexité des algorithmes de synthèse de contrôleurs discrets dépend typiquement de la taille des modèles symboliques. Enfin, les contrôleurs de sécurité basés sur des modèles symboliques plus grands nécessitent plus de mémoire pour leur implémentation en temps réel. Un besoib de réductions de la complexité de calcul des approches de synthèse basées sur l'abstraction a motivé un nombre considérable de recherches au cours de la dernière décennie et a motivé la rédaction de cette thèse. Pour surmonter cette limitation, nous proposons d'utiliser

• des algorithmes de synthèse paresseux pour les systèmes de transitions;

• des modèles symboliques efficaces en taille. L'idée principale des approches paresseuses pour surpasser l'algorithme de synthèse classique [Tabuada, 2009] est de restreindre les calculs à l'essentiel pour la partie synthèse [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF], Hussien and Tabuada, 2018, Hsu et al., 2019, Nilson et al., 2017, Rungger and Stursberg, 2012]. Dans de telles approches, les abstractions sont calculées à la volée, parallèlement à la procédure de synthèse, et la partie inexplorée du modèle symbolique reste non calculée. Pour minimiser la taille des modèles symboliques on peut bénéficier de la stabilité incrémentale [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF], Pola et al., 2010, Saoud and Girard, 2018] ou de la monotonie [Kim et al., 2017, Sinyakov andGirard, 2020a] du système d'origine. Des abstractions efficaces ont également été proposées pour les systèmes différentiellement plats [START_REF] Liu | Reactive controllers for differentially flat systems with temporal logic constraints[END_REF] et pour les systèmes présentant un structure d'interconnexion [START_REF] Gruber | Sparsity-Sensitive Finite Abstraction[END_REF]. En tant que solution pour la classe générale des systèmes, les abstractions multi-échelles sont souvent considérées [START_REF] Gol | Language-guided controller synthesis for linear systems[END_REF], Girard et al., 2016, Hsu et al., 2019, Nilson et al., 2017]. Nous nous concentrerons sur eux dans le chapitre 4.

Le chapitre 2 structure les approches de synthèse paresseuses existantes et met l'accent sur trois sources d'efficacité: les informations sur les états contrôlables a priori [Girard et al., 2016, Koenig andLikhachev, 2005], les priorités sur les entrées [START_REF] Hussien | Lazy controller synthesis using three-valued abstractions for safety and reachability specifications[END_REF], Girard et al., 2016, Hsu et al., 2019, Nilson et al., 2017], et les états non accessibles depuis l'ensemble initial [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF]. Le chapitre 3 présente une nouvelle technique d'échantillonnage temporel adaptatif appliquant la structure souhaitée (liée au voisin) du modèle symbolique.

Un algorithme de synthèse paresseux pour les abstractions liées aux voisins est ensuite fourni, avec une extension pour les abstractions avec un échantillonnage temporel arbitraire. Dans l'esprit, l'idée est proche du résultat du théorème de Nagumo ( [Blanchini, 1999]) et du principe de visée extrême ( [Subbotin, 1995]). Cependant, à notre connaissance, ces idées n'ont jamais été mises en oeuvre dans le cadre de la synthèse de contrôle basée sur l'abstraction. Le chapitre 4 adapte les idées d'exploration de modèle symbolique incrémental et de synthèse paresseuse présentées dans [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF] pour les systèmes de transitions déterministes aux abstractions non déterministes. Un modèle symbolique multi-échelle avec une grille adaptative est également introduit. Le chapitre 5 présente deux classes de systèmes de transitions monotones et fournit des conditions suffisantes pour qu'une abstraction d'un système dynamique monotone [START_REF] Angeli | Monotone control systems[END_REF]] soit monotone. Ensuite, des algorithmes de synthèse paresseux pour des modèles symboliques monotones et des spécifications de sécurité dirigées (et leurs intersections) sont présentés. Le résultat est basé sur des abstractions efficaces qui ont été introduites dans [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF]. v

List of Figures

1.3

The left figure shows transitions with two different durations: for a control u 1 we stop before leaving a radius 1, while for a control u 2 -an interval with a radius 2. We then say that action corresponding to u 1 is less valuable than the action corresponding to u 2 since we prefer first to go further. The central figure shows a 2-layered grid: a coarser level is marked with a normal line and a finer level with a dashed line. The input up brings us from a state q to a state q such that q ⊂ q. The transition corresponding to input (u, 2), where 2 determines the duration ends at the finest layer. The right figure then represents the same transition but with the corresponding adaptive grid. . . . . . . . . . . . . . .

1.4

The left figures show two trajectories of an input-state monotone dynamical system. The right figure provides an example of a lower-closed safety set. In all figures, a natural component-wise order on R 2 is considered for both the input and the state spaces. . . . . . . . . . . . . . . . . . . . . . . . . . .

1.5

The left figure illustrates that if the transition system is lower input state monotone, then we for any two states q 1 Q q 2 and two inputs u 1 U u 2 , F (q 1 , u 1 ) ⊆↓ F (q 2 , u 2 ). Right figure shows that a finite lower-closed set Q (i.e. Q s.t. Q =↓ Q) can be represented by its basis Bas(Q) = {q 1 , q 2 , q 3 , q 4 }, since Q =↓ Bas(Q). . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.1 Illustration of Algorithm 2.1. Algorithm 2.1 iteratively removes all unsafe actions from a transition system until the system stops changing. An action is unsafe if it can not prevent the system from steering into an unsafe or blocking state. Unsafe actions are marked with a red color. Blocking states are filled with grey, the unsafe state -with black. A state q with p(q) = 1 is contoured with black, with p(q) = 0 -with red. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.2 Illustration of Algorithm 2.2 execution.Blocking states are filled with grey. The unsafe state is black.

A state q such that p(q) = 1 are contoured with black, with p(q) = 0 -with red. Let us remark that all transitions in the system are between neighboring states. Hence, we can restrict exploration to those states that border with blocking or unsafe states. The unexplored elements are marked with the dashed line, while the normal line denoted states already involved in computations. At the end of execution, states q 8 , q 4 stay unconsidered, but we can automatically mark them as controllable, including all actions enabled at these states to the maximal safety controller. . . . . . . . . . . . . . .

2.3

Illustration of Algorithm 2.3 execution. Unsafe actions are red. Blocking states are grey. Controls u 1 , u 2 have priority 2, u 3 , u 4 have priority 1. If a state is contoured with black, it has priority 2, and the actions with priority 2 are enabled for this state. If with blue, it has priority 1, and the inputs with priority 1 are available. If with red, then its priority is 0. We enable lower priority transitions for a state only if it is uncontrollable with higher priority actions. Enable at the current iteration transition marked with a normal line, while action marked with a dashed line are non-available. The actions which remain untouched at step 9 are not included in the maximal input lazy safety controller. . . . . 2.4 Illustration Algorithm 2.4 execution. Unsafe actions are red, blocking states are grey, and the initial states are marked with a double line. The computations are restricted to states, which reachable from the initial set. States which are non-reachable from the initial set are countered with a dashed line.

Hence, states q 11 , q 12 and q 8 are not included in the domain of the maximal state lazy safety controller.

3.1 Illustration of the adaptive time sampling technique (right figure) compared to a fixed time sampling approach (left figure). Black cells represent unsafe states; green and blue cells represent F (q, u 1 ) and F (q, u 2 ) correspondingly. The red square represents the abstract state neighborhood N A (q). While in the left figure, transition duration is determined by pre-fixed time sampling parameter τ f ix , in the right figure, a transition stops just before leaving N A (q) (see eq. (3.2)). . . . . . . . . . . . . . . . . the actions with priority 2 are enabled for this state. If with blue, it has priority 1, and the inputs with priority 1 are available. If with red, then its priority is 0. We enable lower priority transitions for a state only if it is uncontrollable with higher priority actions. Enable at the current iteration transition marked with a normal line, while action marked with a dashed line are non-available. Reachable from the initial set states are countered with a normal line, non-reachable with a dashed line. The actions marked with a dashed line in step 9 are not included in the maximal input lazy safety controller. . . . figures, a natural component-wise order on R 2 is considered for both the input and the state spaces. . 5.2 Illustration of Theorem 5.2.1. Given two states q 1 Q q 2 and two inputs u 1 U u 2 , if the transition system is LISM then we have that F (q 1 , u 1 ) ⊆↓ F (q 2 , u 2 ).

Illustration

List of Tables

3.1

Vehicle and safety parameters. The values are taken from [Darbha, 1997, Saoud et al., 2020] [Tabuada, 2009] and with sparse abstractions [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF] and the lazy algorithm from [START_REF] Hussien | Lazy controller synthesis using three-valued abstractions for safety and reachability specifications[END_REF] [Tabuada, 2009], the classical fixed point algorithm with sparse abstractions [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF] and the lazy algorithm from [START_REF] Hussien | Lazy controller synthesis using three-valued abstractions for safety and reachability specifications[END_REF], respectively. . . . .

5.3

Runtime comparison when varying the number of inputs. T s lm , T cl , T s cl and T s 3v are the running time of Algorithm 5.5, the classical fixed point algorithm with box abstractions [Tabuada, 2009] and with sparse abstractions [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF] and the lazy algorithm from [START_REF] Hussien | Lazy controller synthesis using three-valued abstractions for safety and reachability specifications[END_REF] [Tabuada, 2009], the classical fixed point algorithm with sparse abstractions [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF] and the lazy algorithm from [START_REF] Hussien | Lazy controller synthesis using three-valued abstractions for safety and reachability specifications[END_REF], respectively. . . . .

List of Symbols and Abbreviates

N, Z, R nonnegative integers, integers and real numbers correspondingly

N p , R p , Z p p-dimensional vector spaces originated by N, Z, R correspondingly L(T , S) is a space of measurable function on T taking their values from S s ∈ L(T , S) is a function belonging to L(T , S) ≺ S a partial order on S cl(X) is a closure of a set X Σ f = (T , R nx , U, W, f ) a control system with a dynamic given by ẋ = f (x, u, w), u ∈ U, w ∈ W x f (t | x(0), u, w) a trajectory of Σ f corresponding to an initial condition x(0), a control u ∈ L(T , U)
, and a disturbance w ∈ L(T , W)

Reach(τ | q, u) a robust to admissible disturbance reachable set, corresponding to an initial set q and a constant control function u : [0, t] → u and Reach(τ | q, u) an over-approximation of Reach(τ | q, u)

Transition system Σ = (Q, U, F ) transition system Q, U
a set of states and inputs correspondingly F a transition relation

F (q, u)
a set of successors corresponding to a state q and an input u P re F (q, u) set of predecessors corresponding to a state q and an input u w.r. Chapter 1

Introduction

Cyber-physical systems (CPS) are physical and engineered systems whose operations are monitored, coordinated, controlled and integrated by a computing and communication core [START_REF] Rajkumar | Cyber-physical systems: The next computing revolution[END_REF]. It is clear, that they are to become ubiquitous in modern societies: autonomous vehicles, smart buildings, robots...many grand challenges await in the economically vital domains of transportation, health care, manufacturing, agriculture, energy, defense, aerospace, and buildings. The design, construction and verification of CPS pose a multitude of technical issues.

It requires a wide range of expertise from control theory to embedded software engineering to cope with the tight interactions between the computational and physical elements of a CPS. This renders the development of a CPS challenging and time-consuming. Moreover, since CPS are often safety-critical, a significant amount of effort must be invested in system integration and verification to ensure the soundness of the proposed design.

A sound design of CPS, taking into account the interactions between the computational and physical elements, requires model-based approaches. CPS models are heterogeneous: the continuous behavior is described by differential equations (in general non-linear), while the discrete behavior is formalized with finite-state automata frameworks. As pointed out in [Derler et al., 2012, Kim andKumar, 2012], being able to deal with heterogeneity is a prerequisite to the foundation of a sound framework for CPS design. During the past decade, significant progress towards that goal has been made, notably in the area of hybrid dynamical systems. Hybrid systems are dynamical systems exhibiting both continuous and discrete behaviors. Motivated by the multiplication of "discrete" embedded computing devices interacting with the "continuous" physical world, the research on hybrid systems has rapidly developed at the interface of computer science and control since the nineties. Each discipline has brought its models and methods, and their combination has allowed the scientific community to build the foundations of a theory of hybrid systems. The notion of hybrid automaton [Henzinger, 2000, Lygeros et al., 2003], which is one of the most commonly used mathematical models of hybrid systems, combines differential equations and finite-state automata and is a typical example of this cross-fertilization. More generally, hybrid systems research has allowed new topics at the intersection of computation and control.

Another challenging issue in developing CPS is a complex control objective that goes beyond the traditional control theory (e.g. stability, controllability, observability...). For example, one often has to address safety, reachability, fault-tolerance, or even specifications given by some logic formula or automaton describing the acceptable temporal behaviours of the system [START_REF] Belta | Formal Methods for Discrete-Time Dynamical Systems[END_REF], Cassandras and Lafortune, 2009[START_REF] Sinyakov | Formal Synthesis from Control Programs[END_REF].

Design of Safety Critical Cyber-Physical Systems

As was mentioned above, CPS are safety-critical. Intuitively, safety requires that "bad" things do not happen and it is of the utmost importance in many engineering problems, often prioritized over other performance requirements.

Insulin pumps should protect a diabetic person from hyper or hypoglycemia [START_REF] Gillis | Glucose estimation and prediction through meal responses using ambulatory subject data for advisory mode model predictive control[END_REF], Hovorka et al., 2004, Kushner et al., 2019]. Adaptive cruise control assistants should keep a car at a safe distance from the previous vehicle [START_REF] Alam | Guaranteeing safety for heavy duty vehicle platooning: Safe set computations and experimental evaluations[END_REF], Ames et al., 2017, Darbha, 1997]. Climate control should maintain the temperature in an intelligent building into the desirable range [Meyer et al., 2013, Thavlov andBindner, 2015]. Satellite station keeping [START_REF] Weiss | Station keeping and momentum management of low-thrust satellites using mpc[END_REF], traffic networks [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF] and biochemical networks [Sontag, 2007] control, power grids design [START_REF] Kader | Safety controller design for incrementally stable switched systems using event-based symbolic models[END_REF]. . . in all these practical applications the behavior of the controlled system should satisfy the safety requirements. Moreover, a safety specification often appears as a sub-task of a more complex problem [START_REF] Chen | Safe platooning of unmanned aerial vehicles via reachability[END_REF], including control objectives given by hybrid automaton [START_REF] Nilsson | Correct-by-Construction Adaptive Cruise Control: Two Approaches[END_REF] or linear temporal logic formula [START_REF] Tajvar | Safe Motion Planning for an Uncertain Non-Holonomic System with Temporal Logic Specification[END_REF]. Being a critical issue in designing CPS, safety specification is the main topic of this manuscript. However, before moving forward let us formalize the considered problem.

Formal Problem Statement

A control system Σ f = (T , R nx , U, W, f ) consists of a time domain T = [0, +∞), a state space R nx , a compact set U ⊂ R nu , a compact set W ⊂ R nw
, and a non-linear function f : R nx × U × W → R nx , such that for any control u ∈ L(T , U), any disturbance w ∈ L(T , W) and any initial condition x(0) ∈ R nx in the whole domain R nx there exists a unique solution x f (t | x(0), u, w), t ∈ T of the following differential equation

ẋ(t) = f (x(t), u(t), w(t)) (1.1)
in the sense of Caratheodory. The notation L(T , S) is used for the space of functions s, measurable on T , such that s(t) ∈ S, t ∈ T almost everywhere. Let us also use a bold font to denote a function s inL(T , S).

We then call a solution x f (t | x(0), u, w), t ∈ T a trajectory of the system Σ f = (T , R nx , U, W, f ) corresponding to an initial condition x(0), a control function u, and a disturbance w. When the control inputs of system Σ f = (T , R nx , U, W, f ) are generated by a state-feedback controller u(t, x) : T × R nx → U, the dynamics of the closedloop system, corresponding to a disturbance realization w, is given by ẋ(t) = f (x(t), u(t, x(t)), w(t)), t ∈ T , and the trajectory of closed-loop system is denoted as x u f (t | x(0), w). The class of admissible closed-loop controls u(t, x(t)) must, however, be restricted so that the closed-loop system has a unique solution (in the sense of Caratheodory) in the considered domain.

Problem 1.1.1. Given a control system Σ = (T , R nx , U, W, f ) find an admissible safety controller, which keeps all trajectories of the closed-loop system inside a safety set Y ⊂ R nx . Here the controller is said to be admissible if it is robust against any measurable bounded disturbance w ∈ L(T , W ) and there exists a unique solution of the closed-loop system.

Literature Overview

On Computation of Maximal Control-Invariant Sets

A fundamental concept related to safety specification is (robust) control invariant sets. By definition, a subset of the state space is a control invariant set (or a viable set [START_REF] Aubin | Viability Kernel of Control Systems[END_REF]) if, for all initial conditions chosen among its elements, we can keep the trajectory inside the set by means of proper control action. If disturbances, in addition, are considered, then the set is known as a robust control invariant set. So, to solve a safety control problem means to find a (robust) control invariant set included in a given safe set and there is a practical interest in getting the invariant set, which is maximal by inclusion. The existence and uniqueness of such a set was, for example, studied within the viability theory [START_REF] Aubin | Viability Kernel of Control Systems[END_REF]. Though the problem of finding maximal control-invariant sets for arbitrary systems is intractable, there is an extensive literature on computing numerical approximations. Polytopic projection [Blanchini, 1999, Anevlavix andTabuada, 2019]), LMI-based Lyapunov type analysis techniques [START_REF] Khlebnikov | Optimization of linear systems subject to bounded exogenous disturbances: The invariant ellipsoid technique[END_REF], sum of squares programming [Papachristodoulou andPrajna, 2005, Tan andPackard, 2008], Minkowski type methods [START_REF] Kolmanovsky | Theory and computation of disturbance invariant sets for discrete-time linear systems[END_REF]] and linear programming approaches [Trodden, 2016] allow us to compute convex approximations of maximal invariant sets for linear system.

For nonlinear systems the problem has been addressed with approaches based on value-function approximations [Mitchell et al., 2005, Kurzhanski and[START_REF] Kurzhanski | [END_REF], a control barrier functions design [START_REF] Ames | Control barrier function based quadratic programs for safety critical systems[END_REF], and interval analysis techniques [START_REF] Alam | Guaranteeing safety for heavy duty vehicle platooning: Safe set computations and experimental evaluations[END_REF], Jaulin et al., 2001, Li and Liu, 2018a, Meyer et al., 2013]. However, the heterogeneous dynamic of CPS and demand to incorporate the safety into more difficult control specifications have turned the attention of the considerable part of the research community to abstraction-based synthesis approaches [START_REF] Belta | Formal Methods for Discrete-Time Dynamical Systems[END_REF], Tabuada, 2009].

Abstraction-Based Control Synthesis (ABCS) Approaches

In recent years, controller synthesis techniques based on abstractions have received considerable attention within the control systems community. Continuous-time abstractions serve for two reasons: simplify the dynamic of the original system [START_REF] Fu | Hierarchical control via approximate simulation and feedback linearization[END_REF], Dang et al., 2010] or reduce the number of dimensions [START_REF] Girard | Hierarchical control using approximate simulation relations[END_REF].

However, this work is dedicated to so-called symbolic model control when one creates a finite-state discretetime abstraction on top of the original system. The latter allows to leverage computer-science control synthesis techniques and enrich the class of available specifications [START_REF] Cormen | Introduction to Algorithms[END_REF]. We call the abstraction a symbolic model since one abstract state is a symbol representing infinitely many states of the original state space. Symbolic model control is a popular branch of the modern control theory. The dynamics of considered system varies from simple double integrators [START_REF] Fainekos | Temporal logic motion planning for dynamic robots[END_REF], over linear [START_REF] Wongpiromsarn | Receding horizon temporal logic planning for dynamical systems[END_REF], Rungger et al., 2013] and piecewise affine [START_REF] Yordanov | Temporal logic control of discrete-time piecewise affine systems[END_REF] to nonlinear systems [Tabuada, 2009, Reissig et al., 2017, Girard, 2010, Liu et al., 2013, Zamani et al., 2011]. The control problems range from reach-avoid [Tabuada, 2009, Girard, 2010, Reissig et al., 2017, Zamani et al., 2011] and safety specifications [START_REF] Hsu | Lazy abstraction-based controller synthesis[END_REF], Tabuada, 2009, Girard, 2010, Saoud et al., 2020], fragments of LTL [START_REF] Fainekos | Temporal logic motion planning for dynamic robots[END_REF], Wongpiromsarn et al., 2009, Liu et al., 2013] to full LTL [Tabuada andPappas, 2006, Kloetzer and[START_REF] Kloetzer | [END_REF].

Roughly speaking, control synthesis based on symbolic models is a three-step procedure. In the first step, the continuous or hybrid system (together with the specification) is lifted to an abstract domain where it is substituted by a finite transition system [START_REF] Belta | Formal Methods for Discrete-Time Dynamical Systems[END_REF], which mimics the original dynamic. In the second step, an auxiliary problem on the abstract domain ("abstract problem") is solved using discrete methods [START_REF] Cassandras | [END_REF]Lafortune, 2009, Cormen et al., 2001]. In the third step, the controller synthesized for the abstraction is refined to the concrete system [START_REF] Belta | Formal Methods for Discrete-Time Dynamical Systems[END_REF], Tabuada, 2009].

Behavioural Relationships

The correctness of abstraction-based approaches is usually ensured by connecting the original system with its abstraction in terms of a system relation. The notion of simulation [Milner, 1989, Park, 1981] guarantees that an execution is possible for the abstraction if it is possible for the concrete system. The concept of bisimulation states that an execution is possible for the abstraction if and only if it is possible for the concrete system [Pappas, 2003]. Since the construction of bisimilar abstractions was possible for restricted classes of systems, the notion of simulation was relaxed by [START_REF] Girard | Approximate bisimulations for constrained linear systems[END_REF]. The construction of approximately bisimilar deterministic abstractions was made possible for incrementally stable systems [Angeli, 2002]. An extension called alternating approximate bisimilarity has been proposed in [START_REF] Pola | Symbolic models for nonlinear time-delay systems using approximate bisimulations[END_REF], allowing for the construction of non-deterministic abstractions. While in the approximate alternating (bi-)simulation relations, the refined controller needs to contain the abstraction as a building block. The notion of feedback-refinement relation [START_REF] Reissig | Feedback refinement relations for the synthesis of symbolic controllers[END_REF], which in spirit are the same as over-approximation relations [START_REF] Liu | Synthesis of reactive switching protocols from temporal logic specifications[END_REF], was proposed to address this shortcoming. Finally, a first approach to construct a behavioural relationship taking into account the structural properties of dynamical systems has been recently proposed in [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF], where the notion of directed alternating simulation relation was shown to be efficient in order to deal with monotone dynamical systems [START_REF] Angeli | Monotone control systems[END_REF].

Toolboxes

Various tools built on abstraction-based methods are available for the purpose of control synthesis. Tools such as LTLMoP [START_REF] Finucane | Ltlmop: Experimenting with language, temporal logic and robot control[END_REF], TuLip [START_REF] Wongpiromsarn | Tulip: A software toolbox for receding horizon temporal logic planning[END_REF] are restricted to simple integrator dynamics and piecewise affine control systems, respectively, while 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],

ROCS [START_REF] Li | Rocs: A robustly complete control synthesis tool for nonlinear dynamical systems[END_REF], SCOTS [START_REF] Rungger | Scots: A tool for the synthesis of symbolic controllers[END_REF], and Co4Pro [START_REF] Sinyakov | Formal controller synthesis from specifications given by discrete-time hybrid automata[END_REF]] consider nonlinear systems. The differences between Pessoa, CoSyMa and ROCS, SCOTS, Co4Pro become apparent in terms of the type of symbolic model which is used to solve the synthesis problem. CoSyMa requires the original system to be incrementally stable [Angeli, 2002] and computes symbolic models that are approximately bisimilar to the original system [Girard, 2010]. Pessoa, additionally to approximately bisimilar symbolic models, supports the computation of approximately alternatingly similar symbolic models [Tabuada, 2009]. However, Pessoa can not handle nonlinear systems unless the user provides their own overapproximation function. Accepting general non-linear systems, symbolic models implemented by SCOTS are based on feedback refinement relations [START_REF] Reissig | Feedback refinement relations for the synthesis of symbolic controllers[END_REF].

The kernel of ROCS is interval branch-and-bound scheme, with limitation that customized inclusion functor has to be provided by the user. Comparing to SCOTS and ROCS the internal rechability algorithm are improved in Co4Pro to achive the better performance of abstraction-based approaches. Concerning the specifications SCOTS, Pessoa, CoSyMa, ROCS natively supports the controller design to enforce invariance and reachability. LTLMoP and TuLip support more general specifications like GR(1) [START_REF] Bloem | Synthesis of reactive(1) designs[END_REF]. The most resent toolbox Co4Pro supports specifications given by a discrete-time hybrid automaton.

Over-approximations of Reachable Sets

As previously stated, the exact reachable set of linear continuous systems can only be computed in special cases [START_REF] Lafferriere | Symbolic reachability computation for families of linear vector fields[END_REF]. Thus, the reachable set has to be computed in an overapproximative way in order to verify if an unsafe set is possibly reached. Several geometric representations for linear continuous systems have been investigated: polytopes [START_REF] Chutinan | Computational techniques for hybrid system verification[END_REF], ellipsoids [START_REF] Kurzhanski | Dynamics and Control of Trajectory Tubes[END_REF], griddy polyhedra [START_REF] Asarin | Approximate reachability analysis of piecewise-linear dynamical systems[END_REF], zonotopes [Girard, 2005], or support functions [START_REF] Girard | Efficient reachability analysis for linear systems using support functions[END_REF] which unify the other mentioned representations. For linear systems with disturbances zonotopes [Girard, 2005] and support functions [START_REF] Girard | Efficient reachability analysis for linear systems using support functions[END_REF] have clearly outperformed existing methods, allowing the verification of systems with more than 100 continuous state variables. The reachability analysis of non-linear or hybrid systems has been a challenging problem over the last few decades. Many existing results are based on analysis of solutions of Hamilton-Jacobi-Isaacs equation [START_REF] Mitchell | A time-dependent hamilton-jacobi formulation of reachable sets for continuous dynamic games[END_REF] on Taylor models [START_REF] Chen | Taylor model flowpipe construction for non-linear hybrid systems[END_REF]. However, while aiming to provide as precise approximations as possible, these approaches are not very suitable for symbolic model control where a considerable number of reachable sets should be estimated. For abstraction-based synthesis we recommend to focus on simple interval over-approximations, trading accuracy for efficiency. The literature on interval-based reachability analysis contains a wide range of methods. The main classes of approaches are summarized below. Approaches based on interval arithmetics are presented in [START_REF] Jaulin | Applied Interval Analysis[END_REF]. In other methods, interval reachability analysis is achieved through the preservation of partial orders by the system description resulting from a monotonicity property of the dynamics [START_REF] Angeli | Monotone control systems[END_REF]. This approach can be applied to both monotone systems [START_REF] Moor | Abstraction based supervisory controller synthesis for high order monotone continuous systems[END_REF], as well as for mixed-monotone systems [Coogan andArcak, 2015, Meyer et al., 2018]. Some methods focus on the propagation of the initial set over time based on an upper bound of the growth or contraction of the distance between trajectories of a continuous-time system [START_REF] Maidens | Reachability analysis of nonlinear systems using matrix measures[END_REF], Reissig et al., 2017, Fan et al., 2016]. Methods based on differential inequalities bound the system dynamics by auxiliary differential equations whose solutions define lower and upper bounds of the reachable set for the main system [Scott andBarton, 2013, Shen andScott, 2017]. The interested reader can find a comprehensive overview of interval-based reachability analysis techniques many of which have been implemented in [START_REF] Meyer | Tira: Toolbox for interval reachability analysis[END_REF] in the recent book [START_REF] Meyer | Interval Reachability Analysis.Bounding Trajectories of Uncertain Systems with Boxes for Control and Verification[END_REF].

Illustrative Example: ABCS for Safety Specification

Let us use Figure 1.1 to briefly explain how symbolic model control can be used to solve Problem 1.1.1. Given a control system Σ f = (T , R nx , U, W, f ) and a safe set Y we aim to compute a transition system Σ = (Q, U, F ), with finite sets of states Q and inputs U , and transition relation F ⊆ Q × U × Q that is linked to concrete system Σ f with feedback refinement relationship. Let us introduce a finite partitioning on the state space R nx and associate every element of this partitioning belonging to Y (countered with red) with a safe state q i ∈ Q, i = 1, . . . , 24. In the first sub-figure of Figure 1.1 the safe sets are filled with white color. The grey region is associated with an unsafe state q us ∈ Q. Thus, an abstract state is considered as atomic symbol representing an infinite number of states from R nx . We then approximate the original set of inputs U with a finite subset U . In our particular example U = {u 1 , u 2 } and transitions corresponding to u 1 and u 2 are marked with black and blue correspondingly. Introducing a time sampling parameter τ f ix we then say that for all q ∈ Q S = Q \ {q us }, u ∈ U, q ∈ Q transition (q, u, q ) ∈ F if and only if q ∩ Reach(τ f ix | q, u) = ∅, where Reach(τ f ix | q, u) is an over-approximation of the reachable set q 1 q 6 q 11 q 16 q 21 q 22 q 17 q 12 q 7 q 2 q 3 q 4 q 5 q 10 q 9 q 8 q 13 q 14 q 18 q 23 q 24 q 19 q 20 q 15 q us q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15 q 16 q 17 q 18 q 19 q 20 q 21 q 22 q 23 q 24 Y q us q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15 q 16 q 17 q 18 q 19 q 20 q 21 q 22 q 23 q 24 create an abstraction synthesize a controller for the abstraction q 1 q 6 q 11 q 16 q 22 q 17 q 12 q 7 q 2 q 3 q 4 q 5 q 10 q 9 q 8 q 13 q 14 q 18 q 23 q 19 q 15

... Reach(τ f ix | q, u), corresponding to an initial set q, a constant control function u : [0, t] → u, u ∈ U and admissible disturbances w ∈ L(T , W), i.e.

Reach(t | q, u) = x ∈ R nx | ∃ x(0) ∈ q and ∃ w ∈ L([0, t], W) such that x f (t | x(0), u, w) = x .
Remark 1.3.1. Here we use the notation Reach(t | q, u) instead of Reach(t | q, u) to emphasize that the reachable set corresponds to a constant control function. We will keep this logic later in the text as well.

So, to compute transition originated in a state q 1 and corresponding to controls u 1 , u 2 we have to calculate two different reachable tubes, as it is shown in the first sub-figure. We then repeat the same procedure for every q ∈ Q S , u ∈ U to compute the whole symbolic model (the second sub-figure). Let us remark that F (q 1 , u 1 ) = {q us , q 11 }, and F (q 1 , u 2 ) = {q 6 , q 7 , q 12 }, i.e., the obtained transition system is non-deterministic. To synthesize a safety controller for the abstraction one can use the classical algorithm from [Tabuada, 2009]. According to that algorithm, all unsafe transitions are iteratively removed from the transition system until the system stops changing.

The safety controller C : Q → 2 U is then initialised for every state q with remaining actions. A transition is unsafe if it is not safe, while safe transitions correspond to actions, preventing the system from steering into a blocking or unsafe state. For example in the second sub-figure of Figure 1.1 the transitions colored with black from states q 1 , q 21 and the transitions colored with blue from states q 24 and q 20 are unsafe since they steers into q us . A state is blocking if there is no transitions allowing to leave this state (blocking states are grey). Hence, a safety controller C ensures that all trajectories of the controlled transition system are infinitely long and belong to the safe set Dom(C) ⊆ Q S ⊆ Y (subfigure 3 for the illustration). Here Dom(C) denotes the domain of the controller, i.e.

Dom(C) = {q ∈ Q S | C(q) = ∅}.
We then can guarantee for the original system Σ f = (T , R nx , U, W, f ) that all trajectories starting in Dom(C) can be maintained within a safe set Y infinitely long. Indeed, let, for example, x(0) ∈ q 1 (sub-figure 4). Since q 1 ∈ Dom(C) there is a controller u 2 ∈ C(q 1 ) and if we apply input u 2 τ f ix seconds we end up in q 6 , q 7 or in q 12 , depending on a disturbance realization w. Let us suppose that transition finishes at q 7 . Since C is a safe controller for the transition system states q 7 ∈ Dom(C) and there is a safe input u 1 ∈ C(q 7 ) such that in τ seconds it again brings us in the Dom(C) ⊆ Y, and so on. Hence, the real-time controller for the original system is implemented as a look-up table and, we guarantee that every τ seconds the closed-loop trajectory of Σ f is in a safe set Y . To guarantee that it doesn't leave Y between too check-points, one either chooses τ sufficiently small, or additionally requires that Reach(t | q, u) ∩ Y = ∅, t ∈ [0, τ f ix ] for all q ∈ Q S , u ∈ U , while constructing the symbolic model.

Let us remark that if a safe controller C enables several inputs for a state, as for example in q 12 , any of them ensure safety and we can benefit from this flexibility to achieve more difficult control objectives.

Motivation and Main Contributions

The main drawback of abstraction-based synthesis approaches is poor scalability. Indeed, symbolic models are commonly obtained through the discretization of state and input spaces. More accurate abstractions require more accurate sampling parameters and result in symbolic models with many states and inputs. Consequently, the construction of precise abstractions required for a successful synthesis is often computationally intractable. Moreover, the complexity of the discrete controller synthesis algorithms typically depends on the size of symbolic models. Finally, safety controllers based on larger symbolic models require more memory for their real-time implementation. A demand to reduce the computational complexity of abstraction-based synthesis approaches reasoned considerable amount of research over the last decade and motivated writing this thesis. There are several research directions one can explore aiming to overcome the scalability issues:

• compositional approaches as a way to overcome the curse of dimensions [Saoud, 2019];

• efficient reachability algorithms as a way to speed-up computation of symbolic models [START_REF] Meyer | Interval Reachability Analysis.Bounding Trajectories of Uncertain Systems with Boxes for Control and Verification[END_REF].

However, let us leave these two directions out of the scope of this manuscript and focus on the following two:

• lazy synthesis algorithms for transition systems;

• size-efficient symbolic models.

The main idea of lazy approaches to outperform the classical synthesis algorithm [Tabuada, 2009] is to restrict computations to the essential for the synthesis part [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF], Hsu et al., 2019, Hussien and Tabuada, 2018, Nilson et al., 2017, Rungger and Stursberg, 2012]. In such approaches, abstractions are computed on the fly, in parallel with the synthesis procedure, and the unexplored part of the symbolic model remains uncalculated. To minimize the size of symbolic models one can benefit from incremental stability [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF], Pola et al., 2010, Saoud and Girard, 2018] or monotonicity [Kim et al., 2017, Sinyakov andGirard, 2020a] of the original system. Efficient abstractions were also proposed for differentially flat systems [START_REF] Liu | Reactive controllers for differentially flat systems with temporal logic constraints[END_REF] and for systems exhibiting a sparse interconnection structure [START_REF] Gruber | Sparsity-Sensitive Finite Abstraction[END_REF]. As a solution for general class of systems multi-scale abstractions are often considered [START_REF] Gol | Language-guided controller synthesis for linear systems[END_REF], Girard et al., 2016, Hsu et al., 2019, Nilson et al., 2017]. We will focus on them in Chapter 4.

Chapter 2 structures the existing lazy synthesis approaches and emphasizes three sources of efficiency: information about a priori controllable states [Girard et al., 2016, Koenig andLikhachev, 2005], priorities on inputs [START_REF] Hussien | Lazy controller synthesis using three-valued abstractions for safety and reachability specifications[END_REF], Girard et al., 2016, Hsu et al., 2019, Nilson et al., 2017], and non-reachable from initial set states [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF]. Chapter 3 introduces a novel adaptive time-sampling technique enforcing the desired (neighbor-linked) structure of the symbolic model. A lazy synthesis algorithm for neighbor-linked abstractions is then provided, with an extension for abstractions with arbitrary time-sampling. Chapter 4 adapts the incremental symbolic model exploration and lazy synthesis ideas presented in [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF] for deterministic transition systems to non-deterministic abstractions. A size-efficient multi-scale symbolic model with an adaptive grid is also introduced. Chapter 5 introduces two classes of monotone transition systems and provides sufficient conditions for an abstraction of a monotone dynamic system [START_REF] Angeli | Monotone control systems[END_REF]] to be monotone. Then, lazy synthesis algorithms for monotone symbolic models and directed safety specifications (and their intersections) are presented.

Thesis Outline

Overall work is dedicated to efficient safety controller synthesis using the abstraction based approaches. The numerical implementations of Chapters 3 and 5 have been implemented in MATLAB, while the numerical implementations of Chapters 2 have been implemented in C++. We summarize below the results illustrated in each chapter.

Chapter 2. Safety Controller Synthesis for Finite Transition System

In Chapter 2, we first remind the classical procedure [Tabuada, 2009] for maximal (by inclusion) safety controller synthesis for finite transition systems (Algorithm 2.1). We then focus on lazy synthesis approaches, which outperform the classical algorithm in terms of efficiency. Structuring existing results, we emphasize three sources of laziness:

• priorities on input space [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF], Hsu et al., 2019, Hussien and Tabuada, 2018];

• information about a priori controllable states [Girard et al., 2016, Koenig andLikhachev, 2005].

• non-reachable from initial set states [Girard et al., 2016, Tripakis andAltisen, 1999].

We then provide three lazy synthesis algorithms which benefit from these sources. Algorithm 2.2 avoids exploration of states and transitions which are safely controllable a priory. Algorithm 2.3 explores the lower-priority actions only if the safety problem is unsolvable with higher-priority actions. Based on the incremental exploration of the transition system, Algorithm 2.4 restricts computations for reachable from initial set states only. Algorithm 2.2 returns the maximal safety controller but compute it lazily. The controllers returned by Algorithm 2.3 and Algorithm 2.4 do not satisfy the maximality requirement, and we call them maximal input-lazy and maximal state-lazy safety controllers correspondingly. Both these controllers are a particular case of the maximal lazy safety controller introduced in [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF]. Maximal input-lazy safety controller C * has the property that all safely controllable states are in the domain of C * . Moreover, if the controller enables an input, it also enables all inputs that have the same priority and preserve safety. However, if several inputs can maintain safety, the controller enables only inputs with the highest priority (Definition 2.3.2). Maximal state-lazy safety controller C * has a property that a safely controllable state is in Dom(C * ) if and only if it is reachable from the initial set (Definition 2.3.3). Lazy synthesis approaches explore only part of the transition system and allow us to compute the abstraction on-the-fly.

Chapter 3. Lazy Controller Synthesis Based on Safe Set Boundary Exploration

Chapter 3 proposes an abstraction-based approach to synthesize a safety controller solving Problem 1.1.1. The main idea consists in creating a neighbor-linked abstraction, where only transitions between neighboring states are allowed. To construct the abstraction with the desired structure, we interrupt every transition just before leaving the abstract state neighborhood (Figure 1.2 (left)). This idea differs from existing time-sampling approaches, where transitions duration is determined with a given parameter [Tabuada, 2009]. We then use Algorithm 2.2 to synthesize the maximal safety controller lazily by iteratively exploring only those states which border the uncontrollable domain (Theorem 3.1.1), since as soon a safe frontier is found, all internal states are controllable a priori with any admissible input. We then show that even when abstraction is not neighbor-linked, the controller returned by Algorithm 2.2 can be refined to solve Problem 1.1.1 by using a novel control refinement scheme that interrupts the closed-loop trajectory of the original system when it reaches a boundary state of the controllable domain (Theorem 3.3.1). Such a refining procedure ensures that the trajectory does not over-jump the safe boundary, where we have the abstract controller to push the system back towards the interior. In the internal set any admissible control is then allowed

(Figure 1.2 (right)).
In spirit, the idea is close to the result of Nagumo theorem ( [Blanchini, 1999]) and extreme aiming principle ( [Subbotin, 1995]). In simple words, Nagumo theorem says that a convex and closed set S is a positive invariant of the system (1.1) if and only if for all x ∈ ∂S derivative ẋ points inside S or it is tangent to S, while in [Subbotin, 1995] the authors propose to use any control input until the trajectory reaches the boundary. However, to the best of our knowledge, these ideas has never been implemented within the abstraction-based control synthesis framework.

q us q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15 q 16 q 17 q 18 q 19 q 20 q 21 q 22 q 23 q 24 q 1 q 6 q 11 q 16 q 22 q 17 q 2 q 3 q 4 q 5 q 10 q 14 q 18 q 23 q 19 q 15 q 24 q 20 q 21

N A (q) Reach(τ A q,u | q, u) Reach(τ | q, u) q Y Figure 1.2:
The left figure illustrates adaptive time-sampling techniques: while transition duration is commonly determined by a given time sampling parameter τ , we propose interrupting every transition stops just before leaving N A (q). The right figure represents the result of the synthesis procedure for an arbitrary abstraction, while the central figure shows the corresponding domain of the continuous-time controller. In the green region, we apply any admissible input, but as soon as closed-loop trajectory reaches the white area, we switch to the "abstract" controller, which steers us back to the controllable domain.

Reach(τ u,2 q | q, u) q ′ q up u Reach(τ u2,2 q | q, u 2 ) Reach(τ u1,1 q | q, u 1 ) q u 2 u 1 Reach(τ u,2 q | q, u) u q Figure 1.3:
The left figure shows transitions with two different durations: for a control u 1 we stop before leaving a radius 1, while for a control u 2 -an interval with a radius 2. We then say that action corresponding to u 1 is less valuable than the action corresponding to u 2 since we prefer first to go further. The central figure shows a 2-layered grid: a coarser level is marked with a normal line and a finer level with a dashed line. The input up brings us from a state q to a state q such that q ⊂ q. The transition corresponding to input (u, 2), where 2 determines the duration ends at the finest layer. The right figure then represents the same transition but with the corresponding adaptive grid.

Chapter 4. Lazy Synthesis with Adaptive Symbolic Abstractions

Chapter 4 focuses on approaches, which iteratively refine symbolic models when synthesis for coarser abstractions has not been successful [START_REF] Gol | Language-guided controller synthesis for linear systems[END_REF], Girard et al., 2016, Hsu et al., 2019[START_REF] Li | Rocs: A robustly complete control synthesis tool for nonlinear dynamical systems[END_REF]. We first construct a multilayered symbolic model with multi-scale time sampling. On the state space of the concrete system, we introduce several uniform Cartesian partitions embedded one into another and combine them into a multilayered grid. We then again constrain transitions duration by intervals that must contain the reachable set. However, unlike the adaptive-time sampling in Chapter 3, neighborhoods of different sizes are used to implement the multiple time duration idea (Figure 1.3 (left)). We also introduce an input up, which allows switching from the current layer to the previous (coarser) one. We also finish all non-up transitions at the finest layer. Aiming to use a lazy synthesis Algorithm 2.3 we define a partial order on inputs space, prioritizing transitions with a longer duration and putting the input up on top of everything (Figure 1.3 (middle)). In addition to abstraction refining, we propose to explore the symbolic model forwardly and thus restrict the controller synthesis computations to states that are reachable from the initial set only. Thus, we merge Algorithm 2.3 and Algorithm 2.4 from Chapter 2 and compute a controller inheriting properties from both maximal input-lazy and state-lazy controllers (Algorithm 4.2). Such a controller was first considered [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF], but their synthesis procedure was restricted to a deterministic transition system. We overcome this issue in the present work. Let us remark that with lazy synthesis, we compute for a state q transitions with a shorter duration only if q is uncontrollable with longer duration actions. We also do not compute abstraction for states embedded in q if it is controllable. We also show in Section 4.2.1 that the multilayered grid can be replaced with a more efficient adaptive grid. (two right sub-figures of Figure 1.3 illustrate the difference between adaptive and multi-layered grid).

Chapter 5. Lazy Synthesis for Monotone Systems and Directed Specifications

Chapter 5 is devoted to monotone control systems and specifications given by lower-closed and upper-closed sets. I.e.,it is devoted to systems whose trajectories preserve some partial orderings on their state and input spaces [START_REF] Angeli | Monotone control systems[END_REF], Kamke, 1932, Hirsch and Smith, 2004, Müller, 1927, Smith, 1995] and specifications given by sets which coincide with their lower under upper closure correspondingly, where a lower closure of

a set A ⊂ L is a set ↓ A = a∈A ↓ a, where ↓ a = {q ∈ L | q L a}, while an upper closure is a set ↑ A = a∈A ↑ a,
where ↑ a = {q ∈ L | a L q}. See Figure 1.4 for an illustration.

u, w

u ′ u w w ′ t x ′ 0 x 0 x f (t | x ′ 0 , u ′ , w ′ ) x f (t | x 0 , u, w) ⇒ Y =↓ Y Figure 1.4:
The left figures show two trajectories of an input-state monotone dynamical system. The right figure provides an example of a lower-closed safety set. In all figures, a natural component-wise order on R 2 is considered for both the input and the state spaces.

Adapting results from [START_REF] Angeli | Monotone control systems[END_REF], we provide criteria for a dynamical system to be state monotone or input-state monotone and use Example 5.1.1 to illustrate the difference between these two classes of systems.

We then present sufficient conditions on state-space partitioning ensuring that the symbolic models inherit the monotonicity of the original plant (Assumptions 5.2.1, 5.2.2) and characterize state-monotone and input-state monotone transition systems correspondingly (Theorem 5.2.1 and its corollary). We distinguish lower and upper (input-)state transition system (Definitions 5.2.1, 5.2.2), but until Section 5.3.4, we focus on lower (input-)state monotone system and lower-closed safety specifications, assuming that similar results for upper (input-)state monotone system and upper-closed safety specifications can be derived analogously. We say that a transition system Σ = (Q, U, F ) is lower state monotone if for all q 1 , q 2 ∈ Q, for all inputs u enabled in q 2 if q 1 Q q 2 , then u is enabled in q 1 and F (q 1 , u) ⊆↓ F (q 2 , u). And it is lower input-state monotone if for all q 1 , q 2 ∈ Q, for all inputs u 2 enabled in q 2 if q 1 Q q 2 and u 1 U u 2 , u 1 ∈ U then u 1 is enabled in q 1 and F (q 1 , u 1 ) ⊆↓ F (q 2 , u 2 ). See Figure 1.5 (left) for an illustration. Any

q 1 q 2 q 1 q 2 q 3 q 4 Q =↓ Q = ∪ 4 i=1 ↓ q i F (q 1 , u 1 ) F (q 2 , u 2 ) u 2 u 1 Figure 1.5:
The left figure illustrates that if the transition system is lower input state monotone, then we for any two states q 1 Q q 2 and two inputs

u 1 U u 2 , F (q 1 , u 1 ) ⊆↓ F (q 2 , u 2 ). Right figure shows that a finite lower-closed set Q (i.e. Q s.t. Q =↓ Q) can be represented by its basis Bas(Q) = {q 1 , q 2 , q 3 , q 4 }, since Q =↓ Bas(Q).
finite lower-closed set can be represented by its basis [START_REF] Finkel | Well-structured transition systems everywhere![END_REF] (Figure 1.5 (right)). Hence, to compute the domain of the maximal safety controller for a state-monotone transition system (Theorem 5.3.1), it is enough to iteratively explore only those states, which belong to the basis of controllable domain (Algorithm 5.3).

Moreover, for lower input-state, it is sufficient to use inputs with lower priorities (Theorem 5.3.4). Let us remark that for a lower state-monotone system if a state q is controllable with an input u then all states belonging to ↓ q are controllable with an input u. Moreover if system is lower input-state monotone transition system then additionally if for a state q an input u is safe then all inputs u u are safe. The latter allows us to compute the maximal safety controller for lower (input-)state monotone transition systems lazily (Theorem 5.3.2, Algorithm 5.4 and Algorithm 5.5). We then enrich the class of considered specification by intersections of lower-closed and upper-closed sets in Section 5.3.4. Let us remark that instead of using classical box abstraction we use efficient sparse abstractions proposed in [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF], where the sparse transition relation F S (q, u) = max(F (q, u)), q ∈ Q, u ∈ U. In Figure 1.5 (left) sparse successors are marked with dark blue and green for transitions F (q 1 , u 1 ) and F (q 2 , u 2 ).

Chapter 6. Conclusion and Future Work

In the last chapter, we summarize the results of the thesis and propose several directions for future research.

Publications

The work presented in this thesis led to several papers either published or accepted.

Journal paper:

• Ivanova E., Saoud A. and Girard A. Lazy Chapter 2

Safety Controller Synthesis for Finite

Transition System: How to Speed-Up the

Computations?

As mentioned in the introduction, the successful synthesis requires quite precise abstractions with many states and inputs to be stored and a considerable number of transitions to be computed. Moreover, the complexity of discrete methods used for abstract controller synthesis grows with the size of the symbolic model making synthesis computationally intractable. A demand to overcome a scalability issue of symbolic model approaches reasoned a wave of research in the last decade and motivated writing this thesis. Various methods to reduce the computational effort were proposed. In [START_REF] Kim | Compositional controller synthesis for vehicular traffic networks[END_REF], Meyer et al., 2017, Swikir and Zamani, 2019] the authors use compositional approaches as a common way to tackle the curse of dimensions. However, this research branch is out of the scope of this manuscript, and the interested reader is referred to [Saoud, 2019] and reference therein. Other works benefit from incremental stability [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF], Pola et al., 2010, Saoud and Girard, 2018] or monotonicity [Kim et al., 2017, Sinyakov andGirard, 2020a] to minimize the size of symbolic models. Efficient abstractions were also proposed for differentially flat systems [START_REF] Liu | Reactive controllers for differentially flat systems with temporal logic constraints[END_REF] and for systems exhibiting a sparse interconnection structure [START_REF] Gruber | Sparsity-Sensitive Finite Abstraction[END_REF]. As a solution for general class of systems multi-scale abstractions were introduced [START_REF] Gol | Language-guided controller synthesis for linear systems[END_REF], Girard et al., 2016, Hsu et al., 2019[START_REF] Li | Rocs: A robustly complete control synthesis tool for nonlinear dynamical systems[END_REF], Nilson et al., 2017]. We will return in more detail to all these ideas in the following chapters.

This Chapter is devoted to lazy synthesis approaches for a safety specification. In such approaches, abstractions are computed on-the-fly, restricting computations only to the essential for the synthesis part. Section 2.1 introduces the notion of a finite transition system. Section 2.2 formulates a safety control problem for a transition system and provides a classical algorithm synthesizing maximal safety controller. Section 2.3 starts with a literature review of lazy approaches. Then Subsection 2.3.1 introduces the lazy synthesis algorithm accelerating maximal safety controller computations if the information of a priory controllable states is available. The lazy algorithm in Subsection 2.3.2 benefits from a partial order introduced on the input set. Subsection 2.3.3 proposes to restrict the computations for reachable from initial states only while using incremental search to explore the transition system. All algorithms in Section 2.3 are applicable for non-deterministic transition systems. Section 2.4 summarises the ideas of this Chapter.

Preliminaries

Let us start with the main definitions.

Definition 2.1.1. A transition system is a tuple Σ = (Q, U, F ), consisting of a set of states Q, a set of inputs U , and

a transition relation F ⊆ Q × U × Q. If sets Q, U are finite Σ = (Q, U, F
) is said to be a finite transition system.

In this thesis, we only work with finite transition systems, and from now, we will shortly call them transition systems for simplicity. For every transition (q, u, q ) ∈ F the state q is named u-predecessor of q and similarly the state q is named u-successor of q. For the set of all u-predecessors of the state q the notation F -1 (q, u) is used, while the set of all u-successors of a state q is denoted by

F (q, u). If there is q ∈ Q, u ∈ U such that | F (q, u) | > 1,
then the transition system is called non-deterministic, otherwise it is deterministic. Since F (q, u) may be empty let us introduce a set Enab F (q) = {u ∈ U | F (q, u) = ∅} of all enabled inputs at a state q ∈ Q. If Enab F (q) = ∅, then q is said to be blocking, otherwise it is non-blocking. We also use notation Block F (Q ) to describe the set of all blocking states in a set Q ⊆ Q. If Block F (Q) = ∅, then the transition system is called non-blocking.

Definition 2.1.2. A trajectory of a transition system Σ = (Q, U, F ) is a finite or infinite sequence of transitions

q 0 u0 -→ q 1 u1 -→ q 2 u2 -→ q 3 u3 -→ . . ., s.t. q i ∈ Q, u i ∈ U and q i+1 ∈ F (q i , u i ) for all i ≥ 0. Definition 2.1.3. A controller for a transition system Σ = (Q, U, F ) is a map C : Q → 2 U , such that C(q) ⊆ Enab F (q) for every q ∈ Q. Let us use notation Dom(C) = {q ∈ Q | C(q) = ∅} for a domain of controller C. If Dom(C) = ∅ the controller is called trivial, otherwise non-trivial.

Maximal Safety Controller

Problem 2.2.1 (Safety Specification). For a given transition system Σ = (Q, U, F ) and a safe set Q S ⊆ Q, synthesize a non-trivial controller C such that Dom(C) ⊆ Q S and for any trajectory q 0 u0 -→ q 1 u1 -→ q 2 u2 -→ q 3 u3 -→ . . ., such that q 0 ∈ Dom(C) and u i ∈ C(q i ), i ≥ 0 the following is satisfied: q i ∈ Dom(C) for all i ≥ 0.

A desired controller C is then called a safety controller for transition system Σ = (Q, U, F ) and a safe set Q S ⊆ Q.

Definition 2.2.1. A safety controller for a transition system Σ = (Q, U, F ) and a safe set

Q S ⊆ Q is a controller C such that the following two properties hold 1. Dom(C) ⊆ Q S ;
2. for all q ∈ Dom(C) for all u ∈ C(q) the following inclusion is satisfied F (q, u) ⊆ Dom(C).

Definition 2.2.2. For a given transition system Σ = (Q, U, F ) and a controller C, the controlled transition system

Σ/C = (Dom(C), U, F C
) is a transition system with the reduced transition relation

F C ⊆ F , such that (q, u, q ) ⊆ F C if and only if u ∈ C(q).
Hence, if C is a non-trivial safety controller, then the controlled transition system Σ/C = (Dom(C), U, F C ) is non-blocking and all trajectories of this system belong to the safe set Q S .

Lemma 2.2.1. For a given transition system Σ = (Q, U, F ), a safe set Q S ⊆ Q there exists the unique maximal safety controller C such that for any safety controller C the following hold

1. Dom(C) ⊆ Dom( C);
2. for all q ∈ Dom(C) the inclusion C(q) ⊆ C(q) is satisfied.

Obviously, to solve Problem 2.2.1 means to synthesize a non-trivial safety controller and the maximal safety controller C is the most complete solution one can get. That justifies the following notion of controllability.

Definition 2.2.3. Let Q S be a safe set. A state q ∈ Q of transition system Σ = (Q, U, F ) is safety controllable if and only if q ∈ Dom( C). The set of safety controllable states is denoted Cont(Σ, Q S ).

The algorithm, proposed in [Tabuada, 2009], is the most common way to compute the maximal safety controller.

According to this algorithm, all unsafe transitions are iteratively removed from the transition system until the system stops changing. A transition is safe if it corresponds to an action, preventing the system from steering into a blocking or unsafe state. Otherwise, it is unsafe. The maximal safety controller is initialized to permit all transitions of the resulting system. This simple idea admits various implementations, so let me briefly comment on Algorithm 2.1 (on page 31) and prove that it indeed returns the maximal safety controller. Let a function p : Q → {0, 1} indicates whether a state q ∈ Q is controllable (p(q) = 1) or not (p(q) = 0), and the reduced transition relation F p is defined as follows: (q, u, q ) ∈ F p if and only if p(q) = 0 and for all q ∈ F (q, u) the equality p(q ) = 0 is satisfied. First, all safe states in Q S are marked as controllable, while all states beyond the safe set as uncontrollable (lines 2-5). Then we iteratively explore all potentially controllable states, marking as uncontrollable those which are blocking (lines 6-11). Updating the function p we automatically remove from the transition relation F p all unsafe transitions. When procedure stops, the reduced transition relation is used to initialize the controller C (lines 12-15).

Remark 2.2.1. In the definition of the the reduced transition relation F p we write p(q ) = 0 instead of p("q") = 1 to ease comparison of the result of this section with the results of the following sections.

Lemma 2.2.2. Let Algorithm 2.1 executes for transition systems

Σ 1 = (Q, U, F 1 ), Σ 2 = (Q, U, F 2 ) with safety specifications Q 1 S , Q 2 S correspondingly, and let C 1 , C 2 be returned controllers. Let Q 1 S ⊆ Q 2 S and Enab F 1 (q) ⊆ Enab F 2 (q) for all q ∈ Q. If for all q ∈ Q, u ∈ Enab F 1 (q) the inclusion holds F 2 (q, u) ⊆ F 1 (q, u) then C 1 (q) ⊆ C 2 (q)
for all q ∈ Q.

Proof. The fact that C 1 (q) ⊆ C 2 (q) for all q ∈ Q means that

Enab F 1 p 1 (q) ⊆ Enab F 2 p 2
(q) for all q ∈ Q when the algorithm reach the line 12. Under assumptions of the lemma about transition relations F 1 and F 2 the latter is equivalent to p 1 (q) ≤ p 2 (q) (see the definitions of the reduced transition relations F 1 p1 and F 2 p2 ). Let us now prove that inequality holds. Since Q 1 S ⊆ Q 2 S at line 5 the inequality p 1,0 (q) ≤ p 2,0 (q) obviously holds for all q ∈ Q and this give me induction base. Let p 1,i (q) ≤ p 2,i (q) at the beginning of i iteration of the loop 6-11. Then

Q 1 E,i ⊆ Q 2 E,i and since the transition relation F 1 p1,i is included in F 2 p2,i the set B 2 i is included in B 1 i from where p 1,i+1 (q) ≤ p 2,i+1 (q).
Let us also remark that if at some iteration ĩ the set B 2 ĩ is already empty, while B 1 ĩ is not then the inequality p 1,i (q) ≤ p 2, ĩ(q), q ∈ Q is also obviously holds for all i ≥ ĩ until B i becomes empty as well.

Theorem 2.2.1. Let C computed by Algorithm 2.1. Then, C is the maximal safety controller.

Proof. Let us first remark that since the set Q is finite and with every iteration of the loop, all blocking states are marked as uncontrollable and then never explore again, Algorithm 2.1 always ends its execution. Moreover since F p (q, u) ⊆ F (q, u) for all q ∈ Q, u ∈ U the map C is a controller for the transition system Σ = (Q, U, F ). Let us prove that it is the maximal safety one.

Safety. Let us first show that a state q ∈ Q belongs to Dom(C) if and only if p(q) = 0. If q ∈ Dom(C) then

Enab Fp (q) = 0, consequently, from the definition of F p it follows that p(q) = 0. Let for a state q ∈ Q, p(q) is equal to 0, when the execution reaches the line 12. It means that the state q was in Q E at the last iteration of the loop 6-11 and since the exit condition from the loop is B = ∅ the state q / ∈ Block Fp (Q E ), i.e. there exists u ∈ Enab Fp , consequently, q ∈ Dom(C). Hence, from the definition of F p it follows that for all q ∈ Dom(C) the inclusion F p (q, u) ⊆ Dom(C) is satisfied for all u ∈ Enab Fp , i.e. for all q ∈ Dom(C) and for all u ∈ C(q) the inclusion F (q, u) ⊆ Dom(C). To prove that Dom(C) ⊂ Q S let me suppose the opposite: there exists q ∈ Dom(C) ∩ (Q \ Q S ). Obviously, if some state q was marked as uncontrollable (i.e. p(q) = 0) it stays uncontrollable until the end of Algorithm 2.1 execution. Hence,

if q ∈ Q \ Q S then p(q) = 0, but this contradicts to q ∈ Dom(C).
Maximality. Let C is the maximal safety controller for a transition system Σ = (Q, U, F ) and a safe set Q S . Since C is a safety controller then for all q ∈ Q the following holds C(q) ⊆ C(q). To prove the opposite let me run Algorithm 2.1

for transition system Σ = (Q, U, F C ) and a safe set Dom( C). In this case, the returned controller C obviously coincide with the maximal safety controller C. Since Dom( C) ⊆ Q S and for all q ∈ Q the set Enab F C (q) = Enab F (q), moreover for all u ∈ Enab F (q) sets of successors F C (q, u), F (q, u) are equal, from Lemma 2.2.2 it follows that C(q) ⊆ C(q). This ends the proof.

q us u 1 u 2 u 3 u 1 q 1
q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 2 u 1 u 4 u 3 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 1 u 4 q us u 1 u 2 u 3 u 1 q 1
q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 2 u 1 u 4 u 3 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 1 u 4 u 2 u 2 1 2 q us u 3 u 1 q 1
q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14

q 15 u 3 u 2 u 1 u 2 u 2 u 1 u 4 u 3 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 4 u 2 3 q us u 3
q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 1 u 4 u 3 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 4 4 q us u 3
q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 4 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 4
q us u 3 q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 4 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 6 u 3 u 3 u 3 u 3 u 3 u 3 5 Figure 2.1: Illustration of Algorithm 2.1. Algorithm 2.
1 iteratively removes all unsafe actions from a transition system until the system stops changing. An action is unsafe if it can not prevent the system from steering into an unsafe or blocking state. Unsafe actions are marked with a red color. Blocking states are filled with grey, the unsafe statewith black. A state q with p(q) = 1 is contoured with black, with p(q) = 0 -with red.

Figure 2.1 illustrates the execution of Algorithm 2.1.Starting at step 1 with a simple transition system, we first indicate which state is unsafe. Then at step 3, the unsafe set is initialized with priority 0. Consequently, all actions steering to q us are removed from the system. At steps 4-6, we continue iteratively delete inputs, which can not prevent safety, until at step 6, we get a non-blocking transition system, all trajectories of which belong to Q S = {q 1 , . . . , q 15 }. Though Algorithm 2.1 is sound and complete, it explores all states and all transitions making computations too labor-intensive for many real-world problems, where a considerable number of states and inputs should be explored. In the next section, we introduce more efficient safety synthesis algorithms and discuss their correctness and completeness with respect to the classical synthesis approach.

Lazy Synthesis Algorithms

The obvious way to reduce the computational burden is to avoid computations, which are non-essential for synthesis goals. This is a purpose for lazy synthesis algorithms [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF], Nilson et al., 2017, Hsu et al., 2019, Hussien and Tabuada, 2018, Rungger and Stursberg, 2012, Kader et al., 2019]. Unlike the classical algorithm, in lazy approaches, the system is abstracted parallel with the controller synthesis. Hence, one can avoid calculating the part of the abstraction, which is not involved in the synthesis procedure. The worst-case complexity of lazy approaches usually coincides with the classical synthesis's complexity or can be even higher, but lazy algorithms are more efficient in practice. Lazy synthesis usually requires additional assumptions about a given transition system, and the following three different sources of laziness are mainly considered in the literature:

• priorities on input space. In [START_REF] Hussien | Lazy controller synthesis using three-valued abstractions for safety and reachability specifications[END_REF], once a safe input is found for a state, the other controls are not explored for this state. The authors start with an empty transition relation and iteratively add new transitions essential for the synthesis purpose. At every iteration, the precomputed part of the symbolic model is explored. Then, one randomly chooses N states from uncontrollable states, where N is a parameter

given by the user. For each chosen state, one randomly picks an unexplored input and adds the corresponding tradition to the abstraction. The algorithm returns only the domain of the maximal safety controller and not the whole maximal safety controller. So, in some sense, the authors introduce a random order on the set of inputs and try to solve the problem using as higher priorities actions as possible. In [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF], Nilson et al., 2017, Hsu et al., 2019, Kader et al., 2019] the authors use multi-scale abstractions and prioritize actions with longer duration. The idea to give different inputs different priorities is common while dealing with more general specifications as well. For example, many path-finding algorithms explore the most promising actions [Hart et al., 1968, Rungger and[START_REF] Rungger | [END_REF] first. In cases when specification can not be satisfied, the least-violating [Girard andEqtami, 2021, T ůmová et al., 2012] actions are often favored.

• non-reachable from initial set states. In [Girard et al., 2016, Tripakis andAltisen, 1999] it is also proposed to restrict computations only for states, which are reachable from the initial set. To do so, the authors implement the incremental transition system exploration, which in turn enables the usage of their approach while dealing with more general control problems, such as, for instance, a reach-avoid specification [START_REF] Hsu | Lazy abstraction-based controller synthesis[END_REF], Reissig et al., 2017].

• information about a priory controllable states. If, in addition, the incrementally explored transition system is deterministic, one can mark a state as controllable as soon as a safe loop-path has been found for this state [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF]. These a priory controlled states need not be investigated in future iterations of the synthesis algorithm. Skipping exploration of a part of the transition system is also popular when slightly changing specifications are considered [START_REF] Koenig | Fast replanning for navigation in unknown terrain[END_REF].

We provide three lazy synthesis algorithms Algorithm 2. Input: Σ = (Q, U, F ) and a safe set QS Output: MS controller C 1 begin 2 for q ∈ QS do 3 p(q) := 1;

4 for q ∈ Q \ QS do 5 p(q) := 0; 6 repeat 7 QE := {q ∈ Q | p(q) = 0}; 8 B := BlockF p (QE); 9 for q ∈ B do 10 p(q) := p(q) -1; 11 until B = ∅; 12 for q ∈ QE do 13 C(q) := EnabF p (q); 14 for q ∈ Q \ QE do 15 C(q) := ∅; 16 return C; Algorithm 2.2: LazySynthesisMSC(Σ, Q S , I EB ) Input: Σ = (Q, U, F ), a safe set QS, an indicator IEB Output: MS controller C 1 begin 2 for q ∈ QS do 3 p(q) := 1; 4 for q ∈ Q \ QS do 5 p(q) := 0; 6 repeat 7 QEB := {q ∈ Q | p(q) = 0 and IEB(q) = 1}; 8 B := BlockF p (QEB); 9 for q ∈ B do 10 p(q) := p(q) -1; 11 until B = ∅; 12 for q ∈ {q ∈ Q | p(q) = 0} do 13 C(q) := EnabF p (q); 14 for q ∈ Q \ {q ∈ Q | p(q) = 0} do 15 C(q) := ∅; 16 return C; Algorithm 2.3: MILSC(Σ, Q S , U ) Input: Σ = (Q, U, F ) and a safe set QS Output: MILS controller C. 1 begin 2 for q ∈ QS do 3 p(q) := N ; 4 for q ∈ Q \ QS do 5 p(q) := 0; 6 repeat 7 QE := {q ∈ Q | p(q) = 0}; 8 B := BlockF p, U (QE); 9 for q ∈ B do 10 p(q) := p(q) -1; 11 until B = ∅; 12 for q ∈ QE do 13 C(q) := EnabF p, U (q); 14 for q ∈ Q \ QE do 15 C(q) := ∅; 16 return C; Algorithm 2.4: MSLSC(Σ, Q S , Q init ) Input: Σ = (Q, U, F ), a safe set QS, an initial set Qinit Output: MSLS controller C. 1 begin 2 for q ∈ QS do 3 p(q) := 1; 4 for q ∈ Q \ QS do 5 p(q) := 0; 6 repeat 7 Q R E := ReachF p ({q ∈ Qinit | p(q) = 0}) ; 8 B := BlockF p (Q R E ); 9 for q ∈ B do 10 p(q) := p(q) -1; 11 until B = ∅; 12 for q ∈ Q R E do 13 C(q) := EnabF p (q); 14 for q ∈ Q \ Q R E do 15 C(q) := ∅; 16 return C;
The detailed description of Algorithm 2.

Source of Laziness: Information about A priory Controllable States

This section introduces a lazy Algorithm 2.2, which benefits from information about a priory controllable states.

Definition 2.3.1. Consider Σ = (Q, U, F ) and a set Q E ⊆ Q. We say that a set Q EB ⊆ Q E is an essential basis of set Q E if for all q ∈ Q E \ Q EB the set Enab F (q) = ∅ and for all u ∈ Enab F (q) the following holds F (q, u) ⊆ Q E . q us u 1 u 2 u 3 u 1 q 1
q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 2 u 1 u 4 u 3 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 1 u 4 u 2 1 q us u 1 u 2 u 3 u 1 q 1
q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 2 u 1 u 4 u 3 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 1 u 4 u 2 2 u 3 u 3 q us u 3 u 1 q 1
q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 2 u 1 u 4 u 3 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 4 u 2 3 u 3 q us u 3
q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 1 u 4 u 3 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 4 4 u 3 q us u 3
q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 4 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 4 5 u 3 q us u 3
q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 4 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 5 u 3 Figure 2
.2: Illustration of Algorithm 2.2 execution.Blocking states are filled with grey. The unsafe state is black. A state q such that p(q) = 1 are contoured with black, with p(q) = 0 -with red. Let us remark that all transitions in the system are between neighboring states. Hence, we can restrict exploration to those states that border with blocking or unsafe states. The unexplored elements are marked with the dashed line, while the normal line denoted states already involved in computations. At the end of execution, states q 8 , q 4 stay unconsidered, but we can automatically mark them as controllable, including all actions enabled at these states to the maximal safety controller.

Hence, if at some iteration of Algorithm 2.1 a set Q EB is an essential basis of a set Q E , then all states q ∈ Q \ Q E are controllable a priory at this iteration and the following result is true.

Theorem 2.3.1. Let a set Q E = {q ∈ Q | p(q) = 0}
and let at every iteration of the loop 6-11 of Algorithm 2.2 the

set Q EB = {q ∈ Q E | I EB (q) = 1}
is essential basis of Q E then the controller C computed by Algorithm 2.2 is the maximal safety controller.

Proof. Indeed, from Definition 2.3.1 and definition of the reduced transition relation F p it follows that for all q ∈ Q E such that I EB (q) = 0 the set Enab Fp (q) = 0, consequently q / ∈ B at every iteration of the loop 6-11.

Hence, in the general case, Algorithm 2.2 does not return a safety controller. However, if the information function

I EB : Q → {0, 1}
distinguishes a priory controllable on the current iteration states from those which should be explored, then Algorithm 2.2 synthesize the maximal safety controller. The idea is simple, but the main intrigue is in determining the information function I EB , which is different from an indicator of a set

Q E = {q ∈ Q | p(q) = 0}.
For instance, in our illustrative example (see Figure 2.2), all states are linked only with their neighbors. Hence, iteratively explore only those states that surround blocking or unsafe states is enough. The latter speed up computation in comparison with the classical approach. Moreover, states q 4 , q 8 were never involved in computations, and the corresponding part of the abstraction may remain uncalculated. Of course, in a general system, transitions between non-neighboring states are possible. Still, in Chapter 3, we show how one can ensure that the abstraction (constructed for the original dynamic system) has the desirable structure by using adaptive time sampling techniques.

Another way to get necessary information about a priory controllable states is to benefit from the monotonicity of the systems as we do in Chapter 5.

Source of Laziness: Inputs' Priorities

The ideas of this subsection and the following one were first introduced in [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF]. However, they were restricted to deterministic transition systems. The results provided in this manuscript are applicable for nondeterministic systems as well.

Assumption 2.3.1. Let the set of inputs U be split into N non-intersecting subsets U = U 1 ∪ U 2 . . . ∪ U N and for all u ∈ U i , u ∈ U j , i < j, i, j ∈ {1, . . . , N } it holds that u ≺ u , while inputs u , u belonging to the same subset are considered as equivalent u u .

I.e., it is supposed that a set of inputs U is equipped with a partial order. Then if for some state several inputs preserve safety, it is reasonable to keep only those that have the highest priority. Here we say that an input u ∈ U has higher priority than u ∈ U if and only if u u .

Definition 2.3.2. For a given transition system Σ = (Q, U, F ), a safety specification Q S ⊆ Q a maximal inputs-lazy safety (MILS) controller C * is a safety controller satisfying the following properties

1. Dom(C * ) = Cont(Σ, Q S );
2. for all states q ∈ Dom(C * ):

(a) if u ∈ C * (q) then for all u ∈ Enab F (q) such that u u, it holds that u ∈ C * (q) if and only if

F (q, u ) ⊆ Cont(Σ, Q S ); (b) if u ∈ C * (q), then for all u ∈ Enab F (q) with u ≺ u , it holds that F (q, u ) ∩ Cont(Σ, Q S ) = F (q, u ).
A MILS controller is a particular case of the maximal lazy safety (MLS) controller introduced in [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF].

It corresponds to a situation when an initial set coincides with a safe set. The MLS controller exists for any transition system, and it is unique [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF]. Consequently, a MILS controller exists and is unique, as well. The term maximal refers to the fact that all safety controllable states are in Dom(C * ), and if the controller enables an input, it also enables all inputs which have the same priority and preserve safety. The term inputs-lazy refers to the fact that while several inputs can maintain safety, the controller enables only inputs with the highest priority. Hence, C * represents a trade-off between maximal permissiveness and efficiency. Intuitively, the MILS controller C * can be obtained from the maximal safety controller C by keeping, for every state, only those enabled controls which have a higher priority. Of course, it is not the best way to find C * since it needs first to compute C.

The main idea of a more efficient algorithm for computing the MILS controller is to explore inputs with a lower priority only if we failed to find a safe input with a higher priority. For its implementation, we introduce for every state q ∈ Q a notion of a state priority p(q) and define for a given p : Q → {0, . . . , N } a reduced transition relation F p, U such that (q, u, q ) ∈ F p, U if and only if p(q) ∈ {1, . . . , N }, u ∈ U p(q) , (q, u, q ) ∈ F and for all q ∈ F (q, u) the equality p(q ) = 0 is satisfied. Intuitively, this means that for states with priority from 1 to N, only transitions with the same priority inputs are considered, while states with priority 0 are blocking. Let us now prove that the second property of Definition 2.3.2 is satisfied. For any q ∈ Dom(C) a control u ∈ C(q)

if and only if u ∈ Enab F p, U (q). Then for any u ∈ Enab F (q) ∩ U p(q) we have: if u ∈ Enab F p, U (q) then F (q, u ) =

F p, U (q, u ) ⊆ Dom(C) ⊆ Cont(Σ, Q S ), because C is a safety controller; if F (q, u ) ⊆ Cont(Σ, Q S )
then there is no q ∈ F (q, u ) such that p(q ) = 0 and u ∈ Enab F p, U (q). So, we have (2a). The (2b) follows from the fact that we decrease the priority p of a state q, if either Enab F (q) ∩ U p(q) = ∅, or for all u ∈ Enab F (q) ∩ U p(q) there exists q ∈ F (q, u) such that p(q ) = 0. with actions u 1 , u 2 . At the beginning (step 3), all states except q us get priority 2. Then, if a state q is blocking concerning its current priority at some step, we decrease p(q) by one point. The latter either enable for this state actions with a lower priority (see, for example, a state q 14 at step 6), or delete all unsafe inputs steering to state q (if q get a 0 as, for example, q 15 at step 7).

q us u 1 u 2 u 3 u 1 q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 2 u 1 u 4 u 3 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 1 u 4 u 2 q us u 1 u 2 u 3 u 1 q 1
q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 2 u 1 u 4 u 3 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 1 u 4 u 2 q us u 3 u 1 q 1
q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 2 u 1 u 4 u 3 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 4 u 2 q us u 3 u 1 q 1
q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 2 u 1 u 4 u 3 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 4 u 2 1 2 3 4 q us u 2 u 3
q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 1 u 4 u 3 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 4 5 q us u 3
q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 1 u 4 u 3 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 4
q us u 3 q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 4 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 4 6 7 q us u 3
q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 4 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 4
q us u 3 q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 4 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 8 9 u 3 u 3 u 3 u 3 u 3 u 3 u 3 u 3 u 3 Figure 2

Source of Laziness: Non Reachable from Initial Set States

Let us suppose that the initial set Q init ⊆ Q is fixed. In this case, we have no interest in providing a controller for non-reachable from Q init states.

A state q ∈ Q is reachable from the state q, if q = q or there exists a trajectory connecting them. The set of all reachable states from the state q is denoted by Reach F (q). This definition could be naturally extended for a subset

Q of the set of states Q: Reach F (Q ) = ∪ q∈Q Reach F (q).
Definition 2.3.3. For a given transition system Σ = (Q, U, F ), a safety specification Q S ⊆ Q, and a fixed initial set Q init ⊆ Q a maximal states-lazy safety (MSLS) controller C * is a safety controller satisfying the following properties

1. Q init ∩ Cont(Σ, Q S ) ⊆ Dom(C * );
2. for all states q ∈ Dom(C * ) the input u ∈ C * (q) if and and only if

F (q, u) ⊆ Cont(Σ, Q S ). 3. Dom(C * ) ⊆ Reach F C * (Q init ∩ Dom(C * ));
An MSLS controller is a particular case of the maximal lazy safety controller introduced in [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF]. It corresponds to a situation when all inputs have the same priorities. Since the MLS controller exists for any transition system and it is unique [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF]

= {q ∈ Q | p(q) = 0}. While running the Algorithm 2.4, the intersection Q zero ∩Cont(Σ, Q S )
is always empty.

Proof. Let us use induction to prove this fact. Before the loop 8-12, the set Q zero consists only of unsafe (see line 6) and, as a consequence, uncontrollable states. In the loop, Q zero updates only when some state q ∈ B ⊆ Q gets at line 11 a prioryty zero. Supposing that

Q i zero ∩ Cont(Σ, Q S ) = ∅ let us show that Q i+1 zero ∩ Cont(Σ, Q S ) = ∅, where Q i+1 zero = Q i zero ∪ {q}.
So, let us show, that q ∈ Cont(Σ, Q S ). Since p(q) got value 0 either Enab F (q) = ∅, or for all u ∈ Enab F (q) there exists q ∈ F (q, u) \ {q} such that p(q ) = 0, i.e q ∈ Q i zero and q / ∈ Cont(Σ, Q S ). Hence, C(q) is empty and q is uncontrollable.

Theorem 2.3.3. Let C computed by Algorithm 2.4. Then, C is the MSLS controller.

Proof. We start with safety. Since Dom(C) coincide with the set Q R E and all unsafe states are non-reachable we have Dom(C) ⊆ Q S . Moreover, from the definition of Reach operator we have that for all q ∈ Dom(C) and for all u ∈ U it holds F p (q, u) ⊆ Dom(C). Combining with the fact that for all q ∈ Dom(C) and for all u ∈ Enab Fp (q) the set F p (q, u) coincides with F (q, u), the second requirement from Definition 2.2.1 is satisfied. Now, let us show that all properties of MSLS controller are satisfied (see Definition 2.3.3). Let q ∈ Cont(Σ, Q S ) ∩ Q init . It is equivalent to q ∈ Q init and q ∈ Cont(Σ, Q S ). From where, using the Lemma 2.3.1, we get that q ∈ Q init u 2 q us u 1 u 2 u 3 u 1 q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 2 u 1 u 4 u 3 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 1 u 4 q us u 1 u 2 u 3 u 1 q 1
q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 2 u 1 u 4 u 3 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 1 u 4 u 2 u 2 1 2 q us u 3 u 1 q 1
q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14

q 15 u 3 u 2 u 1 u 2 u 2 u 1 u 4 u 3 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 4 u 2 3 q us u 3
q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 1 u 4 u 3 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 4 4 q us u 3
q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 4 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 u 4
q us u 3 q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

u 3 u 2 u 1 u 2 u 4 u 4 u 1 u 2 u 2 u 3 u 1 u 1 u 2 u 2 6 u 3 u 3 u 3 u 3 u 3 u 3 5 u 2 u 1 u 2 u 2 u 1 u 1 Figure 2
.4: Illustration Algorithm 2.4 execution. Unsafe actions are red, blocking states are grey, and the initial states are marked with a double line. The computations are restricted to states, which reachable from the initial set.

States which are non-reachable from the initial set are countered with a dashed line. Hence, states q 11 , q 12 and q 8 are not included in the domain of the maximal state lazy safety controller.

and p(q) = 0. Consequently, q ∈ Q R E = Dom(C) (see line 7,13), and the first property is satisfied. If a state q ∈ Dom(C * ) then the set F (q, u) ⊆ Cont(Σ, Q S ) for all u ∈ C * (q) since C * is a safety controller. If for an input u ∈ U the set F (q, u ) ⊆ Cont(Σ, Q S ) then there is no q ∈ F (q, u ) such that p(q ) = 0 and u ∈ Enab Fp (q) and we have the second property. The third property follows straightforwardly from line 7.

Figure 2.4 provides an illustration of Algorithm 2.4. Assuming the set of initial states is known we restrict all computations to states, which are reachable from Q init = {q 1 , q 2 , q 5 , q 6 }.

Conclusion

This Chapter structured the existing lazy safety approaches and provided three lazy synthesis algorithms applicable for a general class of non-deterministic transition systems. Algorithm 2.2 avoid exploration of states and transitions which are safely controllable a priory. Algorithm 2.3 explores the lower-priority actions only if the safety problem is unsolvable with higher-priority actions. Based on the incremental exploration of the transition system, Algorithm 2.4 restricts computations for reachable from initial set states only. Let us remark that Algorithms 2.2, 2.3 and 2.4 can be easily combined in one in order to get as maximal gain in efficiency as possible. Later in the manuscript, we provide examples of applying these algorithms in abstraction-based control synthesis approaches. In Chapter 3, using adaptive time-sampling techniques, we construct abstractions where transitions only between neighboring states are allowed and then use the Algorithm 2.2 for efficient synthesis of the maximal safety controller. In Chapter 4, we combine Algorithms 2.3 and 2.4 to synthesise a maximal input-state lazy safety controller for a multi-scale symbolic model. In Chapter 5, we adopt ideas of Algorithms 2.2 and 2.3 to synthesize the maximal input-lazy safety controller for monotone transition systems. We also prove that for this particular class of systems, the maximal safety controller can be reconstructed from the maximal input-lazy safety controller without any computation.

Chapter 3

Lazy Symbolic Controller for

Continuous-Time Systems Based on Safe

Set Boundary Exploration

In this Chapter, we propose an abstraction-based approach to synthesize a safety controller solving Problem 1.1.1.

The main idea consists in creating an abstraction with a particular geometrical structure where only transitions between neighboring states are allowed. Let us call such transition systems neighbor-linked. Though neighborlinked abstractions often appear in path-finding problems [START_REF] Hart | A formal basis for the heuristic determination of minimum cost paths[END_REF], in the general case, symbolic models constructed for an arbitrary dynamic system do not have the desired property. Indeed, in the existing methods, [START_REF] Mazo | Pessoa: A tool for embedded controller synthesis[END_REF], Mouelhi et al., 2013, Wongpiromsarn et al., 2011], a time is usually sampled with a given frequency, and it is the local speed of the controlled dynamic system, which determines how far away from the initial symbolic state a transition ends. However, if all trajectories of the original plant are continuous, we can force the desired structure by interrupting transitions just before leaving the abstract state neighborhood. Related to event-triggered control approaches [Liu et al., 2014, Peng and[START_REF] Peng | [END_REF] such adaptive time sampling technique is a contribution of this thesis.

As it was already briefly discussed in Chapter 2, we then can benefit from the neighbor-linked structure of the proposed abstraction and synthesize the maximal safety controller lazily by iteratively exploring only those states which border with unsafe or blocking states. The lazy synthesis is more efficient than the classical approach; moreover, it does not calculate the unexplored part of the abstraction. Unfortunately, using adaptive time sampling, we lose the flexibility to discretize time and state-space independently. But what if we can restrict exploration to boundary states even when arbitrary time sampling is used to get a symbolic model? Let us run Algorithm 3.2 for an arbitrary transition system. Of course, in this case, there is no guarantee that the synthesized controller is safe, but it still can be refined to solve Problem 1.1.1. Indeed, when a closed-loop trajectory of the original system reaches a boundary state of the controllable domain, we have the abstract controller to push the system back towards the interior where any input, which is permissible for the original system, can be applied. In spirit, this idea is close to the Nagumo theorem result ( [Blanchini, 1999]) and extreme aiming principle ( [Subbotin, 1995]), but to the best of our knowledge, it has never been implemented within the abstraction-based control synthesis framework.

This Chapter is organized as follows. In Section 3.1 we introduce a novel adaptive time-sampling technique and use it to construct neighbor-linked symbolic models for the original system. The particular structure of the abstractions allows synthesizing the maximal safety controller lazily, benefiting from the information about a priori controllable states. We then extend the proposed approach towards arbitrary transition systems from Section 3.2 by introducing a novel control refinement scheme in Section 3.3. In Section 3.4 we consider an illustrative example (adaptive cruise control problem) to show the benefits of the approach.

Neighbor-Linked Abstractions

In Problem 1.1.1, we aim to synthesize a controller for a continuous-time control system

Σ f = (T , R nx , U, W, f )
that maintains all closed-loop trajectories within a safety set Y ⊂ R nx . Let us also remind that the dynamic of

Σ f = (T , R nx , U, W, f ) is given by eq.(1.1): ẋ(t) = f (x(t), u(t), w(t)), t ∈ T , u(t) ∈ U ⊂ R nu , w(t) ∈ W ⊂ R nw ,
where U, W are compact sets. Let us suppose for this Chapter that set Y is a compact as well. To solve the Problem 1.1.1 we use abstraction-based synthesis techniques, and this section is devoted neighbor-linked abstractions for continuous dynamical systems. To enforce the abstraction's desired structure, we first introduce a novel time sampling technique allowing interrupt transitions before leaving an abstract state neighborhood. Then we define an information function that distinguishes boundary states of a set from the inner states and proves that at every iteration of lazy synthesis Algorithm 3.2 it is enough to explore only those states which border with the uncontrollable domain.

Adaptive Time Sampling as Way to Enforce the Desired Structure

Let us first abstract the original system Σ f = (T , R nx , U, W, f ) with a transition system Σ = (Q, U, F ), which have a particular geometric structure: only transitions between neighboring states are allowed.

We first introduce a finite partitioning Q S = {q 1 , . . . , q n } on an internal approximation S of the safety set Y such that S = ∪ n i=1 q i , q i ∩ q j = ∅ for all i = j and define a set of abstract states Q, as follows Q = Q S ∪ {q us }. Here q us = R nx \ S is an unsafe state. We also formally define a neighborhood of a state q ∈ Q, as follows

N A (q) = {q ∈ Q \ {q} | cl(q) ∩ q = ∅ or q ∩ cl(q ) = ∅},
where cl(q) denotes a closure of a set q ⊂ R nx . Thus, depending on the context, a symbol q represents an abstract

q q u 1 u 1 u 2 u 2 N A (q) Reach(τ A q,u | q, u1) Reach(τ A q,u | q, u2) Reach(τfix | q, u1)
Reach(τfix | q, u2) . Black cells represent unsafe states; green and blue cells represent F (q, u 1 ) and F (q, u 2 ) correspondingly. The red square represents the abstract state neighborhood N A (q). While in the left figure, transition duration is determined by pre-fixed time sampling parameter τ f ix , in the right figure, a transition stops just before leaving N A (q) (see eq. (3.2)).

state or a subset of the space R nx , corresponding to this abstract state. Then for every q ∈ Q S we chose a finite number of admissible inputs U S (q) = {u 1 , . . . , u m } ⊆ U and use reachability analysis techniques to compute corresponding transitions. Let Reach(t | q, u S ) be a reachable set

Reach(t | q, u S ) = x ∈ R nx | ∃ x(0) ∈ q and ∃ w ∈ L ∞ ([0, t], W) such that x f (t | x(0), u, w) = x .
corresponding to an initial set q, a constant control function u : [0, t] → u S , u S ∈ U S (q) and admissible disturbances w ∈ L(T , W). We, then define a set U = ∪ q∈Q S U S (q) and say that for every q ∈ Q, u ∈ U transition (q, u, q ) ∈ F if and only if

q ∈ Q S , u ∈ U S (q), q ∈ Q, q ∩ Reach(τ A q,u | q, u) = ∅, (3.1)
and for all t ∈ [0, τ A q,u ] the condition of a collision avoidance Reach(t | q, u) ∩ (R nx \ Y ) = ∅ is satisfied. Here, we use the adaptive time-sampling and a transition duration defined as τ A q,u = min(τ, τ q,u -ε), where τ is a given parameter which determines the maximal evolution time, while τ q,u is a moment of time

τ q,u = inf t∈[0,+∞) Reach(t | q, u) ⊆ N A (q) (3.2)
when the reachable set leaves the neighborhood of N A (q), we chose ε < τ q,u arbitrary small to stop evolution just before leaving. In contrast, τ should be big enough since it only manages situations when a solution stucks within the box. Figure 3.1 illustrates the difference between fixed time sampling and adaptive time sampling techniques.

Both subfigures show two transitions originating at a state q and corresponding to two different controls u 1 and u 2 .

However, transitions in the left figure have a pre-fixed duration τ f ix , while in the right, transitions interrupt just before leaving the abstract state neighborhood. for q ∈ B do 10 p(q) := p(q) -1;

11 until B = ∅; 12 for q ∈ {q ∈ Q | p(q) = 0} do 13 C(q) := EnabF p (q); 14 for q ∈ Q \ {q ∈ Q | p(q) = 0} do 15 C(q) := ∅; 16 return C;
When the dynamic of the original system Σ f = (T , R nx , U, W, f ) is too complex to find exact attendance sets its over-approximations Reach(τ A q,u | q, u) are commonly used instead. Obviously, to get a whole symbolic model, one should estimate quite a lot of reachable sets and we recommend to use simple interval over-approximations [START_REF] Meyer | Interval Reachability Analysis.Bounding Trajectories of Uncertain Systems with Boxes for Control and Verification[END_REF], Maidens and Arcak, 2014, Zamani et al., 2011, Reissig et al., 2017] trading accuracy for efficiency. Moreover, interval estimations match well with grid-aligned partitions, which are often used in symbolic model control [START_REF] Mazo | Pessoa: A tool for embedded controller synthesis[END_REF], Mouelhi et al., 2013, Wongpiromsarn et al., 2011]. A transition is safe if it corresponds to an action preventing the system from steering into a blocking or unsafe state. Otherwise, it is unsafe.

Maximal Safety Controller Synthesis: Inner States as a Source of Laziness

In this section, we aim to synthesize the maximal safety controller for the constructed transition system. I.e., we are looking for the maximal by inclusion controller C, ensuring that all closed-loop trajectories of Σ = (Q, U, F ) starting in Dom(C) are infinite and belong to the safe set Q S .

To compute the desired controller one can iteratively remove all unsafe transitions from Σ = (Q, U, F ) until the abstraction stops changing [Tabuada, 2009]. Let a function p : Q → {0, 1} indicates whether a state q ∈ Q is controllable (p(q) = 1) or not (p(q) = 0), and the reduced transition relation F p is defined as follows: (q, u, q ) ∈ F p if and only if p(q) = 0 and for all q ∈ F (q, u) the equality p(q ) = 0 is satisfied. Then, Algorithm 3.1 returns the maximal safety controller. This statement was proved in Chapter 2, where the classical synthesis Algorithm 3.1 was referred to as Algorithm 2.1. However, since the abstraction Σ = (Q, U, F ) is neighbor-linked we can synthesize the controller more efficiently. Let the information function I EB be defined by (3.3). Then, in opposite to Algorithm 3.1, Algorithm 3.2 explores only boundary states of a set Q E = {q ∈ Q | p(q) = 0} at every iteration of the loop 6-11.

Tacking into account that Algorithm 3.2 coincides with Algorithm 2.2 from Chapter 2 and it is repeated here to improve the readability of the text, let us now prove the correctness of the proposed lazy synthesis approach.

Theorem 3.1.1. For a given transition system Σ = (Q, U, F ) and a safe set Q S = Q \ {q us } let at every iteration of the loop 6-11 of Algorithm 3.2 for all q ∈ Q E = {q ∈ Q | p(q) = 0} the information function is defined as follows

I EB (q) =      0 if N A (q) ⊆ Q E 1 if N A (q) ⊆ Q E (3.3)
Then the controller C returned by Algorithm 3.2 is the maximal safety controller for transition system Σ = (Q, U, F ) and a safe set

Q S = Q \ {q us }.
Proof. Indeed, F (q, U ) ⊆ N A (q) for any q ∈ Q E . Consequently, at every iteration of the loop 6-11 of the Algorithm 3.2, the set

Q EB = {q ∈ Q E | I EB (q) = 1} is an essential basis of Q E = {q ∈ Q | p(q) = 0} (see Definition 2.
3.1) and by Theorem 2.3.1, C is the maximal safety controller.

What if the Abstraction is not Neighbor-Linked?

In the previous section, we construct a neighbor-linked symbolic model for the original system. That allows us to use efficient Algorithm 3.2 instead of the classical synthesis approach Algorithm 3.1 for the maximal safety controller computation. However, with the transition relation defined in Section 3.1.1, we lost flexibility in scaling time sampling parameters independently from space sampling parameters. In this section, we consider a more general case. Let us define a transition relation F * ⊆ Q × U × Q as follows for every q ∈ Q, u ∈ U a transition (q, u, q ) ∈ F * if and only

q ∈ Q S , u ∈ U S (q), q ∈ Q, q ∩ Reach(τ * q,u | q, u) = ∅ (3.4)
and for all t ∈ [0, τ * q,u ) the collision avoidance condition Reach(t | q, u) ∩ (X \ S) = ∅ is satisfied. In opposite to (3.1), in (3.4), we only assume that sampling parameter τ * q,u is greater than zero, and it is determined for any given q ∈ Q, u ∈ U . Such a definition does not put any requirements on a choice of time-sampling parameters permitting us to handle fixed ( [START_REF] Nilsson | Correct-by-Construction Adaptive Cruise Control: Two Approaches[END_REF]), multi-scale ( [START_REF] Hsu | Lazy abstraction-based controller synthesis[END_REF], Girard et al., 2016]) or adaptive time-samplings described in the previous section in a unified way.

It is clear that if we use Algorithm 3.2 synthesize a controller C for the abstraction Σ * (Q, U, F * ), the safety set Q S and the information function I EB (q) defined by (3.3), there is no guarantee that C is a safety controller. However, in the next section, we show that C can still be refined towards a continuous-time controller, which solves the original safety problem.

Controller Refinement for an Arbitrary Abstraction

Let C be a controller given by the Algorithm 3.2 for transition system Σ * = (Q, U, F * ) and a safe set Q S = Q \ {q us }, while the I EB (q) is defined as in (3.3). For every q ∈ Q A \ Dom(C), we define C dur (q) = ∅, while if q ∈ Dom(C) and u ∈ C(q), then the pair (u, τ * u,q ) ∈ C dur (q). Hence, the controller C dur store not only safe inputs, but a real duration of safe transitions. Let us now define a set of border points

Q B = cl {x ∈ R nx | ∃ q ∈ Dom(C) such that x ∈ q and N A (q) ⊆ Dom(C)})
and a set of all internal points Q I = Dom(C) \ Q B correspondingly. We then define a quantizer, associating every border point x ∈ Q B with a state of transition system

Q x (x) = {q ∈ Dom(C) | x ∈ cl(q)}.
If there are several states q ⊂ Q B such that x belongs to q, let Q x (x) returns any of them.

Now we are ready to introduce a controller refinement procedure. Let us consider the control input given for all

t ∈ [t k , t k+1 ) by      u(t, x) ∈ U if m k = 0 u(t, x) = u k , if m k = 1 (3.5) where      m k (t, x) = 0, if x(t k ) ∈ Q I m k (t, x) = 1, if x(t k ) ∈ Q B (3.6) (u k , τ k ) ∈ C dur (Q x (x(t k ))), if m k (t, x) = 1 (3.7)
and the sequence of instants {t k } is given by t 0 = 0 and Let us remark, that while starting inside the set Q I in the mode 0 we can apply any admissible closed-loop control: e.g. u(t, x) = v(t, x). A closed-loop control v(t, x) is admissible if the solution of ẋ(t) = f (x(t), v(t, x), w(t)), t ∈ T q 1 q 6 q 11 q 16

     t k+1 = inf{t > t k | Q x (x(t)) ∈ Q B } if m k = 0 t k+1 = t k + τ k if m k = 1 (3.
q 21 q 22 q 2 q 3 q 4 q 5 q 10 q 23 q 24 q 20 q 15 q 19 1 2 3 4 5 6

q 17 q 18 q 12 q 13 q 14 q 7 q 8 q 9 q us q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15 q 16 q 17 q 18 q 19 q 20 q 21 q 22 q 23 q 24 q us q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15 q 16 q 17 q 18 q 19 q 20 q 21 q 22 q 23 q 24 q us q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15 q 16 q 17 q 18 q 19 q 20 q 21 q 22 q 23 q 24 q us q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15 q 16 q 17 q 18 q 19 q 20 q 21 q 22 q 23 q 24 q 1 q 6 q 22 q 17 q 2 q 3 q 4 q 5 q 10 q 14 q 18 q 23 q 19 q 15 . . . exists and v(t, x) ∈ U for all t ∈ T and x ∈ R nx .

Let us now illustrate the ideas discussed in this Chapter. In step 1 in Figure 3.2, we introduce a Cartesian partitioning on R 2 and mark intervals q 1 , . . . , q 24 as safe abstract states, since they are included in the safe set Y .

We then represent the region R 2 \ (∪ 24 i=1 q i ) by an unsafe state q us . On step 2, we initialize q us with priority zero, while all the others with priority 1. Then we compute transitions only for states which are bordered with the unsafe region. Indeed, since all the internal states (marked with green) are not explored in the first iteration of the loop 6-11, there is no need to pre-compute the symbolic model for them. In step 3, the blocking state q 24 gets priority zero. Hence, we should re-update the set Q EB on step 4 and compute transitions corresponding to q 18 ∈ Q EB . We then re-explore all states in Q EB . Since by the definition of F p , we eliminate all transition steering into q 24 , states q 21 , q 20 become blocking, and we reduce their priority by one point. We then re-update the set Q EB on step 5 and compute transitions originated in q 14 , q 17 ∈ Q EB . On step 5, for any state in Q EB , all transitions go either to another state in Q EB or to an internal state, and we exit the loop 6-11. However, if the abstraction is not neighbor-linked, there is no guarantee that controller C synthesized with lines 12-15 is a safety controller for abstraction. Indeed, for internal states, we may have actions over-jumping the "controllable border in Q I infinitely long, but this behavior is also safe. In step 6, we start from x ∈ q 1 ∈ Q B . We apply the available abstract controller u 2 , and it can bring us to state q 12 ∈ Q I or q 6 ∈ Q B . Suppose that we end up on q 12 ∈ Q I , then we can apply any controller until the trajectory runs into the state q 4 ∈ Q B . There we apply abstract input u 1 and in τ * q4,u1 reach q 3 ∈ Q EB , where we use u 2 for τ * q3,u2 seconds and so on.

Numerical Illustration: Adaptive Cruise Control

As an illustrative example, let us consider the adaptive cruise control problem for two vehicles moving along a straight line ( [Darbha, 1997], [START_REF] Nilsson | Correct-by-Construction Adaptive Cruise Control: Two Approaches[END_REF]). Each vehicle is modeled as a point mass m with velocity changing according to the law

vi = α(F i , v i ) = (F i -(f 0 + f 1 v i + f 2 v 2 i ))/m, i = 1, 2.
In equation above, F i represents a net action of braking and engine torque applied to the wheels, while the second First, we do a feedback linearization of the model for controlled vechile by introducing F 2,lin = α(F 2 , v 2 ). Let us assume that the first car doesn't violate speed restrictions

term (f 1 + f 2 v i + f 3 v 2 i )
v 1 ∈ [0, v max ]. Since for any v 2 ∈ [0, v max ], zero belongs to [α(a, v 2 ), α(b, v 2 )]
we can always choose a suitable control law to do the same for the second car.

Then, we chose a feedback stabilizer as a control law

F 2,lin = u 1 + u 2 (v 1 -v 2 ) + u 3 e 1,2 . Here u 1 ∈ R, u 2 , u 3 ≥ 0.
The deviation e 1,2 from the desirable distance between the cars changes according to the following equation ė1,2 = (v 1 -v 2 ) -ḋdes where d des = hv 2 + r, h > 0.

Hence, the constant time headway spacing policy is considered [Darbha, 1997] (see Figure 3.3 for an illustration).

Finally, the system dynamic is described as follows

v1 = (F 1 -f 0 -f 1 v 1 -f 2 v 2 1 )/m v2 = β(u 1 + u 2 (v 1 -v 2 ) + u 3 e 1,2 , v 2 ) ė12 = v 1 -v 2 -h v2 (3.9)
where

β(z, v) =              z, if v ∈ (0, v max ) max(z, 0), if v = 0 min(z, 0), if v = v max
Varying the new control parameters u 1 , u 2 , u 3 we want to keep the error e 1,2 in a range [-hv 2 -r, e max 1,2 ], while

ensuring that u 1 + u 2 (v 1 -v 2 ) + u 3 e 1,2 ∈ [α(a, v 2 ), α(b, v 2 )].
To construct a symbolic model we introduce on a set Table 3.1: Vehicle and safety parameters. The values are taken from [Darbha, 1997, Saoud et al., 2020].

Parameter Value Unit Parameter Value Unit m 1370 Kg v max 25 m/s f 0 51.0709 N h 2 s f 1 0.3494 N s/m r 2.5 m f 2 0.4161 N s 2 /m 2 e max 1,2 55 m Y = [0, v max ] × [0, v max ] × [-hv max -r,
u = [u 1 , u 2 , u 3 ], ensuring that F 2,lin ∈ [α(a, v 2 ), α(b, v 2 )],
and apply them τ, τ /2, τ /4 or τ /8 seconds.

To compute the symbolic model we use interval over-approximations instead of reachable sets. Let us use notation x = (v 1 , v 2 , e 12 ). The system (3.9) is a mixed-monotone (see Appendix A) and hence for any given state q = [x q , x q ], any given constant control function u : [0, t] → u the following inclusion holds for a reachable set

Reach(t | q, u) robust to all admissible disturbances F 1 ∈ L(T , [a, b]) Reach(t | q, u) ⊆ [x g (t | [x q , x q ], u, F 1 ), x g (t | [x q , x q ], u, F 1 )].
In the equation above, trajectories x g (t | [x q , x q ], u, F 1 ), x g (t | [x q , x 0 ], u, F 1 ) are correspondingly first three and second three components of the solution of the following system

ẋi = g i (ζ i (x, x), [u, u], [b, a]), x i (0) = x q i ẋi = g i (ζ i (x, x), [u, u], [a, b]), x i (0) = x q i where (ζ i (y, z)) j =              y j , j < 3 z j , j > 3, j = 3 + i y i , j = 3 + i i = 1, 3, j = 1, 6 (3.10)
Here the tight decomposition function g :

R 6 × (u, u) × [a, b] 2 → R 3 is defined as follows, g 1 ([y; z], [u; u], [F y 1 ; F z 1 ]) = (F y 1 -f 0 -f 1 v z 1 -f 2 (v z 1 ) 2 )/m g 2 ([y; z], [u; u], [F y 1 ; F z 1 ]) = β(u 1 + u 2 (v y 1 -v y 2 ) + u 3 e y 1,2 , v y 2 ) g 3 ([y; z], [u; u], [F y 1 ; F z 1 ]) =      (1 -h * u 2 )(v y 1 -v z 2 ) -hu 3 e y 1,2 -hu 1 , if 1 -hu 2 ≥ 0 (1 -h * u 2 )(v z 1 -v y 2 ) -hu 3 e y 1,2 -hu 1 , otherwise where y = [v y 1 , v y 2 , e y 1,2 ], z = [v z 1 , v z 2 , e z 1,2 ].
Hence, to find a reachable set over approximation it is enough to solve 6 differential equations (3.10). Let is remark that collision avoidance condition Reach(t | q, u) ∩ (R 3 \ Y ) = ∅ can be easily verified, since as soon as one of the corners x or x violates the safety restrictions we can interrupt ODE 3.1 are taken from [Saoud et al., 2020]. In the following, the implementations has been done in MATLAB, Processor Intel Core i7-8700, 3.20 Hg, RAM 16 GB.

Conclusion

In this Chapter, we introduced a novel lazy synthesis algorithm for a finite transition system with a safety specification. The main idea was to iteratively explore only the boundary states of the controllable domain, supposing that internal states are safely controllable a priory. The worst-case complexity of the proposed algorithm coincides with the complexity of the classical brute-force exploration ( [Tabuada, 2009]), but our approach is more efficient in practice. Indeed, if a controllable domain for the abstract controller is non-empty, then we have a computational gain since we don't explore internal states. Moreover, real-time implementation of a closed-loop controller for the original continuous system is more memory efficient since the information for the internal states is not stored. To illustrate the benefits of the proposed approach, we considered an adaptive cruise control problem with a constant headway spacing policy.

Chapter 4

Lazy Safety Controller Synthesis with

Multiscale Adaptive-Sampling

Abstractions

As a finite abstraction for an infinite system, the symbolic model is commonly obtained by discretizing time, state, and input spaces. The smaller the sampling parameters are, the better abstractions mimic the behavior of the concrete system. Consequently, with finer symbolic models, there is more likely a solution for the abstract control problem when there is a solution for the original one. However, dealing with accurate abstractions costs a price.

First, increasing the number of states and inputs in the symbolic model increases the number of transitions to be computed. Second, the complexity of discrete synthesis algorithms essentially depends on the size of symbolic models. Third, abstraction-based controllers are implemented as look-up tables, and the memory requirements for storing them are too high when there are too many elements in the abstraction. In this Chapter, we trade-off between accuracy and efficiency and focus on approaches iteratively refining symbolic models when synthesis with coarser abstractions is failed [START_REF] Gol | Language-guided controller synthesis for linear systems[END_REF], Girard et al., 2016, Hsu et al., 2019[START_REF] Li | Rocs: A robustly complete control synthesis tool for nonlinear dynamical systems[END_REF].

To refine an abstraction, one can decrease the duration of transitions [START_REF] Gonzalez | A descent algorithm for the optimal control of constrained nonlinear switched dynamical systems[END_REF] or precise the space partitioning [START_REF] Gol | Language-guided controller synthesis for linear systems[END_REF][START_REF] Li | Rocs: A robustly complete control synthesis tool for nonlinear dynamical systems[END_REF], Nilson et al., 2017] or both [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF], Hsu et al., 2019]. In the last case, one may reduce time and state discretization parameters synchronously, supposing that the duration of transitions, which start from the initial states with the same size, coincide [START_REF] Hsu | Multi-layered abstraction-based controller synthesis for continuous-time systems[END_REF]. However, there is a common trend in the community [START_REF] Hsu | Lazy abstraction-based controller synthesis[END_REF], Girard et al., 2016, Nilson et al., 2017] to permit for the same initial state transitions with different duration in order to improve the flexibility of abstractions. Following this trend, we consider in this Chapter abstractions allowing multiple transition duration. For such abstractions, it makes sense to synthesize the maximal inputs-lazy safety controller prioritizing those transitions which are longer [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF], Nilson et al., 2017]. What is about state-space discretization let us refine abstraction locally [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF], Hsu et al., 2019, Nilson et al., 2017, Li and Liu, 2018a] since it is more efficient than global refinement [START_REF] Hsu | Multi-layered abstraction-based controller synthesis for continuous-time systems[END_REF]. Indeed, usually, one should be accurate only next to the obstacles or in the regions where the system dynamics change too fast. To react even faster to the local speed of the dynamical system, we propose to constrain the duration of the transitions by a state neighborhood that should contain the reachable set, as opposed to a predetermined duration [START_REF] Gol | Language-guided controller synthesis for linear systems[END_REF], Girard et al., 2016, Hsu et al., 2019[START_REF] Li | Rocs: A robustly complete control synthesis tool for nonlinear dynamical systems[END_REF].

Hence, we again use adaptive time sampling described in the previous Chapter. However, this Chapter uses neighborhoods of different sizes to implement the multiple time duration idea. In addition to abstraction refining, we propose to explore the symbolic model forwardly and thus restrict the controller synthesis computations to states that are reachable from the initial set only. This idea was proposed in ( [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF]), but their approach is restricted to deterministic abstractions. The algorithm presented in this Chapter applies to non-deterministic symbolic models as well.

This Chapter again provides an abstraction-based synthesis approach to solving the Problem 1.1.1. However, unlike the previous Chapter, the initial set X 0 is known, and multi-scale abstractions are considered. In section 4.1, we construct a multilayered abstraction with multi-scale adaptive time sampling. In section 4.2.1, we introduce a partial order on the input space, prioritizing transitions with longer duration. We also enrich the input space by an auxiliary input up, allowing switching from a finer level of the abstraction to a coarser one and give this input the highest priority. We then provide an efficient algorithm for computing the maximal input-state safety controller based on two ideas. To explore inputs with a lower priority only if we failed to find a safe input with higher priority and do not deal with non-reachable from initial set states. The proposed algorithm is implemented as a simple combination of Algorithm 2.3 and Algorithm 2.4. In subsection 4.2.1 we show that a multilayered and an adaptive grid are equivalent from the perspective of control synthesis purposes, but the adaptive grid is less time/memory consumpting.

Section 4.3 refines safety controller computed for the abstraction to the continuous-time safety controller, solving the Problem 1.1.1. In section 4.4, we illustrate the benefits of the proposed approach synthesizing a safety controller maintaining the temperature on the building in a comfortable range for a person.

Multilayered Abstractions with Multi-scale Adaptive-Time Sampling

In Problem 1.1.1, we aim to synthesize a controller for a continuous-time control system

Σ f = (T , R nx , U, W, f )
that maintains all closed-loop trajectories starting in the initial set X 0 ⊂ Y within a safety set Y ⊂ R nx . Let us also remind that the dynamic of Σ f = (T , R nx , U, W, f ) is given by eq.(1.1):

ẋ(t) = f (x(t), u(t), w(t)), t ∈ T , u(t) ∈ U ⊂ R nu , w(t) ∈ W ⊂ R nw ,
where U, W are compact sets. Let us suppose for this Chapter that the set Y is a compact as well. To solve the Problem 1.1.1 we use abstraction-based synthesis techniques, and this section is devoted to multilayered abstraction with multi-scale time sampling for continuous dynamical systems. We first abstract the state space of the concrete system with several uniform Cartesian partitions embedded one into another. Then for every abstract state, we allow the same abstract controllers. To define a transition relation, we use adaptive time sampling techniques introduced in the previous chapter: the duration of the transitions is constrained by state intervals that should contain the reachable set.

Let us start the construction of a symbolic model for the original plant

Σ f = (T, R nx , U, W, f ) by discretizing the state space R nx . Let X = [x,
x) be an n-dimensional interval including a safe set Y . Given a number L > 0, and a state space sampling parameter m x > 0, m x ∈ N nx we introduce for every l = 1, . . . , L a uniform partition

Q l = {q ∈ 2 X | ∃z ∈ Z n s.t. q = [x + z * η l , x + (z + 1) * η l )} (4.1)
where η l = (x -x)/(2 l-1 m x ) and we associate every state x ∈ X with a unique cell q ∈ Q l such that x ∈ q. We also define for every q ∈ Q l , the center of the interval q c = x + (z + 1 2 ) * η l . Depending on the context, we regard an element q ∈ Q l either as an atomic symbol, representing an infinite number of states from X, or as a subset of X.

It is obvious from the definition that for any q i , q j ∈ Q l , q i = q j the intersection q i ∩ q j = ∅ and that X = ∪ q∈Q l q. Lemma 4.1.1. For any l = {1, . . . , L -1} and for any q ∈ Q l there exists a unique set a states

{q i } 2 n i=1 , q i ∈ Q l+1 such that q = ∪ 2 n i=1 q i .
Regarding the safety specification, an element q ∈ Q l is a safe state if and only if q ⊆ Y , an initial state if and only if q ∩ X 0 = ∅. Let us denote by Q l,S a set of all safe states in Q l , and by Q l,init a set of all initial states. We then combine all these partitions into a multilayered grid Q = ∪ L l=1 Q l and use it as a set of states for the multilayered abstraction. Obviously, the layer Q 1 is the coarsest layer of Q and Q L is the finest one (see eq. (4.1)). From Lemma 4.1.1 it also follows that the partitionings Q 1 , . . . , Q L are embedded one into another.

In the next step, a control set U is approximated by its finite subset U µ ⊆ U. For every q ∈ Q l , u µ ∈ U µ we consider the set of all reachable states at the time t ∈ T :

Reach(t | q, u µ ) = {x ∈ R nx | ∃ x(0) ∈ q and ∃ w ∈ L ∞ ([0, t], W) such that x f (t | x(0), u, w) = x},
corresponding to an initial set q, a constant control function u : [0, t] → u µ and all admissible disturbances w . Since the exact computation of reach set is rarely possible, an over-approximation Reach(t | q, u µ ) is commonly used to built symbolic models. Let us remark that we use the same inputs for all states for simplicity, and extension towards the case when for every state q ∈ Q l its proper set of abstract inputs U µ (q) is defined is always possible.

In this Chapter, a symbolic model with multi-scale time sampling is considered, which means that for every given state q ∈ Q and control u µ ∈ U µ we construct n p transitions with different duration. Let us also introduce an input up, which allows switching from the current layer to the previous (coarser) one and define a function l : Q → {1, . . . , L} returning for any q ∈ Q the index of the layer to which q belongs. We now ready to define a transition relation F for every available input in the set U = (U µ × {1, . . . , n p }) ∪ {up}.

• for any q ∈ Q \ Q 1 the transition (q , up, q) ∈ F if and only if q ∈ Q l(q)-1 and q ⊂ q. See Fig. 4.1 (left).

• for any q ∈ Q and any (u µ , j) ∈ U µ × {1, . . . , n p } the transition (q, (u µ , j), q ) ∈ F if and only if

q ∈ Q L , q ∩ Reach(τ uµ,j q | q, u µ ) = ∅, (4.2)
and the condition of a collision avoidance

Reach(t | q, u µ ) ∩ (X \ Y ) = ∅, t ∈ [0, τ uµ,j q ] (4.3)
is satisfied. Here τ uµ,j q = min(τ l , τ uµ,j q -ε), where τ l is a given parameter which determines the maximal evolution time allowed at this layer, while τ uµ,j q is a moment in time given by

τ uµ,j q = inf t∈[0,+∞) Reach(t | q, u µ ) ⊂ q c -(j + 1/2) * η l , q c + (j + 1/2) * η l (4.4)
when the over-approximation of a reachable set leaves the interval with a radius (j + 1/2)η l and a center in q c . We chose ε < τ uµ,j q arbitrary small to stop evolution just before leaving, while τ l should be big enough since it serves only to manage situations where a solution is stuck within the box. In the Fig. 4.1 there is illustration of the idea.

Such a definition of a transition duration using adaptive time-sampling is a contribution of this manuscript. Instead of using prescribed time sampling parameters ( [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF], [START_REF] Hsu | Lazy abstraction-based controller synthesis[END_REF]), this approach allows us to control, approximately, where symbolic transitions finish and better analyze the behavior of the system. At the same time, the collision avoidance condition enables to eliminate solutions, which start and end in the safe set but passes some unsafe regions during the evolution. However, since the intersection of the reachable set with the grid is checked at every instant of time, the authors recommend using simple interval over-approximations [START_REF] Meyer | Interval Reachability Analysis.Bounding Trajectories of Uncertain Systems with Boxes for Control and Verification[END_REF]), trading accuracy for simplicity of implementation. We also finish any non-up transition at the finest layer to be more flexible while moving close to the obstacles.

Hence, in this section, we constructed a multilayered and multi-scale symbolic model Σ = (Q, U, F ) which mimics the dynamic of the original system. In the next section, we will synthesize safety controller for the abstraction, while supposing that specification is given by the safe set Q S = ∪ L l=1 Q l,S and the initial set

Q init = Q L,init is also known.
restricted to the class of deterministic transition systems. Algorithm 4.2 provided below overcomes this limitation.

Algorithm 4.1: ClassicalSynthesisMSC(Σ, Q S )

Input: Σ = (Q, U, F ) and a safe set QS Output: Maximal Safety Controller C 1 begin 2 for q ∈ QS do 3 p(q) := 1;

4 for q ∈ Q \ QS do 5 p(q) := 0; 6 repeat 7 QE := {q ∈ Q | p(q) = 0}; 8 B := BlockF p (QE); 9 for q ∈ B do 10 p(q) := p(q) -1; 11 until B = ∅; 12 for q ∈ Q E do 13 C(q) := EnabF p (q); 14 for q ∈ Q \ QE do 15 C(q) := ∅; 16 return C; Algorithm 4.2: MLSC(Σ, Q S , Q init ) Input: Σ = (Q, U, F ), a safe set QS, an initial set Qinit Output: MSLS controller C. 1 begin 2 for q ∈ QS do 3 p(q) := N ; 4 for q ∈ Q \ QS do 5 p(q) := 0; 6 repeat 7 Q R E := ReachF p, U ({q ∈ Qinit | p(q) = 0}) ; 8 B := BlockF p, U (Q R E ); 9 for q ∈ B do 10 p(q) := p(q) -1; 11 until B = ∅; 12 for q ∈ Q R E do 13 C(q) := EnabF p, U (q); 14 for q ∈ Q \ Q R E do 15 C(q) := ∅; 16 return C;
Theorem 4.2.1. For a given transition system Σ = (Q, U, F ), a safe set Q S and an initial set Q I , let C * be a controller computed by Algorithm 4.2. Then, C * is a safety controller, satisfying the following properties:

1. Q init ∩ Cont(Σ, Q S ) ⊆ Dom(C * ); 2. Dom(C * ) ⊆ Reach F C * (Q init ∩ Dom(C * ));
3. for all states q ∈ Dom(C * ):

(a) if u ∈ C * (q) then for all u ∈ Enab F (q) such that u u, it holds that u ∈ C * (q) if and only if

F (q, u ) ⊆ Cont(Σ, Q S ); (b) if u ∈ C * (q), then for all u ∈ Enab F (q) with u ≺ u , it holds that F (q, u ) ∩ Cont(Σ, Q S ) = F (q, u ).
Proof. Indeed, Algorithm 4.2 is a simple merge of Algorithm 2.3 and Algorithm 2.4. Consequently, the controller synthesised by Algorithm 4.2 inherits properties from MILS and MSLS controllers.

Similar to Figures 2.3 and 2.4 from Chapter 2, Figure 4.2 illustrates the execution of Algorithm 4.2 for a simple transition system: the input set U consist of 4 actions and inputs u 1 , u 2 are more prioritised than u 3 , u 4 , while the initial set is given by Q init = {q 1 , q 2 , q 3 , q 4 }. However, let us highlight the difference between the classical synthesis approach (Algorithm 4.1) and lazy synthesis approach (Algorithm 4.2) while dealing with multilayered and multi-scale symbolic model Σ = (Q, U, F ). So, Algorithm 4.1 coincides with Algorithm 2.1 and hence it returns the maximal safety controller. The function p : Q → {0, 1} indicates whether a state q ∈ Q is controllable (p(q) = 1) or not (p(q) = 0) and the reduced transition relation F p is defined as follows: (q, u, q ) ∈ F p if and only if p(q) = 0 and for all

F A p q 1,n1 u2 --→ F A p . . . . . . um --→ F A p q m,nm = q such that q 0,n0 ∈ Q p up ({q ∈ Q init | p(q) = 0}
) and q j,nj ∈ Q A p for all j = 0, . . . , m. The last is equivalent to the fact

q ∈ Q A,R E .
Proposition 4.2.2. Let us run Algorithm 4.2 for the transition system Σ = (Q, U, F ). Then at every iteration of loop 6-11 the following

Block F p, U (Q R E ) = Block F A p (Q A,R E ) is satisfied. Proof. So, q ∈ Block F p, U (Q R E ) if and only if q ∈ Q R E and F p, U (q, u) = ∅ for any u ∈ U , which is equivalent to q ∈ Q A,R E and Q p up (F p, U (q, u)) = ∅ for any u ∈ U . The last is true if and only if q ∈ Block F A p (Q A,R E ).
So, we can reinitialize the priority of states p (line 11), using only knowledge about Q A p and F A p . Now we explain how to update the adaptive grid Q A p and a transition relation F A p , while changing p during the evolution of Algorithm 4.2.

After execution of lines 2-5, a state in Q is reachable from the finest layer if and only if it is safe or belonging to Q L . Hence, if we start from the coarsest layer Q 1 and recursively split all unsafe states into 2 n pieces until they do not belong to the finest layer Q L , we finally get a grid Q A p , corresponding to the distribution of priority of states p just before the loop 6-11 execution. Since with every iteration of the loop only states included in Q A p change their priorities (see Proposition 4.2.2), we can also update our adaptive grid Q A p without direct usage of the transition relation F p, U . Indeed, if a state q ∈ Q \ Q L gets a priority 0, then, from Lemma 4.1.1 and definition of up transition, it follows that we should replace it by

2 n states q i ∈ Q l(q)+1 , such that q = ∪ 2 n i=1 q i .
There also exists a way to compute the transition relation F A p , using only the current version of Q A p .

Proposition 4.2.3. For any q ∈ Q A p , u ∈ U \ {up} a state q ∈ Q A p belongs to a set F A p (q, u) if and only if the intersection q ∩ Reach(τ uµ,j q

| q, u µ ) = ∅, and the condition of a collision avoidance

Reach(t | q, u µ ) ∩ (X \ Y ) = ∅ is satisfied for all t ∈ [0, τ uµ,j q ].
Proof. Let q ∈ F A p (q, u). From the definition of F A p , this is true if and only if q ∈ Q p up (F p, U (q, u)). From the definition of Q p up last is equivalent to existence q ∈ Q L such that q ∈ Q p up (q ) and q ∈ F p, U (q, u). This is satisfied if and First of all we introduce a controller C dur * : Q * → U µ ×T, such that for every q ∈ Q * \Dom(C * ) we say C dur * (q) = ∅, while if q ∈ Dom(C * ) and (u µ , j) ∈ Enab F * (q), then the pair (u µ , τ uµ,j q

t e T 1 T 2 t h 2 t h 1 α β 1 β 2 γ 1 γ 2
) ∈ C dur * (q). Hence, a controller C dur * store real durations of safe transitions, instead of the sizes of the boxes. Now we are ready to refine the controller C dur * to a safety controller u for the original continuous system. Let us consider the control input given for all t ∈ [t k , t k+1 ) by

u(t, x) = u k where (u k , τ k ) ∈ C dur * (Q x (x(t k ))) (4.5)
and the sequence of instants {t k } is given by t 0 = 0 and t k+1 = t k + τ k (4.6)

Theorem 4.3.1. For a given control system Σ f = (T , R nx , U, W, f ) all trajectories of closed-loop system (1.1),(4.5), and (4.6) starting from a Dom(C) at t = 0 stays within the set S ⊆ Y for all t ∈ T no matter which disturbance w ∈ L(T , W) has been applied.

The statement of the theorem directly follows from the discussion above. We only remark here that the computation of the controller for the abstraction is usually implemented off-line and then stored in a control device memory, while a controller for the continuous system is calculated online using this pre-computed information.

Numerical Illustration: Temperature Regulation in the Building

This section we consider a problem of temperature regulation in two rooms building [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF]. Let each room is equipped with a heater and let T i is a temperature in the room i, i = 1, 2. The evolution of the temperatures could be described by the following system of the differential equations

Ṫ1 = α(T 2 -T 1 ) + β 1 (t e -T 1 ) + γ 1 (t h1 -T 1 )u 1 Ṫ2 = α(T 1 -T 2 ) + β 2 (t e -T 2 ) + γ 2 (t h2 -T 2 )u 2 (4.7)
Here t e is temperature of external environment of the building, t h1 , t h2 are temperatures of the heaters, α is the conduction factor between rooms, β 1 , β 2 are conduction factors between external environment and the first room and the second room correspondingly, γ 1 , γ 2 are conduction factor between heater and rooms. We illustrate the considered configuration in the Figure 4.4. Control parameter u i equals 1 if the room i is heated and 0 otherwise.

Temperature t e is considered as a bounded disturbance.

We run our simulation for the following set of parameters

α = 1/2 * 10 -4 W/J, β 1 = 1/6 * 10 -4 W/J, β 2 = 1/11 * 10 -4 W/J, γ 1 = 1.5 * 10 -4 W/J, γ 2 = 1.5 * 10 -4 W/J, t h1 = 30 C • , t h1 = 40 C • .
A safety specification were given by an initial set X To construct the over-approximations of reachable states we benefit from the fact the system (4.7) is monotone, and, hence, for any given state q = [x q , x q ], any given constant control function u : [0, t] → (u 1 , u 2 ), (u 1 , u 2 ) ∈ U µ the reachable set robust to any admissible disturbances Reach(t |

q, u) ⊆ [x f (t | x q , u, t min e ), x f (t | x q , u, t max e )], where x f (t | x q , u, t min e ), x f (t | x q , u, t max e
) are trajectories of the system (4.7), corresponding to initial values x q , x q , control function u, and constant disturbances t min In Figure 4.5 the results of simulation are provident. We use a dark grey and a light grey for states, which are controllable with a (u µ , 1), u µ ∈ U µ and with a (u µ , 2), u µ ∈ U µ correspondingly, while white region is uncontrollable.

The closed loop trajectory were simulate for 24 hours, supposing that external temperature is varying between 4.1, where the controllability ratio is a capacity ratio Dom(C * ) to Q S . The controllable sets coincides for the adaptive grid and the finest grid, but we get a noticeable time and memory gain. The implementations has been done in C++, processor

Intel Core i7-8700, 2.5 Hg, RAM 16 GB.

Conclusion

In this Chapter, we present an abstraction-based approach to safety controller synthesis for continuous-time nonlinear systems. To reduce the computational burden associated with symbolic control approaches, we develop a lazy controller synthesis algorithm, which uses the incremental forward exploration of the symbolic dynamics and thus allows us to restrict the controller synthesis computations to reachable states only. We propose to use this algorithm with a novel type of multilayered, multi-scale abstractions, which use adaptive sampling of time. Instead of using transitions of predetermined duration, the duration of the transitions is constrained by state intervals that must contain the reachable set, thus enabling a better control of the symbolic transitions. We also prioritize transitions with longer duration and explore lower priority actions only if we can guarantee safety using a higher priority inputs.

In simple words, the proposed lazy algorithm is an alternation procedure between a forward exploration of state space and a backward correction of the obtained transition system in order to satisfy the safety requirements. At the beginning of every iteration, we update for every state a set of enabled inputs. The set of enabled actions depends on the priority of the state. Then we try to find a safety controller. If a state is uncontrollable we either reduce duration of enabled transitions or split a state in several pieces. And then start exploration again. We provide a simple example to illustrate the benefits of the approach.

closed) sets or their intersection. Our choice is inspired by the paper [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF], where efficient sparse abstractions are proposed for monotone dynamical systems and directed specifications. Going one step further, we benefit from a particular structure and synthesize the maximal safety controller lazily.

In spirit, the closest works in the literature is [START_REF] Sadraddini | Safety control of monotone systems with bounded uncertainties[END_REF]. In [START_REF] Sadraddini | Safety control of monotone systems with bounded uncertainties[END_REF], the authors introduce a notion of s-sequence to characterize a controlled invariant of the system. This notion is relatively close to the notion of basis, which we use to represent directed sets in our work. However, looking at the computation of controlled invariants as an optimization problem [START_REF] Sadraddini | Safety control of monotone systems with bounded uncertainties[END_REF] does not guarantee the maximality of the obtained control invariant set. They also propose to use a simple open-loop control policy to keep a trajectory within a safe set. Although such an approach is memory efficient, it is hardly possible to use their controller as a start point for more general tasks (for example, obstacle-avoided reachability specification [START_REF] Reissig | Feedback refinement relations for the synthesis of symbolic controllers[END_REF] or optimal control problems with hard constraints).

The Chapter is organized as follows. Section 5.1 introduces input-state and state monotone dynamical systems.

It also provides an illustrative example emphasizing the difference between these two classes of systems. We then adapt results from [START_REF] Angeli | Monotone control systems[END_REF] to characterize the considered objects. Subsection 5.1 is devoted to directed safety specifications. Section 5.2 defines lower and upper (input-)state monotone transition systems, provides a tool for their characterization, and determines the procedure, preserving the monotonicity property of the original plant while creating a symbolic abstraction. Section 5.3 presents lazy algorithms to compute the maximal safety controller for monotone transition systems and directed safety specification and their intersection.

Monotone Dynamical Systems and Directed Safety Specifications

In this section, we consider monotone control systems with disturbances [START_REF] Meyer | Compositional abstraction and safety synthesis using overlapping symbolic models[END_REF], but in contrast to the existing terminology, we distinguish the systems whose trajectories preserve a partial order on the state-space from those that also preserve the monotonicity of the input space. We adapt the results [START_REF] Angeli | Monotone control systems[END_REF] to provide criteria for a dynamical system to be state monotone or input-state monotone and illustrate the gap between these two classes of systems with a simple example. We then follow the paper [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF] and focus on directed safety specifications.

Input-State and State Monotone Dynamical Systems and Their Characterization

Let us start with introducing the notions of state monotone and input-state monotone dynamical systems and with Figure 5.1 illustrating the given definitions.

Definition 5.1.1. Let S be a compact subset of a state space R s and let S be equipped with a partial order S .

Then for two functions s, s ∈ L ∞ (T , S) we say, that s S,T s if the following holds s(t) S s (t) for all t ∈ T .

u, w Definition 5.1.2. Consider a control system Σ f = (T , R nx , U, W, f ), where R nx and W are equipped with partial orders R nx and W correspondingly. The system Σ = (T , R nx , U, W, f ) is said to be state monotone (SM) with respect to the partial orderings R nx , W if for all x 0 , x 0 ∈ R nx , for all u ∈ L ∞ (T , U) and for all w, w ∈ L ∞ (T , W)

u ′ u w w ′ t x ′ 0 x 0 x f (t | x ′ 0 , u ′ , w ′ ) x f (t | x 0 , u, w) ⇒ Y =↓ Y
the following implication holds x 0 R nx x 0 , w W,T w ⇒ x f (t, x 0 , u, w) R nx x f (t, x 0 , u, w ), t ∈ T .

Definition 5.1.3. Consider a control system Σ f = (T , R nx , U, W, f ), where R nx , U, and W are equipped with partial orders R nx , U and W correspondingly. The system Σ = (T , R nx , U, W, f ) is input-state monotone (ISM) with respect to the partial orderings R nx , U , and W if for all x 0 , x 0 ∈ R nx , u, u ∈ L ∞ (T , U), and w, w ∈ L ∞ (T , W)

such that x 0 R nx x 0 , u U ,T u , and w W,T w the following holds x f (t, x 0 , u, w) R nx x f (t, x 0 , u, w ), t ∈ T .

It follows straightforwardly from the definitions above that any ISM control system is a SM control system. Moreover, any SM system can be seen as ISM, with a partial order defined as u U u ⇔ u = u . However, this trivial order does not have any practical interest, and while speaking about ISM transition systems, we assume that there are at least two elements in u, u ∈ U, such that u ≺ U u .

In this manuscript, we focus on a subclass of (input-)state monotone systems, which is called (input-) state cooperative systems. Similar to definitions in [START_REF] Angeli | Monotone control systems[END_REF] we say that an (input-)state monotone system

Σ = (T , R nx , U, W, f ) is a (input-)state cooperative system if partial orders on R nx , U ⊆ R nu , W ⊆ R nw are induced
by the positive orthants R nx + , R nu + , R nw + correspondingly. Then, adapting the Kamke-Müller condition [Kamke, 1932] we characterize (input-) state cooperative systems, as follows.

Theorem 5.1.1. The system Σ f = (T , R nx , U, W, f ) with locally Lipschitz vector field f is input-state cooperative if and only if for all i = 1, . . . , n x for all x R nx x, such that x i = x i , for all u U u , w W w the following inequality is satisfied f i (x, u, w) ≤ f i (x , u , w ), where partial orders R nx , U , W are induced by R nx + , R nu + , R nw + correspondingly.

Corollary 5.1.1. The system Σ = (T , R nx , U, W, f ) with locally Lipschitz vector field f is state cooperative if and only if for all i = 1, . . . , n x for all x R nx x, such that x i = x i , for all u ∈ U and for all w W w the following inequality is satisfied f i (x, u, w) ≤ f i (x , u, w ), where partial orders R nx , W are induced by R nx + , R nw + correspondingly.

We are now ready to provide an example illustrating the difference between SM and ISM systems.

Example 5.1.1. Let us consider a control system Σ f = (T , R 2 , U, W, f ), where U = {1, 2} and W = ∅. Hence, there is no disturbance in the system's dynamic ẋ = f (x, u), where f (x, u) defined as follows

f (x, u) =      A 1 x if u = 1 A 2 x if u = 2
where

A 1 =    0.1 0.9 3 0.7    and A 2 =    0.2 2 0.1 0.7   
Using the Corollary 5.1.1 we can conclude that the transition system presented above is state cooperative, while it is not input-state cooperative for any non-trivial partial order on U .

Another well-known in the literature criterion is formulated in terms of partial derivatives of the vector field.

Theorem 5.1.2. The system Σ = (T , R nx , U, W, f ) with continuously differentiable vector field f is input-state cooperative if and only if for all x ∈ R nx , u ∈ U, w ∈ W, for all i, j = 1, . . . , n x , j = i, k = 1 . . . n u , l = 1 . . . n w the following inequalities are satisfied

∂f i ∂x j (x, u, w) ≥ 0, ∂f i ∂u k (x, u, w) ≥ 0, ∂f i ∂w l (x, u, w) ≥ 0.
Corollary 5.1.2. The system Σ = (T , R nx , U, W, f ) with continuously differentiable vector field f is input-state cooperative if and only if for all x ∈ R nx , w ∈ W, for all i, j = 1, . . . , n x , j = i, l = 1 . . . n w the following inequalities are satisfied ∂f i ∂x j (x, u, w) ≥ 0, ∂f i ∂w l (x, u, w) ≥ 0.

Directed Safety Specifications

In this section, we introduce the notion of directed safety specifications, i.e., specifications determined by lowerclosed or upper-closed sets. Proposition 5.1.1 ( [Reddy, 1995]). Let L be a partially ordered set, A i ⊆ L be finite subsets satisfying

A i =↓ A i for all i ∈ {1, . . . , p}, p ∈ N 1 . Then ↓ (∪ p i=1 A i ) = ∪ p i=1 A i and ↓ (∩ p i=1 A i ) = ∩ p i=1 A i . Analogously, let A i ⊆ L be finite subsets satisfying A i =↑ A i for all i ∈ {1, . . . , p}, p ∈ N 1 . Then ↑ (∪ p i=1 A i ) = ∪ p i=1 A i and ↑ (∩ p i=1 A i ) = ∩ p i=1 A i .
Figure 5.3: The first two partitions satisfy Assumption 5.2.1, while the third partition does not satisfy Assumption 5.2.1. The first and third partitions satisfy Assumption 5.2.2, while the second partition does not satisfy Assumption 5.2.2. The state-space is equipped with the component-wise partial order defined on R 2 .

Assumption 5.2.2. Let for all q, q ∈ Q if there exists (x, x ) ∈ q × q satisfying x R nx x , then

x q 1 R nx x q 1 .
Intuitively, Assumption 5.2.1 (respectively, Assumption 5.2.2) reflects the fact that the partitioning should preserve the lower (respectively, upper) monotonicity property from continuous to symbolic states. Fig. 5.3 shows examples of partitions satisfying Assumptions 5.2.1 and 5.2.2. Keeping in mind Assumptions 5.2.1 and 5.2.2, let us define a partial order on the abstract set of states Q as follows:

• If Assumption 5.2.1 is satisfied, then for all q 1 , q 2 ∈ Q, q 1 Q q 2 if and only if x q1 2 R nx x q2 2 ;

• If Assumption 5.2.2 is satisfied, then for all q 1 , q 2 ∈ Q, q 1 Q q 2 if and only if x q1 1 R nx x q2 1 ;

• If both Assumptions 5.2.1 and 5.2.2 are satisfied, then for all q 1 , q 2 ∈ Q, q 1 Q q 2 if and only if

x q1 1 R nx x q2 1 and x q1 2 R nx x q2 2 .
In the following result, we show that, under Assumptions 5.2.1 and 5.2.2, monotonicity of the original system

Σ f = (T , R nx , U, W, f
) is preserved when constructing its symbolic box abstraction Σ B = (Q, U, F ).

Proposition 5.2.1. Let us consider control system

Σ f = (T , R nx , U, W, f ). If Σ f = (T , R nx , U, W, f
) is an input state cooperative system and if its symbolic box abstraction Σ B = (Q, U, F ) satisfies Assumption 5.2.1, (respectively, Assumption 5.2.2), then Σ B = (Q, U, F ) is a LISM (respectively, UISM) transition system. Moreover, when both Assumptions 5.2.1 and 5.2.2 are satisfied, then Σ B = (Q, U, F ) is an ISM transition system Proof. We only provide a proof for the case of LISM, the cases of UISM and ISM can be derived similarly. We should prove that for all q 1 , q 2 ∈ Q and for all u 1 , u 2 ∈ U, if q 1 Q q 2 and u 1 U u 2 , the following is satisfied: for all q 1 ∈ F (q 1 , u 1 ) there is q 2 ∈ F (q 2 , u 2 ), such that q 1 Q q 2 . Let q 1 , q 2 ∈ Q and u 1 , u 2 ∈ U, such that q 1 Q q 2 and u 1 U u 2 . Under Assumption 5.2.1, the last is equivalent to

x q1 2 R n x x q2 2 and u 1 U u 2 . Let q 1 ∈ F (q 1 , u 1 ), from the monotonicity of Σ f = (T , R nx , U, W, f ) and the construction of Σ B = (Q, U, F ), we have the existence of m ∈ {1, . . . , M } such that x f (τ | x q1 2 , u 1 , w m 2 ) ∈ q 1 . Let q 2 ∈ Q is such that x f (τ | x q2 2 , u 2 , w m 2 ) ∈ q 2 . Then q 2 ∈ F (q 2 , u 2 ).
Here functions u 1 , u 2 , w m 1 , w m 2 are constant functions with values w m 1 , w m 2 correspondingly Moreover, there are

x = x f (τ | x q1 2 , u 1 , w m 2 ) and x = x f (τ | x q2 2 , u 2 , w m
2 ), such that x ∈ q 1 , x ∈ q 2 and since Σ f = (T , R nx , U, W, f ) is an input-state monotone control system, one has x R nx x. Hence, from Assumption 5.2.1,

x q 1 2 R nx x q 2
2 . The last is equivalent to

q 1 Q q 2 . q x q 2 x q 1 x f (τ | x q 2 , u, w m 2 )
x f (τ | x q 1 , u, w m 1 ) q We then have the following corollary for SM systems.

Corollary 5.2.2. Let us consider control system

Σ f = (T , R nx , U, W, f ). If Σ f = (T , R nx , U, W, f ) is a state
cooperative system and if its symbolic box abstraction Σ B = (Q, U, F ) satisfies Assumption 5.2.1, (respectively, Assumption 5.2.2), then Σ B = (Q, U, F ) is a LSM (respectively, USM) transition system. Moreover, when both Assumptions 5.2.1 and 5.2.2 are satisfied, then Σ B = (Q, U, F ) is an ISM transition system Hence, the monotonicity property is preserved when going from the original system to its symbolic abstraction.

As soon as Assumption 5.2.1 or Assumption 5.2.2) or both is satisfied. Moreover, if the Q S is lower-closed (upperclosed) with respect two the partial order R nx , and Assumption 5.2.1 (respectively, Assumption 5.2.2) holds, then the set Q S is lower (respectively, upper) closed with respect to the partial order Q S . Here again, we look at the set Q S either as a subset of R nx , or as a collection of abstracts states. Let us remark that Q S can be lower-closed with respect two the partial order R nx and be finite only if there is q ∈ Q S such that q = (-∞, x q 2 ).

Sparse Abstractions for (Input-)State Monotone Control Systems

In this section we introduce sparse abstractions for Σ f = (T , R nx , U, W, f ). We then show that when we are dealing with directed specifications, sparse abstractions are equivalent to box abstraction Σ B = (Q, U, F ) from the perspectives of synthesis. However, sparse abstractions are more efficient since they are less non-deterministic. To define a sparse abstraction, let us introduce the operators max and min for a finite partially ordered set.

Definition 5.2.3. Let L be a partially ordered set and A ⊆ L is a finite subset. The set of minimal elements of A is defined as min(A) = {q ∈ A | ∀q 1 ∈ A, q L q 1 or (q, q 1 ) ∈ Inc L }. Similarly, the set of maximal elements of A is defined as max(A) = {q ∈ A | ∀q 1 ∈ A, q L q 1 or (q, q 1 ) ∈ Inc L }.

For a control (input-)state monotone control system Σ f = (T , R nx , U, W, f ) an upper-sparse abstraction is defined as Σ U S = (Q, U, F U S ) where sets Q, U are inherited from Σ B = (Q, U, F ) and the transition relation is defined for q ∈ Q S , u ∈ U as F U S (q, u) = max(F (q, u)). Right sub-figure of Figure 5.4 illustrates the difference of an upper sparse abstraction Σ U S = (Q, U, F U S ) and box abstraction Σ B = (Q, U, F ). While for a state q the set of successors F (q, u) include all grey boxes, the set F U S (q, u) consist of two blue ones. Hence the abstraction

Σ U S = (Q, U, F U S ) is less non-deterministic than Σ B = (Q, U, F ).
Similarly, a lower-sparse abstraction is defined as

Σ LS (Σ) = (Q, U, F LS )
where Q, U are inherited from Σ B (Σ) and the transition relation is defined for q ∈ Q, u ∈ U as F U S (q, u) = min(F (q, u)).

Remark 5.2.2. Let us remark that the transition relation of the upper sparse abstraction Σ U S = (Q, U, F U S ) can be equivalently defined as follows: for all q ∈ Q S , u ∈ U , q ∈ F U S if and only q ∈ max(∪ M m=1 q m ), where q m is such that

x f (τ | x q 2 , u, w m
2 ) ∈ q m (see Figure 5.4 for an illustration).

Although our definition of upper-sparse abstraction is slightly different from one proposed in [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF],

the transition system Σ U S = (Q, U, F U S ) is still related to Σ B = (Q, U, F ) with an upper alternating simulation relation [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF].

We first show how to preserve the monotonicity when constructing upper or lower-sparse abstractions.

Proposition 5.2.2. Let the box abstraction

Σ B = (Q, U, F ) of the control system Σ f = (T , R nx , U, W, f ) be LISM, then its upper-sparse abstraction Σ U S = (Q, U, F U S ) is also LISM. Similarly, let the box abstraction Σ B = (Q, U, F ) of the discrete-time control system Σ f = (T , R nx , U, W, f ) is UISM, then its lower-sparse abstraction Σ U S = (Q, U, F U S
) is also UISM.

Proof. We only provide a proof for the case of LISM, the case of UISM can be derived similarly. Consider q 1 , q 2 ∈ Q, u 1 , u 2 ∈ U such that q 1 Q q 2 , u 1 U u 2 and let q 1 ∈ F U S (q 1 , u 1 ) = max(F (q 1 , u 1 )), then q 1 ∈ F (q 1 , u 1 ). From Proposition 5.2.1, Σ B = (Q, U, F ) is input-state monotone, then there exists q 2 ∈ F (q 2 , u 2 ) such that q 1 Q q 2 .

Coupling the last with the fact that there exists q 2 ∈ max(F (q 2 , u 2 )) such that q 2 Q q 2 (see Definition 5.2.3), we finally get that Σ U S = (Q, U, F U S ) is ISM.

We then have the following corollary for SM systems. (input-)state monotone and the safe set is lower-closed, one can compute the maximal safety controller lazily.

Analogous results hold for upper (input-)state monotone transition systems with upper-closed specifications, but we leave them unproven, taking into account to the similarity of the statements.

Lazy Synthesis for State Monotone Transition Systems

In this section, we aim to synthesize the maximal safety controller C for a LSM transition system Σ = (Q, U, F ) and a lower-closed safety specifications Q S ⊆ Q. Looking for a lazy approach, we split the synthesis procedure into two steps. First, benefiting from the ordered structure of the state space, we efficiently compute the domain of the maximal safety controller. And then, we calculate the controller itself using the notion of u-predecessor of a set. Unlike the classical synthesis, where one explores all the states in Q S and all the inputs U , in our approach, all inputs are explored, but not necessarily all the states.

Domain of Maximal Safety Controller

Let us start with a characterization of the domain of the maximal safety controller for LSM transition systems and lower-closed safety specifications.

Lemma 5.3.1. Let us run Algorithm 5.1 for a LSM transition system Σ = (Q, U, F ) and lower-closed safety specification Q S ⊆ Q, then at every iteration of loop 6-11 the set Q E is lower-closed.

Proof. Indeed, at the first iteration the set Q E coincides with Q S and, consequently, is lower closed. Assuming that the set Q i E is lower closed let us show that the set Q i+1 E is lower-closed as well (here

Q i E is a set Q E at ith iteration of the loop 6-11). Since set Q i+1 E always included in its lower closure we only need to show that ↓ Q i+1 E ⊆ Q i+1 E . Suppose the opposite. Let there is q ∈↓ Q i+1 E such that q / ∈ Q i+1 E .
On the one hand, since q ∈↓ Q i+1 E there exists q ∈ Q i+1 E such that q ∈↓ q . From lines 6-11 of Algorithm 5.1 we have that

Q i+1 E = Q i E \ Block F i p (Q i E ). Consequently, q ∈ Q i+1 E is equivalent to q ∈ Q i E and q / ∈ Block F i p (Q i E ).
for q ∈ Q S do 3 p(q) := 1; 4 for q ∈ Q \ Q S do 5 p(q) := 0; 6 repeat 7 Q EB := {q ∈ Q | p(q) = 0 and I EB (q) = 1}; 8 B := Block Fp (Q EB ); 9 for q ∈ B do 10 p(q) := p(q) -1; 11 until B = ∅; 12 return {q ∈ Q | p(q) = 0};
latter is true if and only if p i (q ) = 1 and there is u ∈ U, such that F (q , u) = ∅ and for all q ∈ F (q , u) the following hold p(q ) = 1, i.e. in other words, F (q , u)

⊆ Q i E . On the other hand, q / ∈ Q i+1 E if and only if either p i (q) = 0 or p i (q) = 1, but q ∈ Block F i p (Q i E ). Let p i (q) = 0 then q / ∈ Q i E
, the same time q ∈↓ q and we have shown that q ∈ Q i E . Thus, we got a contradiction to the fact that

Q i E is lower closed. Let p i (q) = 1 and q ∈ Block F i p (Q i E )
. However, it also can not be true, since there is u ∈ U such that F (q , u) = ∅, q Q q and Σ = (Q, U, F ) is lower state monotone the set F (q, u) is also non empty, moreover from Corollary 5.2.1 we have F (q, u) ⊆↓ F (q , u) ⊆ Q i E .

Corollary 5.3.1. The domain of the maximal safety controller for a LSM transition system Σ = (Q, U, F ) and lowerclosed safety specification Q S ⊆ Q is a lower-closed set.

So, at every iteration of loop 6-11, the set Q E is lower-closed, and from the first sight, Bas(Q E ) is a nice candidate for being the essential basis of the set Q E (see Definition 2.3.1), but it is not. Indeed, we only can guarantee that if for all q ∈ Bas(Q E ) there exits u ∈ U such that F (q, u) ⊆ Q E then for all q ∈ Q E there exits u ∈ U such that

F (q, u) ⊆ Q E .
I EB (q) =      0 if q ∈ Bas(Q E ) 1 if q ∈ Bas(Q E )
where

Q E = {q ∈ Q | p(q) = 0} (5.3)
Then Algorithm 5.3 returns the domain of the maximal safety controller.

q 1 q 2 F (q 2 , u 1 )

F (q 2 , u 2 ) F (q 1 , u 2 ) F (q 1 , u 1 ) q 1 F (q 3 , u 2 ) F (q 3 , u 1 ) F (q 1 , u 2 ) F (q 1 , u 1 ) q 3 q 4 F (q 3 , u 2 ) F (q 3 , u 1 ) F (q 4 , u 1 ) q 3 F (q 4 , u 2 ) F (q 5 , u 1 ) F (q 5 , u 2 ) q 5 q 4 q 5 q 3 dom( C) = ∪ 5 i=3 ↓ q i Figure 5
.6: Illustration of Algorithm 5.3. If p(q) = 1, then q either blue or white. Red states are uncontrollable (i.e. p(q) = 0). Blue states are the basis of a set Q E . The input set U = {u 1 , u 2 }.

Proof. Let us first remark that Algorithm 5.3 repeats Algorithm 5.2 until the line 12 and then instead of initializing a controller C it simply returns the domain of C. Thus, it is enough to prove that Dom(C) = Dom( C), where C is a controller synthesised by Algorithm 5.2 for a LSM transition system Σ = (Q, U, F ), lower-closed safety specification Q S ⊆ Q and the information function defined by (5.3). And C is the maximal safety controller for or the transition system Σ = (Q, U, F ), and safety specification Q S ⊆ Q. Since we know that C can be calculated with Algorithm 2.1, let us run Algorithm 2.1 in parallel to Algorithm 5.2. Let the sets Q i E,1 , Q i E,2 contain all states from Q such that p i 1 (q) = 0, p i 2 (q) = 0 at the beginning of ith iteration of the loop 6-11, of Algorithm 2.1 and 5.2 correspondingly.

Obviously,

Q 1 E,1 = Q 1 E,2 . Let Q 1 E,i ⊆ Q 2 E,i then B i 1 ⊆ B i 2 and consequently Q i+1 E,1 ⊆ Q i+1 E,2
. Hence, by induction we get that Dom( C) ⊆ Dom(C).

To show that Dom(C) ⊆ Dom( C) let us first prove that Dom(C) is lower-closed. At the beginning of the loop 6-11 of Algorithm 5.2 the set Q E = {q ∈ Q | p(q) = 0} coincides with Q S , and, hence, Q 1 E is lower-closed. Let at the ith iteration of the loop the set Q i E = {q ∈ Q | p i (q) = 0} is lower-closed. Since with the information function defined by (5.3) we reduce priorities for some states from Bas(Q i E ) the set Q i+1 E is also lower-closed. Thus, Dom(C) =↓ Dom(C). Taking into account that Σ = (Q, U, F ) is LSM, we can define a new controller C for Σ as follows: C * (q) = ∅ for all q ∈ Q \ (Dom(C)), while for all q ∈ Dom(C) we set C * (q) = ∪ {q ∈Bas(Dom(C))|q∈↓q } C(q ). Indeed, if an input is enabled at a state q ∈ Q it is also enabled for all q ∈↓ q and the definition of C * is correct. Since Dom(C * ) = Dom(C) to end the proof it is enough to show that C * is a safety controller for the transition system

Σ = (Q, U, F ), and safety specification Q S ⊆ Q. Indeed, Dom(C * ) = Dom(C) ⊆ Q S . Moreover, for all q ∈ Dom(C * )
for all u ∈ C * (q) there exist q ∈ Bas(Dom(C * )) such that q ∈↓ q , F (q , u) = ∅ and F (q , u) ⊆ Dom(C) = Dom(C * ).

From Corollary 5.2.1 we have that F (q, u) ⊆↓ F (q , u). The same time ↓ F (q , u) ⊂ Dom(C * ) since Dom(C * ) is lower-closed. So, C * is a safety controller and Dom(C * ) ⊆ Dom( C).

Hence, to compute the domain of the maximal safety controller for LSM transition system and lower-closed safety specification, it is enough to explore only the basis of Q E . Figure 5.6 illustrates execution of Algorithm 5.3 for a simple transition system. As soon as every state in Q EB is non-blocking with respect to the reduced transition relation F p , i.e. for every q

∈ Q EB = Bas(Q E ) there exists u ∈ U such that F (q, u) ⊆ Q E =↓ Q EB we may conclude q 4 q 3 q 5 dom( C) = ∪ 5 i=3 ↓ q i F (q 3 , u 1 )
F (q 4 , u 1 ) F (q 5 , u 1 )

F (q 3 , u 2 ) F (q 4 , u 2 ) F (q 5 , u 2 )
q 5 q 4 q 5 q 3 q 4 q 3 q 5 q 3 q 6 F (q6, u1)

F (q 7 , u 2 ) q 5 q 4 q 7 F (q 7 , u 2 ) q 5 q 4 q 8 q 5 q 8 q 3 q 4 q 6 C P re(dom( C), u 2 , dom( C)) P re(dom( C), u 1 , dom( C)) Let now D ⊆ A, assuming that D ⊆ Pre(A, u, B) we immediately have from the Definition 5.3.2 that F (q, u) ⊆ B for all q ∈ Bas(D) since Bas(D) ⊆ D ⊆ Pre(A, u, B) . Now let us prove the second implication. Let for all q ∈ Bas(D) the set F (q, u) ⊆ B. First, we have that D ⊆ A. For q ∈ D, there exists q ∈ Bas(D) such that q ≤ Q q .

Hence, F (q , u) ⊆ B. Since q ≤ Q q , we have from Corollary 5.2.1 that F (q, u) ⊆↓ F (q , u) ⊆↓ B = B. Hence, D ⊆ Pre(A, u, B).

Corollary 5.3.2. Let C be the maximal safety controller for a LSM transition system Σ = (Q, U, F ) and lower-closed safety specification Q S ⊆ Q. Then for all q 1 , q 2 ∈ Q, if q 1 ≤ Q q 2 then C(q 2 ) ⊆ C(q 1 ).

Intuitively, the set Pre(A, u, B) can be seen as the maximal by inclusion lower-closed subset C of B such that for all q ∈ Bas(C) the set F (q, u) ⊆ B. Hence, to compute we can use the following procedure. Initializing a set Q E with a set Bas(A) at line 4 of Algorithm 5.4, we first explore every element of the Q E . Those q ∈ Q E which are controllable (i.e., there exist an input u ∈ U such that F (q, u) ⊆ B ) we accumulate in a set Q C , all the others in a set Q U . Then, at the next iteration of loop 3-7, we shrink out all uncontrollable states from a set A and explore the basis of what is left. However, for states belonging to Bas(A \ Q U ) ∩ Q C we already know that they are controllable, so we

focus on q ∈ Q E = Bas(A \ Q U ) \ (Bas(A \ Q U ) ∩ Q C ).
Then there are two options. If Q E is non-empty, we should re-update the sets Q U and Q C (lines 5 and 6) and go for another loop iteration. While if Q E is empty, we can stop the procedure. Indeed Q E = ∅ if either all states in A are uncontrollable, or we find a set of controllable states Q C , such that for any two states q, q ∈ Q C are incomparable with respect to the order Q . Moreover, for all states in A • CL is the maximal safety controller for the transition system Σ and the lower-closed safety specification Q L ;

• CU is the maximal safety controller for the transition system Σ and the upper-closed safety specification Q U .

Then, for all q ∈ Q, CLU (q) ⊆ CL (q) ∩ CU (q). Proof. Since Q LU ⊆ Q L , we have that CLU (q) ⊆ CL (q) for all q ∈ Q. Similarly, using the fact that Q LU ⊆ Q U we have that CLU (q) ⊆ CU (q) for all q ∈ Q. Hence, we have that CLU (q) ⊆ CL (q) ∩ CU (q) for all q ∈ Q.

The idea of this section is to incrementally synthesize the controller CLU by proceeding in two steps: 1) synthesize the controllers CU and CL ; 2) synthesize the maximal safety controller for the transition system Σ and safety specification Dom( CL ) ∩ Dom( CU ), where for each state q ∈ Dom( CL ) ∩ Dom( CU ), we explore only the inputs u ∈ CL (q) ∩ CU (q). The completeness of the proposed incremental synthesis concerning the classical synthesis is shown in the following result.

Proposition 5.3.2. Under the preliminaries of Lemma 5.3.3, let us define the set Z = Dom( CL ) ∩ Dom( CU ). Let CZ be the maximal safety controller for the transition system Σ and safety specifications Z. Then, for all q ∈ Q,

CLU (q) = CZ (q). Proof. Using the fact that Z = Dom( CL ) ∩ Dom( CU ) ⊆ Q LU = Q L ∩ Q U ,
it follows that CZ (q) ⊆ CLU (q) for all q ∈ Q. On the other hand, we have from Lemma 5.3.3 that Dom( CLU ) ⊆ Dom( CL ) ∩ Dom( CU ) = Z. Hence, CLU (q) = CZ (q) for all q ∈ Q, which ends the proof.

Certainly, the attentive reader may remark that execution of both steps of the synthesis procedure proposed above is equivalent to the execution of the most classical Algorithm 2.1 when we apply it for a pre-computed transition system. However, let us remind that in the first step, we can use more efficient sparse abstractions. And since the symbolic model is calculated on-the-fly the latter speeds up the computations. Moreover, in some particular cases, one can get the maximal safety controller CLU directly from the controllers CL and CU , without running the second step at all. Proposition 5.3.3. Under the preliminaries of Lemma 5.3.3, if for all q ∈ Dom( CL ) ∩ Dom( CU ), CL (q) ∩ CU (q) = ∅, then for all q ∈ Q, CLU (q) = CL (q) ∩ CU (q).

Proof. The first inclusion follows from Lemma 5.3.3. To deal with the second inclusion, let us show that the controller C LU = CL ∩ CU is a safety controller for the transition system Σ and safety specification Q LU . First, we have that

Dom(C LU ) ⊆ Dom( CL ) ∩ Dom( CU ) ⊆ Q L ∩ Q U = Q LU .
Hence, the first condition of Definition 2.2.1 is satisfied. Now let q ∈ Dom(C LU ) and u ∈ C LU (q) = CL (q) ∩ CU (q), the existence of such u is guaranteed by the fact that CL (q) ∩ CU (q) = ∅. Since CL and CU are safety controllers, we have that F (q, u) ⊆ Dom( CL ) ∩ Dom( CU ) = Dom(C LU ). Hence, the second condition of Definition 2.2.1 is satisfied. Then, C LU is a safety controller for the transition system Σ and safety specification Q LU . Hence, from maximality of the controller CLU , we have that C LU (q) = CL (q) ∩ CU (q) ⊆ CLU (q), for all q ∈ Q, which ends the proof. Setting a time step τ = 0.8 s, we generate a discrete-time model corresponding to the continuous-time system (5.5)-(5.7). We also introduce a Cartesian partition on the set X, such that a safe set Y ⊂ X, and input space U with n x = (31, 31, 31) and n u = 50 as state and input discretization parameters correspondingly. We then construct a sparse symbolic model and use Algorithm 5.5 to synthesize the maximal safety controller C for the abstraction.

Let us remind that if for a state q ∈ X an input u ∈ C(x), then all inputs satisfying u U u are enabled by C for this state. Moreover, in our example, we have total order on the input space U . Hence, for each state, it is enough to store only the maximal safe input to reconstruct the whole maximal safety controller (i.e. in fact we synthesize and store maximal input-lazy safety controller). Consequently, the amount of memory required for the controller implementation is significantly reduced. We represent the obtained maximal safety controller C in Figure 5.10.

The blue color of the color bar corresponds to the minimal input F min = -4031.9 mKg/s 2 and the yellow color corresponds to the maximal input F max = 2687.9 mKg/s 2 . For a given state x = (w, d, v), Figure 5.10 shows the maximal allowed control input. Let us remark that to refine the abstract controller for the original system we can either use the classical refinement scheme (Section 1.3) or even consider a closed-loop controller u : X → U ensuring more difficult specifications [Darbha, 1997] as soon as u(x) U C(q), where q is a state such that x ∈ q.

To evaluate the performance of our approach, we compare it with the classical safety synthesis algorithm while exploring different scenarios: we compare our approach with the box abstractions [Tabuada, 2009] and the sparse abstractions [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF]. We also provide a comparison with lazy synthesis procedure, based on three valued abstractions [START_REF] Hussien | Lazy controller synthesis using three-valued abstractions for safety and reachability specifications[END_REF]. In [START_REF] Hussien | Lazy controller synthesis using three-valued abstractions for safety and reachability specifications[END_REF], once a safe input is found for a state, the other controls are not explored for this state. The authors start with an empty transition relation and iteratively add new transitions essential for the synthesis purpose. At every iteration, the precomputed part of the symbolic model is explored. Then, one randomly chooses N 3v ∈ N >0 states from uncontrollable states, where N 3v is a parameter Table 5.1: Runtime comparison when varying the number of states. T s lm , T cl , T s cl and T s 3v are the running time of Algorithm 5.5, the classical fixed point algorithm with box abstractions [Tabuada, 2009] and with sparse abstractions [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF] and the lazy algorithm from [START_REF] Hussien | Lazy controller synthesis using three-valued abstractions for safety and reachability specifications[END_REF] are the required memory to implement the controller resulting from Algorithm 5.5, the classical fixed point algorithm with box abstractions [Tabuada, 2009], the classical fixed point algorithm with sparse abstractions [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF] and the lazy algorithm from [START_REF] Hussien | Lazy controller synthesis using three-valued abstractions for safety and reachability specifications[END_REF], respectively. 15,15,15) 26.4 KB 499.9 KB 18.93 (31,31,31) 232.7 KB 4729 KB 20.32 (63,63,63) 1953.5 KB 41469.3 KB 21.22 given by user. For each of chosen states, one randomly picks an unexplored input and adds the corresponding tradition to the abstraction. The algorithm returns only the domain of the maximal safety controller and not the whole maximal safety controller. Indeed, for every state, only one safe input is returned. Moreover, since the usage of sparse abstractions speed-up synthesis process we also use them when implementing the approach from [START_REF] Hussien | Lazy controller synthesis using three-valued abstractions for safety and reachability specifications[END_REF]. The evaluation is based on two criteria, the computation time and the memory required to implement the maximal safety controller. We explore two different scenarios. In the first case, we vary the state-space discretization parameter n x while keeping the input discretization parameter as a constant n u = 10.

n x M s lm = M s 3v M cl = M s cl M cl /M lm (
The results of run time and memory comparison are represented in Table 5.1 and Table 5.2. In the second case, we set n x = (31, 31, 31) and vary the input discretization parameter n u . The computational results are given in Table 5.3 and Table 5.4.

In Tables 5.1, 5.3, time T s lm is a running time of Algorithm 5.5. Time T cl is a running time of the classical fixed point algorithm when box abstractions are used [Tabuada, 2009]. Time T s cl is a running time of the classical fixed point algorithm when sparse symbolic models are used [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF]]. Time T s 3v is a running time of the lazy algorithm from [START_REF] Hussien | Lazy controller synthesis using three-valued abstractions for safety and reachability specifications[END_REF] implemented for sparse abstractions. For the parameter N 3v the value round(0.6 * n x (1) * n x (2) * n x (3)) have been chosen. We also store the amount of memory needed for controllers implementation in variables M s lm , M cl , M cl and M s 3v correspondingly. Let us remind that for ISM with directed specifications the controllers synthesised for sparse abstractions and box abstractions coincide, hence

M cl = M s cl (column 3 in Tables 3,5). However, it is obvious from columns 3 and 4 of Tables 2,4 that sparse abstractions-based synthesis is much faster, so we repeated the result from [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF]. Since our controller and 3-valued abstractions-based controller store just one safe input for every state, their memory requirements also coincide (column 2 in Tables 3,5). However, we store the maximal safe input for every state. We can easily reconstruct the maximal safety controller without any computations. In contrast, the three-valued abstractions-based Table 5.3: Runtime comparison when varying the number of inputs. T s lm , T cl , T s cl and T s 3v are the running time of Algorithm 5.5, the classical fixed point algorithm with box abstractions [Tabuada, 2009] and with sparse abstractions [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF] and the lazy algorithm from [START_REF] Hussien | Lazy controller synthesis using three-valued abstractions for safety and reachability specifications[END_REF] are the required memory to implement the controller resulting from Algorithm 5.5, the classical fixed point algorithm with box abstractions [Tabuada, 2009], the classical fixed point algorithm with sparse abstractions [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF] and the lazy algorithm from [START_REF] Hussien | Lazy controller synthesis using three-valued abstractions for safety and reachability specifications[END_REF] controller store just a random safe input, and to get the maximal safety controller, one should check for all the other inputs if they allow to remain in the controllable domain. The latter is not efficient when the set of discrete inputs is large. The numerical results highlight the practical speedups and memory efficiency that can be attained using the lazy approach while ensuring completeness with respect to the classical safety algorithm.

Intersection of lower and upper-closed safety specifications

Let us consider another control objective to illustrate the results of Section 5.3.4. We want to synthesise a controller for the follower vehicle, which takes its values from [F min , F max ], to keep the velocity of the follower below v max and guarantees that the relative distance between the leader and the follower remains larger than d min = 10 m and smaller than d max = 150 m, while assuming that the leader vehicle acts as a disturbance d ∈ [0.65 * F min , 0.65 *

F max ] and w max = 25 m/s. In this case, we can use the approach proposed in Proposition 5.3.2 to speed up the computation by a factor of 3.7 in comparison to the classical approach, or by 5.1 if me combine the the incremental synthesis approach with ideas from Chapter 2. Time gain is a result of using a sparse abstraction, instead of a more common box abstraction, to find CL and CU and then use them as a warm point for the following computations.

Since our abstraction is input-state monotone and we have the total order on set of inputs, it is sufficient for every state x to store only safe actions u s min (x), u s max (x) with minimal and maximal value, because all inputs in a range CU (x). In this case we can fully used the benefits of the Algorithm 5.5, and we are 45.7 times faster than the classical approach. All the implementations has been done in MATLAB, Processor Intel Core i7-8700, 3.20 Hg, RAM 16 GB.

Conclusion

In this Chapter, we provide a lazy control synthesis algorithm for monotone transition systems and directed safety specifications. Two classes of monotone transition systems are presented: state monotone transition systems and input-state monotone transition systems. For the first class of systems, a partial order is defined only on the state space. For the second, the input space is ordered as well. The introduced lazy synthesis approach benefits from the ordered structure of the state (input) space and the fact that directed safety specifications are considered. To enrich the class of the considered specifications, we also present an incremental controller synthesis framework, which allows us to deal with intersections of upper and lower-closed safety requirements. We then compare the proposed approach with the classical safety synthesis algorithm and illustrate the advantages, in terms of run-time and memory efficiency, on an adaptive cruise control problem.

Chapter 6

Conclusion and Future Work

A tendency to automate most life processes makes cyber-physical systems (CPS) are irreplaceable in modern society. However, their design is still challenging, and one of the major issues is how to guarantee that the behavior of CPS satisfies the safety constraints. Indeed, a sound synthesis of safety controllers requires model-based approaches. At the same time, the heterogeneous nature of models motivates the usage of abstraction-based techniques, which unfortunately suffer from poor scalability. In this manuscript, we improved the efficiency of abstractionbased approaches by developing algorithms that synthesize the controllers for symbolic models lazily. The proposed algorithms outperform the classical synthesis procedure [Tabuada, 2009] by avoiding computations, which are nonessential for synthesis goals.

Chapter 2 introduced three lazy synthesis approaches applicable for a general non-deterministic transition system Σ = (Q, U, F ). Algorithm 2.2 avoids exploration of states and transitions which are safely controllable a priory.

It returns the maximal safety controller but requires external knowledge about abstractions, which is not always available. Algorithm 2.3 assumes that the input set U is equipped with a partial order and then explores the lowerpriority actions only if the problem is unsolvable with higher-priority actions. It returns the maximal input-lazy safety controller, whose domain coincides with the maximal controllable set, but only inputs with the highest priority are enabled among several inputs preserving safety. Algorithm 2.4 assumes that the initial set Q init ⊂ Q is known and avoids exploration of non-reachable part of abstraction. It returns the maximal state-lazy safety controller, whose domain includes a safely controllable state if and only if it is reachable from Q init . Using lazy algorithms, we can synthesize the abstract controller more efficiently than with the classical Algorithm 2.1. Moreover lazy synthesis allows us to calculate only the part of the abstraction which is involved in the synthesis procedure. Thus, the performance of symbolic model-based approaches is improved.

In Chapter 3 we used abstraction-based techniques to synthesize a safety controller for a general continuoustime control system. The main idea was is to create a neighbor-linked abstraction, where only transitions between neighboring states are allowed. To enforce the desired structure of the symbolic model, we introduced a novel input u, then all states belonging to ↓ q are controllable with an input u. Moreover, for a lower input-state monotone transition system, if for a state q an input u is safe, then all actions u u are safe. We then enriched the class of considered specifications by intersections of lower-closed and upper-closed sets. The numerical implementations of Chapter 5 emphasised the significant improvement in efficiency comparing to the classical algorithms. Certainly, at first glance, it may seem that the results are too limited by a specific class of systems and specifications, but recent research showed that such a problem statement do arrive in challenging practical applications [START_REF] Smith | Monotonicity-based symbolic control for safety in driving scenarios[END_REF].

Future Research

What priorities on inputs should be like?

In Chapter 3 we introduced a partial order on input space by prioritising actions with a longer duration. In Chapter 5 the partial order was naturally inherited from the dynamic of the original plant. However, we find inspiring the ideas to explore the most promising actions [Hart et al., 1968, Rungger and[START_REF] Rungger | [END_REF] first or favor leastviolating [Girard andEqtami, 2021, T ůmová et al., 2012] actions. Moreover, one may be interested in prioritizing the actions based on requirements of an additional specification. Another interesting trend in symbolic model control is prioritize actions which reduce non-determinism.

Adaptive time sampling technique as a way to enforce the desired structure

Abstractions computed with pre-fixed time-sampling are hard to be analyzed since in general, they don't have any particular structure. The same time the results of Chapters 3 and 5 showed that geometrical patterns are the way to ease computations. Moreover playing with transition duration one can create lattice graphs [START_REF] Pivtoraiko | Differentially constrained mobile robot motion planning in state lattices[END_REF],

which were advocated when dealing with systems invariant with respect to geometrical shift, like kinematics models in robotics applications.

Another issue is that for the moment adaptive time-sampling is restricted to a continuous-time system. However, it is interesting to investigate the applicability of such a technique when dealing with discrete-time systems: what the relation between time and space-sampling parameters should be like.

Monotone dynamical systems and beyond...

In Chapter 5 we adopted the results designed for directed safety specifications to their intersection. However, the incremental synthesis approach of Section 5.3.4 still includes a classical synthesis procedure as the last step. At the same time there exists a criterion for an interval to be the controlled interval when monotone dynamical systems are considered [START_REF] Meyer | Controllability and invariance of monotone systems for robust ventilation automation in buildings[END_REF]. Moreover, the result from [START_REF] Meyer | Controllability and invariance of monotone systems for robust ventilation automation in buildings[END_REF] allows us to synthesize a safety controller. We believe that in combination with the ideas of this manuscript, the safety specification can be extended towards the union of several intervals. Another drawback of [START_REF] Meyer | Controllability and invariance of monotone systems for robust ventilation automation in buildings[END_REF] to be overcome, is an assumption that every control component can affect no more than one state variable.

One of the practical interests to investigate monotone dynamical systems is the fact that their analysis is the first step towards the analysis of mixed-monotone systems, which are a very general class of systems [START_REF] Yang | On sufficient conditions for mixed monotonicity[END_REF].

Non-linear systems are often considered through the prism of hybridization or linearisation in order to benefit from linear analysis techniques. However, we believe that addressing monotone patterns in dynamic of non-linear systems through decomposition functions and then benefit from the results for monotone systems is a promising direction of the research.

One important step towards more general specifications

This thesis was dedicated to safety specifications. The motivation was to develop efficient synthesis algorithms for non-deterministic abstractions. The interest for a non-deterministic symbolic model is justified by a limited class of systems [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF] and specifications [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF] for which a deterministic abstraction can be constructed. However, when addressing other control problems, such as, for example, a reach-avoid specification, the non-determinism in the abstraction may ruin everything, making the synthesis unsuccessful even when the controller exists for the original plant. Indeed, if the reachable sets are growing with time, the error propagates too fast (see Figure 6.1 (left)). Hence, it is hardly possible that we can target a small final set. Even in some particular cases, the wrapping effect can be compensated by fine discretisation [START_REF] Hsu | Lazy abstraction-based controller synthesis[END_REF] this results in very intensive computations. The demand to enforce determinism raised a wave of research in coupling abstraction-based methods with local feedback controllers ensuring local stability properties of the closed-loop systems [Tabuada, 2008, Sinyakov and[START_REF] Sinyakov | Formal Synthesis from Control Programs[END_REF]. And this is a problem to pay attention for. • g(t, [x; x], [u; u], [w; w]) = f (t, x, u, w);

• g i (t, [x; y], [u 1 ; u 2 ], [w 1 ; w 2 ]) is non-decreasing in x j , non-increasing in y j when i = j.

• g i (t, [x; y], [u 1 ; u 2 ], [w 1 ; w 2 ])) is non-decreasing in u 1 and w 1 , non-increasing in u 2 and w 2 .

We call f a mixed monotone function and system (1.1) a mixed monotone system if there exits such decomposition function g.

Definition A.0.2. Let f be a mixed monotone function and g be a decomposition of f . Decomposition function g is called tight if for all i ∈ {1, . . . , n x }, for all t ∈ [0, T ], for all x 1 , x 2 ∈ R nx , for all u 1 , u 2 ∈ U , and all w 1 , w 2 ∈ W such that x 1 ≤ x 2 , u 1 ≤ u 2 , w 1 ≤ w 2 , it follows that g i (t, [x 2 ; x 1 ], [u 1 ; u 2 ], [w 2 ; w 1 ]) = max

(ζ i (x, y)) j =             
x j , j < n x y j , j > n x , j = n x + i

x i , j = n x + i Supposing that the initial set X 0 = [x 0 , x 0 ] is an interval, consider a system of equations (i = 1, . . . , n x ) ẋi = g i (t, ζ i (x, x), [û, û], ω), x i (0) = x 0 i ẋi = g i (t, ζ i (x, x), [û, û], ω), x i (0) = x 0 i (A.2)

Denoting the components of its solution as x(t; [x 0 , x 0 ], û) and x(t; [x 0 , x 0 ], û), we have that Reach(t |, X 0 , û) = [x(t; [x 0 , x 0 ], û), x(t; [x 0 , x 0 ], û)] (A.3) is an over-approximation of the forward reachable set Reach(t |, X 0 , û).

1. 1

 1 Illustration of an abstraction-based control synthesis approach for a safety specification. . . . . . . . . 1.2 The left figure illustrates adaptive time-sampling techniques: while transition duration is commonly determined by a given time sampling parameter τ , we propose interrupting every transition stops just before leaving N A (q). The right figure represents the result of the synthesis procedure for an arbitrary abstraction, while the central figure shows the corresponding domain of the continuous-time controller. In the green region, we apply any admissible input, but as soon as closed-loop trajectory reaches the white area, we switch to the "abstract" controller, which steers us back to the controllable domain. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

3. 2

 2 figures represent a corresponding closed-loop trajectory of the dynamic system (3.9), starting at [20, 15, 5] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  of the difference between multilayered and adaptive grid. Left figure shows the successors F (q, u) on 2-layered grid, while the right figure on the corresponding adaptive grid. . . . . . . . . . . . 4.4 Illustration of the considered configuration for temperature regulation problem. . . . . . . . . . . . . . 4.5 Simulation results. A grey area corresponds to the controllable domain: light states are controllable by the actions with priority 1; dark states -with priority 2. The white area is uncontrollable. Concerning the closed-loop trajectory, orange color corresponds to a control {0, 0}, green -to a control {0, 1}, violet -to a control {1, 0}. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.1 Illustration of Definitions 5.1.3 and 5.1.5. The left figures show two trajectories of an input-state monotone dynamical system. The right figure provides an example of a lower-closed safety set. In all

  figure illustrates the result of Theorem 5.3.2. States filled with yellow are controllable by u 2 , with blue -by u 1 , with green -by both u 1 and u 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.8 Illustration of the reordering U = {u 1 , . . . , u 9 } of the input set U = {1, 2, 3} 2 with respect to the component-wise partial order defined on R 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.9 Illustration of the maximal safety controller C for the case of a total order on the input set. U = {u 1 , u 2 , u 3 } with u 1 U u 2 U u 3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 1 . 1 :

 11 Figure 1.1: Illustration of an abstraction-based control synthesis approach for a safety specification.

Proof.

  The proof of the fact that Dom(C * ) = {q ∈ Q | p(q) = 0} also as the fact that C * is a safety controller repeats the proof of analogous result from the Theorem 2.2.1. Since C * is a safety controller Dom(C * ) ⊆ Cont(Σ, Q S ). To prove that Cont(Σ, Q S ) ⊆ Dom(C * ) let me run the Algorithm 2.3 for the transition system Σ = (Q, U, F ) and a safe set Cont(Σ, Q S ) and let the controller C * 1 is the result of the execution. Since the result analogous to Lemma 2.2.2 can be proven for Algorithm 2.3 as well the following inclusion holds C * 1 (q) ⊆ C * (q) for all q ∈ Q. Consequently Dom(C * 1 ) ⊆ Dom(C * ) and since Dom(C * 1 ) = Cont(Σ, Q S ) and we get what we want.

Figure 2 .

 2 Figure 2.3 illustrates the execution of Algorithm 2.3 for a simple transition system. In opposite to previous examples, now actions have different priorities, and we enable for a state actions u 3 , u 4 , only if it is uncontrollable

Figure 3 . 1 :

 31 Figure 3.1: Illustration of the adaptive time sampling technique (right figure) compared to a fixed time sampling approach (left figure). Black cells represent unsafe states; green and blue cells represent F (q, u 1 ) and F (q, u 2 ) correspondingly. The red square represents the abstract state neighborhood N A (q). While in the left figure, transition duration is determined by pre-fixed time sampling parameter τ f ix , in the right figure, a transition stops just before leaving N A (q) (see eq. (3.2)).

  Q S , I EB ) Input: Σ = (Q, U, F ), a safe set QS, an indicator IEB Output: Maximal Safety Controller C {q ∈ Q | p(q) = 0 and IEB(q) = 1}; 8 B := BlockF p (QEB);

  9

  For a given control system Σ f = (T , R nx , U, W, f ) all trajectories of closed-loop system (1.1),(3.5)-(3.8) starting from a Dom(C) at t = 0 stays within the set S ⊆ Y for all t ∈ T no matter which disturbance w ∈ L(T , W) has been applied.Proof. For any initial condition x(0) ∈ Dom(C) and any disturbance w ∈ L ∞ (T , W) the closed-loop trajectory ẋ(t) = f (x(t), u(t, x), w(t)), t ∈ T can not leave the Dom(C) without passing through the set Q B , and for every state in Q B there is a controller which brings us back to the Dom(C) ⊆ S ⊆ Y (see Algorithm 3.2). The Zeno behaviour is impossible since being in mode 0 at t = s ∈ T we can either stay in mode 0 for all t ∈ [s, +∞) or switch to mode 1. If we have switched to mode 1 we spent there at least τ k seconds before switching back to mode 0.

q 16 q 11 Figure 3 . 2 :

 1132 Figure 3.2: Illustration lazy synthesis based on boundary exploration idea. First figure illustrates the discretization of the original state space R 2 . The safe set Y is countered with blue; white cells are safe states; the unsafe state is filled with gray. Figures 2-5 illustrate the execution of Algorithm 3.2. States filled with white and green have priority 1; with grey -priority 0. White states belong to Q EB . States contoured with red are blocking. The inputs set U = {u 1 , u 2 }. Actions corresponding to control u 1 are black, u 2 are blue. Transitions marked with red are unsafe. In opposite to normal line, the dashed line represents transitions that haven't been computed yet. Last figure illustrates a piece of trajectory of a closed-loop system (1.1),(3.5)-(3.8). White states belong to Q B ; green area corresponds to Q I . Normal line represents mode 0, dashed line -mode 1.

  ." Still procedure (3.5)-(3.8) refines C to solve the original problem in the continuous-time domain. For any x ∈ Q B ⊆ Dom(C), there is an abstract input steering the closed-loop trajectory either to Q I or Q B .h For any x ∈ Q I , we can use any control value from U until the trajectory reaches the border Q B again. There we should switch the mode. Certainly, the trajectory may stay

  describes aerodynamic and rolling resistance effects. The net force F i is viewed as a control input for the following vehicle and as a disturbance for the lead one. It is assumed that F i ∈ [a, b], where a = -0.3mg, b = 0.2mg, g is a gravitational constant. Such bounds are consistent with non-emergency braking and acceleration.

Figure 3

 3 Figure 3.3: Illustration an adaptive cruise control problem configuration with a constant time headway spacing policy.

Figure 3

 3 Figure 3.4: Simulation results. Left figure illustrates a safety specification. Right figure represents the domain of the safety controller computed by Algorithm 3.2.

Figure 3 . 5 :

 35 Figure 3.5: Simulation results. Left figures represent a disturbance realization F 1 and a safety control F 2 . Right figures represent a corresponding closed-loop trajectory of the dynamic system (3.9), starting at[20, 15, 5]

Figure 4 . 4 :

 44 Figure 4.4: Illustration of the considered configuration for temperature regulation problem.

Figure 4

 4 Figure 4.5: Simulation results. A grey area corresponds to the controllable domain: light states are controllable by the actions with priority 1; dark states -with priority 2. The white area is uncontrollable. Concerning the closed-loop trajectory, orange color corresponds to a control {0, 0}, green -to a control {0, 1}, violet -to a control {1, 0}.

  0 = [19, 23] × [19, 23], safe set Y = [19, 23] × [19, 23], and a disturbance t e ∈ [-10, 10]. We also suppose that at given instant at most one heater is switched on, i.e. a control set U = {{0, 0}, {0, 1}, {1, 0}}. For the abstraction, we chose L = 4, n x = [4; 4], U µ = U, and n p = 2. Let us introduce the notation A state vector x = [T 1 ; T 2 ].

  • and t max e = 10C • and initial point x 0 = [19.084; 19.27]. The orange color correspond to a control {0, 0}, green to a control {0, 1}, violet to a control {1, 0}. To evaluate efficiency, we also run a simulation for two extreme cases: L = 1, n x = [4; 4] and L = 1, n x = [25; 25], which correspond to a coarsest grid and to a finest grid of considered four-layered adaptive grid. One can see the comparison of the results in Table

Figure 5 . 1 :

 51 Figure 5.1: Illustration of Definitions 5.1.3 and 5.1.5. The left figures show two trajectories of an input-state monotone dynamical system. The right figure provides an example of a lower-closed safety set. In all figures, a natural component-wise order on R 2 is considered for both the input and the state spaces.

  Let L be a partially ordered set, a lower closure of a set A ⊆ L is a set ↓ A = a∈A ↓ a, where↓ a = {q ∈ L | q L a}, while an upper closure is a set ↑ A = a∈A ↑ a, where ↑ a = {q ∈ L | a L q}.Definition 5.1.5. Given a partially ordered set, we say that a subsetA ⊆ L is lower-closed (respectively upperclosed) if ↓ A = A (respectively ↑ A = A).We illustrate the Definition 5.1.5 with a lower-closed set Y in Figure5.1. The following result shows that union (an intersection) of a lower-closed (upper-closed) sets is lower-closed (upper-closed).

Figure 5 . 4 :

 54 Figure 5.4: Illustration of difference between box and sparse abstractions. Left: A box abstraction for a fixed disturbance interval [w m 1 , w m 2 ], m ∈ {1, . . . , M }. Right: box (grey) and sparse (blue) abstractions for a monotone system with a lower-closed safety specification for M = 3.

Figure 5 . 5 :

 55 Figure 5.5: Illustration of Definition 5.3.1. A lower-closed set A and its basis Bas(A) = {a 1 , a 2 , a 3 , a 4 }. The statespace is equipped with the component-wise partial order defined on R 2 and we have: A =↓ A =↓ Bas(A).

  From the definition of reduced transition relation F i p , the Algorithm 5.3: LazySynthesisDomainMSC(Σ, Q S , I EB ) Input: Σ = (Q, U, F ), a safe set Q S , an indicator I EB Output: Domain of MS controller C 1 begin 2

  The last statement is a consequence of the definition of a lower-closed set and the third item of Corollary 5.2.1. Since Bas(Q E ) is not the essential basis of the set Q E Algorithm 5.2 (repeats Algorithm 2.2) does not return the maximal safety controller. Still, the following result shows that it returns a controller which domain coincides with Dom( C). Theorem 5.3.1. Let us run Algorithm 5.3 for a LSM transition system Σ = (Q, U, F ), lower-closed safety specification Q S ⊆ Q and the information function

Figure 5

 5 Figure 5.7: Illustration of lazy synthesis of the maximal safety controller for a LSM transition system with lowerclosed specification. Red state are uncontrollable. White states belong to Dom( C). The left figure represents the Dom( C) and its basis {q 3 , q 4 , q 5 }. Figures in the middle illustrate computation of the sets P re(Dom( C, u 1 , Dom( C))) and P re(Dom( C, u 2 , Dom( C))) by Algorithm 5.4. States filled with grey belong to Q U . States contoured with colors belong to Bas(Dom(C) \ Q U ). States contoured with blue and yellow are controllable by inputs u 1 and u 2 correspondingly (i.e. belong to Q C ). The right figure illustrates the result of Theorem 5.3.2. States filled with yellow are controllable by u 2 , with blue -by u 1 , with green -by both u 1 and u 2 .

Figure 5 .

 5 Figure 5.10: Simulation results. Maximal safety controller C for a lower-closed safety specification.

  u s max (x)] are admissible. See the maximal controller in the Figure 5.11. If we set up the parameter d max as 200 m the assumption of Proposition 5.3.3 is satisfied and CLU (x) = CL (x) ∩

  Figure 5.11: Simulation results. Maximal safety controller C for an intersection of lower-closed and upper-closed safety specification.

Figure 6 . 1 :

 61 Figure 6.1: Left figures illustrates construction of a non-deterministic abstraction. Right figures illustrates a deterministic one.

  f i (t, x, u, w) Let us also introduce a set of notation: θ = [u, u], θ = [u, u], ω = [w, w], ω = [w, w]. And define function ζ i that map R 2nx into itself:

Titre:

  Synthèse efficace des contrôleurs de sécurité à l'aide de modèles symboliques et d'algorithmes paresseux Mots clés: Synthèse de contrôleur, Modèles symboliques, Méthodes formelles Résumé: Cette thèse porte sur le développement d'approches efficaces de synthèse de contrôleurs basées sur l'abstraction pour les systèmes cyber-physiques (CPS). Alors que les méthodes basées sur l'abstraction pour la conception de CPS ont fait l'objet de recherches intensives au cours des dernières décennies, l'évolutivité de ces techniques reste un problème. Cette thèse se concentre sur le développement d'algorithmes de synthèse paresseuse pour les spécifications de sécurité. Les spécifications de sécurité consistent à maintenir la trajectoire du système à l'intérieur d'un ensemble sûr donné. Cette spécification est de la plus haute importance dans de nombreux problèmes d'ingénierie, souvent prioritaires par rapport à d'autres exigences de performance. Les approches paresseuses surpassent l'algorithme de synthèse classique [Tabuada, 2009] en évitant les calculs, qui ne sont pas essentiels pour les objectifs de synthèse. Le chapitre 1 motive la thèse et présente l'état de l'art. Le chapitre 2 structure les approches de synthèse paresseuses existantes et met l'accent sur trois sources d'efficacité : les informations sur les états contrôlables a priori, les priorités sur les entrées et les états non accessibles à partir de l'ensemble initial. Le chapitre 3 propose un algorithme, qui explore itérativement les états à la frontière du domaine contrôlable tout en évitant l'exploration des états internes, en supposant qu'ils sont contrôlables en toute sécurité a priori. Un contrôleur de sécurité en boucle fermée pour le problème d'origine est alors défini comme suit : nous utilisons le contrôleur abstrait pour repousser le système d'un état limite vers l'intérieur, tandis que pour les états internes, toute entrée admissible est valide. Le chapitre 4 présente un algorithme qui restreint les calculs de synthèse du contrôleur aux seuls états atteignables tout en privilégiant les transitions de plus longue durée. Le système original est abstrait par un modèle symbolique avec une grille adaptative. De plus, un nouveau type d'échantillonnage temporel est également envisagé. Au lieu d'utiliser des transitions de durée prédéterminée, la durée des transitions est contrainte par des intervalles d'état qui doivent contenir l'ensemble accessible. Le chapitre 5 est consacré aux systèmes de transition monotones. L'approche de synthèse paresseuse introduite bénéficie d'une propriété monotone des systèmes de transition et de la structure ordonnée de l'espace d'état (d'entrée), et du fait que des spécifications de sécurité dirigées sont prises en compte. La classe de spécifications considérée s'enrichit alors d'intersections d'exigences de sécurité supérieures et inférieures fermées. Le chapitre 6 conclut la discussion et soulève de nouvelles questions pour les recherches futures.

  . . . . . 4.1 Runtime comparison when varying the number of states. . . . . . . . . . . . . . . . . . . . . . . . . .

5.1 Runtime comparison when varying the number of states. T s lm , T cl , T s cl and T s 3v are the running time of Algorithm 5.5, the classical fixed point algorithm with box abstractions

Controller Synthesis for Monotone Transition Systems and Directed Safety Specifications

.

Automatica, 2021.

International conference:

• Ivanova E. and Girard A. Lazy

Symbolic Controller for Continuous-Time Systems Based on Safe Set Boundary Exploration

  . IFAC Conference on Analysis and Design of Hybrid Systems, Brussel, Belgium, July 2021.

• Ivanova E. and Girard A. Lazy Safety Controller Synthesis with Multiscale Adaptive-Sampling Abstractions of Nonlinear Systems. IFAC World Congress, Berlin, Germany, July 2020. • Saoud A., Ivanova E. and Girard A. Efficient Synthesis for Monotone Transition Systems and Directed Safety Specifications. IEEE Conference on Decision and Control, Nice, France, December 2019.

  Starting with the highest priority for states in a safe set Q S and with the lowest one for the others (lines 2-5), we iteratively decreasing by one point the priority of all blocking but controllable states (line 10) in the main block of Algorithm 2.3 (lines 6-11) until the reduced transition relation F p, U stops changing. Then F p, U is used to initialize the controller C. Let us remark that if all inputs have the same priority, Algorithm 2.3 coincides with Algorithm 2.1.

	Theorem 2.3.2. Let C

* computed by Algorithm 2.3. Then, C * is the MILS controller.

  .3: Illustration of Algorithm 2.3 execution. Unsafe actions are red. Blocking states are grey. Controls u 1 , u 2 have priority 2, u 3 , u 4 have priority 1. If a state is contoured with black, it has priority 2, and the actions with priority 2 are enabled for this state. If with blue, it has priority 1, and the inputs with priority 1 are available. If with red, then its priority is 0. We enable lower priority transitions for a state only if it is uncontrollable with higher priority actions. Enable at the current iteration transition marked with a normal line, while action marked with a dashed line are non-available. The actions which remain untouched at step 9 are not included in the maximal input lazy safety controller.

  an MSLS controller exists and is unique, as well. From Definition 2.3.2 it follows that all controllable safety states in Q S , which are reachable from Q init are in Dom(C * ) and this explain the term maximal in the name of C * . At the same time, the controller C * is called state-lazy since non-reachable from the initial set states are not in the domain. The MSLS controller C

* can be obtained from the maximal safety controller C by removing the states that are not reachable from initial states, but this is obviously not the most efficient way to find C * . The main Algorithm 2.4 from Algorithm 2.1 by line 7, thereby restricting exploration to states, which are reachable from the initial set. Let us remark that if Q init coincides with Q S , then Algorithm 2.4 returns the maximal safety controller.

Lemma 2.3.1. Let Q zero

  e max 1,2 ] a uniform Cartesian partition. The number of intervals in every direction is described by a given parameter n p x . Intervals on the border are flat, while internal intervals whether semi-closed from the right side or open if they are next to the right border. For example, in first direction we have {0}, (0, η], (η, 2η], . . . , (v max -η, v max ), {v max }, where η = v max /n p x (1). For every state belonging to a safe set Y , we chose n p u different admissible inputs

Table 4 .

 4 1: Runtime comparison when varying the number of states.

	Grid	Number of states Execution time Controllability Ratio
	Adaptive grid	18	7 s	98%
	Coarsest grid	9	5 s	89%
	Finest grid	625	50 s	98%

  , respectively.

	n x	T s lm	T cl /T s lm	T s cl /T s lm	T s 3v /T s lm
	(15,15,15)	2.96 s	31.22	15.52	11.18
	(31,31,31)	18.16 s	53.35	23.19	14.92
	(63,63,63) 118.67 s	85.21	30.85	16.25
	Table 5.2: Memory comparison when varying the number of states. M s lm , M cl , M s cl and M s 3v

Table 5 .

 5 , respectively. 4: Memory comparison when varying the number of states. M s lm , M cl , M s cl and M s 3v

	n u	T s lm	T cl /T s lm	T s cl /T s lm	T s 3v /T s lm
	10 18.19 s	54.01	23.42	15.06
	20 20.56 s	95.08	41.08	25.96
	40 25.26 s 154.03	66.67	43.25

  , respectively.

	n u M s lm = M s 3v	M cl = M s cl	M cl /M lm
	10	232.7 KB	4729 KB	20.32
	20	232.7 KB	6200.1 KB	26.64
	40	232.7 KB	9141.8 KB	39.29

A binary relation L ⊆ L × L is a total order if it is a partial order and for all l 1 , l

∈ L we have either l 1 L l 2 or l 2 L l 1 .

Acknowledgements

Reach(τ u,2 q | q, u) q ′ q up u Reach(τ u2,2 q | q, u 2 ) Reach(τ u1,1 q | q, u 1 ) 2) with a transition F (q , up) = q, and (4.3) with a transition F (q, u). Unsafe states are marked with black. Right figure illustrates adaptive timesampling techniques (see (4.4)). Transitions with two different duration are shown: for a control u 1 we stop before leaving an interval with a radius 1, while for a control u 2 -an interval with a radius 2.

Synthesis of Maximal Input-State Lazy Safety Controller

The less restrictive safety controller one can provide for Σ = (Q, U, F ) is the maximal safety controller C. Still, its computation is too labor-intensive for many real-world problems. Indeed, according to the classical synthesis approach [Tabuada, 2009] one should first pre-compute the whole symbolic model and then iteratively remove all unsafe transitions from Σ = (Q, U, F ) until the abstraction stops changing. However, the idea of working with a multi-scale abstraction is to explore (and to compute) for a state q transitions with a shorter duration only if q is uncontrollable with longer duration actions. We also do not want to compute abstraction for states embedded in q if it is controllable. Moreover, since Q init is known, it is reasonable to provide a controller only for states that are reachable from the initial set. Let us relax the maximality requirement for a desirable controller. Let the input set U be equipped with the following partial order U • for all (u µ , j 1 ), (u µ , j 2 ) ∈ U µ × {1, . . . , n p } we say (u µ , j 1 ) ≺ U (u µ , j 2 ) if and only if j 1 < j 2 .

• for any (u µ , j) ∈ U µ × {1, . . . , n p } the following holds (u µ , j) ≺ U up.

I.e., transitions with a longer duration are preferred to transitions with a shorter one, and control up has the highest priority. We then aim to compute for Σ = (Q, U, F ) the maximal lazy safety (MLS) controller C * . Where the term maximal refers to the fact that all safety controllable initial states should be in Dom(C * ), and if the controller enables an input, it should also enable all inputs which have the same priority and preserve safety. The term lazy refers to the fact that when several inputs can preserve safety, the controller should enable only inputs with the highest priority. Intuitively, C * can be obtained from C by keeping for every state only those enabled actions, which have a higher priority, and by removing the states that are not reachable from initial states. Certainly, it is not the best way to find C * . In [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF] the authors propose a more efficient synthesis procedure, but their result is u 2 q us u 1 u 2 u 3 u 1 q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15 u 3

q us u 1 u 3 u 1 q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15 u 3

q us u 3 u 1 q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15 u 3

u 2 q us u 3 u 1 q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

q us u 3 q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15

q us u 3 q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 q 9 q 10 q 11 q 12 q 13 q 14 q 15 Enable at the current iteration transition marked with a normal line, while action marked with a dashed line are non-available. Reachable from the initial set states are countered with a normal line, non-reachable with a dashed line. The actions marked with a dashed line in step 9 are not included in the maximal input lazy safety controller.

q ∈ F (q, u) the equality p(q ) = 0 is satisfied. The same time in Algorithm 4.2 the function p : Q → {0, . . . , n p + 1}

determines the priority of a state q ∈ Q. The reduced transition relation F p, U is defined as follows (q, u, q ) ∈ F p, U if and only if p(q) ∈ {1, . . . , n p + 1}, u ∈ U p(q) , (q, u, q ) ∈ F and for all q ∈ F (q, u) the equality p(q ) = 0 is satisfied.

Here U j ⊂ U, j = 1, . . . , n p + 1 are classes of equivalency with respect to the partial order U , i.e. U np+1 = {up},

and input up has the highest priority the later means that we explore q ⊂ q only if q is uncontrollable.

In other words if q eventually gets the priority 0 and l(q) > 1 it is replaced by 2 n states q i ∈ Q l(q)+1 such that q = ∪ 2 n i=1 q i . Thus, the introduction of an artificial input up allows us to manipulate a multilayered grid and transitions duration using one general framework. Let us remark that using Algorithm 4.2 it makes sense to calculate the symbolic model on-the-fly remaining the unexplored part of the abstraction unconstructed.

From a Multilayered to an Adaptive Grid

However, the abstraction considered in the previous section has two significant disadvantages. First, when we run Algorithm 4.2, we have to store a multilayered grid Q, while it is better to work with an adaptive grid consisting of cells of different sizes. Second, for every fixed distribution of priorities of states p : Q → {0, . . . , n p + 1} a reduced transition relation F p, U includes a lot of auxiliary transitions which serves only for switching from a finer layer to a coarser one. At the same time, we prefer to keep in memory only transitions directly related to the dynamic of the original system.

For a given p let us choose as an adaptive grid

q , up) = ∅ and ∃{q i } N i=0 , q i ∈ Q, i = 0, N such that q 0 = q, q = q N , q j+1 = F p, U (q j , up), j = 0, N -1}

and its extension for all

and only if it is reachable from the finest layer only with up transitions, and there is no possibility to go higher for this state. Let us remark that for any q i , q j ∈ Q A p , q i = q j the following q i ∩ q j = ∅ is satisfied, moreover X = ∪ q∈Q A p q. For the associated transition relation let us introduce

Its definition is correct because for any q ∈ Q A p , u ∈ U the set F p, U (q, u) either empty, or included in Q L . Let us remark that for any given p : Q → {0, . . . , n p + 1}, any q ∈ Q A p the set

Proof. Remembering that any non-up transition always finishes at the lowest layer, while input up strictly prioritized that all the others, we have from the definition of Reach F p, U , that q ∈ R, F p, U (q, up) = ∅ is equivalent to the existence of a trajectory

q m,nm = q such that q 0,0 ∈ {q ∈ Q init | p(q) = 0}, q i,0 ∈ Q L for all i = 0, . . . , m and q j,nj ∈ Q A p for all j = 0, . . . , m. This is true (see the the definition of Q p up (q)) if and only if there exist a trajectory only if there exists q ∈ Q L such that q ∈ Q p up (q ), q ∩ Reach(τ uµ,j q

| q, u µ ) = ∅ and the condition of a collision avoidance

]. From Lemma 4.1.1 and definition of up transition the last is equivalent to q ∈ Q A p , q ∩ Reach(τ uµ,j q

| q, u µ ) = ∅, and the condition of a collision avoidance

]. That ends the proof.

We illustrate the difference between a multilayered grid and an adaptive grid in Fig. Finally, we show that we can fully simulate the main part of Algorithm 4.2, using only adaptive grid Q A p and a transition relation F A p . It is also important to mention that the abstraction is not required to be pre-computed but constructed on-the-fly. Let us write, C * (q) := Enab F A p (q) for all q ∈ R * and empty otherwise, for a controller initialization part (lines 12-15). It is obvious, that C * (q) is a safety controller for a transition system Σ * = (Q * , U, F * ), where a state space Q * and a transition relation F * are correspondingly Q A p and F A p after we exit the loop. Moreover, since for any p : Q → {0, . . . , n p + 1}, any q ∈ Q A p the set F A p (q, up) = ∅, the input up never appears in a final safety controller C * . So, we can just skip it from the earlier beginning by initializing in line 3 every safe state with priority n p , instead of n p + 1.

Controller Refinement for an Abstraction with Adaptive Grid

In the previous section, we computed a safety controller C * (q) for a transition system

which is an abstraction for the continuous time Σ f = (T, R nx , U, W, f ). Let us now provide a safety controller for the original plant.

Chapter 5

Efficient Controller Synthesis for Monotone Dynamical Systems and

Directed Safety Specifications

This Chapter is devoted to monotone control systems, i.e., systems whose trajectories preserve some partial orderings on their state and input spaces [START_REF] Angeli | Monotone control systems[END_REF], Hirsch and Smith, 2004, Kamke, 1932, Müller, 1927, Smith, 1995]. On the one hand, our interest is motivated by many practical applications in which such systems appear. For example, traffic networks [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF], Coogan et al., 2016], biological networks [Sontag, 2007, Angeli andSontag, 2003], blood glucose control [START_REF] Gillis | Glucose estimation and prediction through meal responses using ambulatory subject data for advisory mode model predictive control[END_REF], power systems [START_REF] Zonetti | A symbolic approach to voltage stability and power sharing in time-varying DC microgrids[END_REF], vehicle platoons [START_REF] Nilsson | Correct-by-Construction Adaptive Cruise Control: Two Approaches[END_REF] and temperature regulation systems [START_REF] Meyer | Controllability and invariance of monotone systems for robust ventilation automation in buildings[END_REF]. On the other hand, monotone control systems are a subclass of nonlinear control systems relatively easy to analyze, and many notable results

were derived for them last decades. Extending pioneer works of [Kamke, 1932, Müller, 1927, Krasnoselskii, 1968],

Hirsch and Smith contribute to stability theory for continuous-time monotone systems and provide several verification criteria for a system to be monotone [Smith, 1988, Smith, 1995, Hirsch and Smith, 2004]. Angeli and Sontag extend their results to systems with inputs [START_REF] Angeli | Monotone control systems[END_REF]. The monotonicity property also simplifies significally the reachability analysis of the non-linear system [START_REF] Meyer | Interval Reachability Analysis.Bounding Trajectories of Uncertain Systems with Boxes for Control and Verification[END_REF], Ramdani et al., 2010[START_REF] Sinyakov | Formal Synthesis from Control Programs[END_REF]. Concerning to invariance for monotone systems, relying on ideas of [START_REF] Abate | Box invariance for biologically-inspired dynamical systems[END_REF],

the authors in [START_REF] Meyer | Compositional abstraction and safety synthesis using overlapping symbolic models[END_REF] propose a necessary and sufficient condition for an interval to be controlled invariant. However, their result is restricted to monotone systems where every input affects no more than one state variable. We overcome this limitation by using abstraction-based techniques, which allow us to compute a nonconvex safely controllable set for a general monotone dynamical system.

However, we focus on a particular class of safety specifications represented by directed (lower-closed or upper-

Monotone Abstractions for Monotone Dynamical Systems

In this section, we first define the class of monotone dynamical systems. We then present different types of abstractions, namely box and sparse abstractions. Finally, we show under which assumptions these abstractions preserve the monotonicity of the original plant.

Monotone Transition Systems

Let us now introduce the class of monotone transition systems that preserve partial order on input and state spaces.

Definition 5.2.1. Consider a transition system Σ = (Q, U, F ) where the set of states Q is equipped with a partial order Q . The transition system Σ is said to be:

• Lower state monotone (LSM) if for all q 1 , q 2 ∈ Q such that q 1 Q q 2 , for all u ∈ Enab F (q 2 ) it follows, that u ∈ Enab F (q 1 ) and for any q 1 ∈ F (q 1 , u), there is q 2 ∈ F (q 2 , u), such that q 1 Q q 2 ;

• Upper state monotone (USM) if for all q 1 , q 2 ∈ Q such that q 1 Q q 2 , for all u ∈ Enab F (q 1 ) it follows, that u ∈ Enab F (q 2 ) and for any q 2 ∈ F (q 2 , u), there is

The transition system Σ is said to be state monotone (SM) if it is both LSM and USM.

Let us remark that the concepts of USM and LSM coincide when the transition system Σ is deterministic.

Definition 5.2.2. Consider a transition system Σ = (Q, U, F ) where the set of states Q and the set of inputs U are equipped with partial orders Q , U , respectively. The transition system Σ is said to be:

• Lower input-state monotone (LISM) if for all q 1 , q 2 ∈ Q, such that q 1 Q q 2 , for all u 2 ∈ Enab F (q 2 ) all inputs u 1 ∈ U, such that u 2 U u 1 belong to Enab F (q 1 ), and for all q 1 ∈ F (q 1 , u 1 ), there is q 2 ∈ F (q 2 , u 2 ), such that

• Upper input-state monotone (UISM) if for all q 1 , q 2 ∈ Q, such that q 1 Q q 2 , for all u 1 ∈ Enab F (q 1 ) all inputs

, and for all q 2 ∈ F (q 2 , u 2 ), there is q 1 ∈ F (q 1 , u 1 ) such that

The transition system Σ is said to be input-state monotone (ISM) if it is both LISM and UISM.

Similar to the case of SM transition systems, the concepts of UISM and LISM coincide when the transition system Σ is deterministic.

Characterization of Monotone Transition Systems

In this section, we provide a criterion allowing us to verify if a transition system is a lower or upper (input-)state monotone. Let us characterize lower (input-)state monotone transition systems only while keeping in mind that

.2: Illustration of Theorem 5.2.1. Given two states q 1 Q q 2 and two inputs u 1 U u 2 , if the transition system is LISM then we have that F (q 1 , u 1 ) ⊆↓ F (q 2 , u 2 ).

analogous results hold for upper (input-)state monotone transition systems as well. We start with an auxiliary lemma.

Lemma 5.2.1. Let L be a partially ordered set and A, B ⊆ L. The set A is included in the lower closure of the set

The proof follows immediately from the fact that for any set B ⊆ L we have

Theorem 5.2.1. For a transition system Σ = (Q, U, F ) the following statements are equivalent:

(i) Σ is a LISM transition system;

(ii) for all q 1 , q 2 ∈ Q, for all u 2 ∈ Enab F (q 2 ), u 1 ∈ U if q 1 Q q 2 and u 1 U u 2 , then u 1 ∈ Enab F (q 1 ) and

) and for any q 1 ∈ F (q 1 , u 1 ), there exists

A graphical representation of the conditions in Theorem 5.2.1 is provided in Figure 5.2. We then have the following corollary for LSM transition systems.

Corollary 5.2.1. For a system Σ = (Q, U, F ) the following statements are equivalent:

(i) Σ is a LSM transition system;

(ii) for all q 1 , q 2 ∈ Q, for all u ∈ Enab F (q 2 ) if q 1 Q q 2 , then u ∈ Enab F (q 1 ) and F (q 1 , u) ⊆↓ F (q 2 , u);

Box abstraction

In this part, we discuss a special class of symbolic models Σ B = (Q, U, F ), preserving the monotonicity property of the original (input-) state monotone system

First of all, we over-approximate the compact set W by a finite union of multi-dimensional intervals

Then, we introduce a partitioning Q on R nx . We say that a state q ∈ Q belongs to a safe set Q S ⊂ Q if and only if q ⊂ Y , otherwise the state q is unsafe, i.e., q ∈ Q U S = Q \ Q S . We assume that with introduced partitioning, the set Q S is a finite set. Moreover, it is supposed that the partitioning Q is grid-aligned, i.e. each element q ∈ Q is described as a multi-dimensional semi-intervals q = [x q 1 , x q 2 ). Choosing the set of admissible abstract inputs, as follows U = {u 1 , . . . , u m } ⊆ U we then use reachability analysis techniques to compute the transition relation F .

Then from Definitions 5.1.2,5.1.3 for the reachable set corresponding to an initial set q = [x q 1 , x q 2 ), and a constant control function u : T → u, u ∈ U the following is satisfied

where for all m = 1 . . . M functions w m 1 , w m 2 are constant disturbances with values w m 1 , w m 2 correspondingly.

Let for all q ∈ Q S , for all u ∈ U transition (q, u, q ) ∈ F if and only if q ∈ Q S , u ∈ U, q ∈ Q, the intersection

and for all t ∈ [0, τ ] the condition of a collision avoidance

Where u is a constant control function with value u, functions w m 1 , w m 2 are constant disturbances with values w m 1 , w m 2 correspondingly, τ is a fixed time sampling parameter. We illustrate the construction of the transitions for the box abstraction in Figure 5.4. Taking into account the remark 5.2.1, we may conclude that the constructed

feed-back refinement relation [START_REF] Reissig | Feedback refinement relations for the synthesis of symbolic controllers[END_REF], and a safety controller synthesised for Σ B = (Q, U, F ), can be refined to solve the Problem 1.1.1. However, to increase the efficiency of the synthesis procedure, we are interested in preserving monotonicity of the original system while constructing Σ B = (Q, U, F ). Let us make some additional assumptions about partitioning Q S .

Assumption 5.2.1. Let for all q, q ∈ Q if there exists (x, x ) ∈ q × q satisfying x R nx x , then x q 2 R nx x q 2 . specification Q S . Similarly, if Q S is an upper-closed safety specification, then the maximal safety controller CB for the box abstraction Σ B = (Q, U, F ) and the safety specification Q S coincides with the maximal safety controller CLS for the lower-sparse abstraction Σ LS = (Q, U, F LS ) and the safety specification Q S .

Proof. We only provide a proof for the case of lower-closed safety specifications, the case of upper-closed safety specifications can be derived similarly. Let us show that CB is a safety controller for Σ U S = (Q, U, F U S ). Indeed, since CB is a safety controller for Σ B it is obvious that Dom( CB ) ⊆ Q S . Let q ∈ Dom( CB ), then for all u ∈ CB (q) the following is satisfied F U S (q, u) ⊆ F (q, u) ⊆ Dom( CB ). Hence, CB is a safety controller for Σ U S = (Q, U, F U S ) and safe set Q S . Then, from the definition of maximal safety controller one has CB (q) ⊆ CUS (q) for all q ∈ Q.

Let us show that CUS is a safety controller for Σ B = (Q, U, F ). Again, it is obvious, that Dom( CUS ) ⊂ Q S . Let q ∈ Dom( CUS ), u ∈ CUS (q) and let q ∈ F (q, u). Then there exists q ∈ F U S (q, u) = max(F (q, u)) such that q Q q .

Since F U S (q, u) ⊆ Dom( CUS ) we have that q ∈ Dom( CUS ). Moreover, since the safe set Q S is lower-closed, we have from Proposition 5.3.1 that Dom( CUS ) is lower-closed and one we get that q ∈ Dom( CUS ). Hence, CUS is a safety controller for Σ B = (Q, U, F ) and from the maximality of the controller CB , one has CUS (q) ⊆ CB (q) for all q ∈ Q.

We then have the following corollary for SM systems. Intuitively, the result of Proposition 5.2.3 shows that we can use sparse abstractions instead of box abstraction while working with (input-) state monotone systems and directed specifications.

Maximal Safety Controller for Monotone Transition Systems and Directed Specifications

Considering a system Σ = (Q, U, F ) and a safety specification Q S ⊆ Q, we solve, in this section, a synthesis problem that consists in determining a controller, which keeps the trajectories of the system inside a safe set Q S . for q ∈ B do 10 p(q) := p(q) -1;

We focus on the case when Σ = (Q, U, F ) is a lower or upper (input-)state monotone, and a safety specification is directed. To synthesize the maximal safety controller [Tabuada, 2009]one can use the classical synthesis Algorithm 5.1 (repeats Algorithm 2.1 from Chapter 2), where the function p : Q → {0, 1} indicates whether a state q ∈ Q is controllable (p(q) = 1) or not (p(q) = 0) and the reduced transition relation F p is defined as follows: (q, u, q ) ∈ F p if and only if p(q) = 0 and for all q ∈ F (q, u) the equality p(q ) = 0 is satisfied. However, the classical approach is too source-demanding for many real-world problem. This section provides a more efficient lazy synthesis approach, benefiting from the particular structure of Σ = (Q, U, F ) and Q S .

Lower-closed and Upper-closed Sets

Let us use operators max and min (see Definition 5.2.3) to introduce the notion of the basis for finite lower-closed and upper-closed sets [START_REF] Finkel | Well-structured transition systems everywhere![END_REF].

Definition 5.3.1. Let L be a finite partially ordered set. Let A ⊆ L be a lower-closed (upper-closed) set. A set

The basis of a lower-closed (upper-closed) set can be used for its simpler representation. Indeed, let A is lowerclosed (upper-closed) set and let B = Bas(A), then A = i=1,...,N ↓ a i (A = i=1,...,N ↑ a i ) and for all a i , a j ∈ B, if a i = a j then (a i , a j ) ∈ Inc L . The existence and uniqueness of a finite basis for a finite lower-closed (upper-closed) set follow from the fact that the relation L is a well-quasi-order [Higman, 1952]. An illustration of the concept of basis is given in Figure 5.5.

In the following two subsections, we consider a safety control problem for (input-)state monotone transitions system with directed safety specifications. We show that in a particular case when the transition system is lower Algorithm 5.4: Pre(A, u, B)

Input: A LSM transition system Σ = (Q, U, F ), lower-closed sets A, B ⊆ Q, and an input u ⊆ U . Output: Bas(Pre(A, u, B))

that all states in Q E are safely controllable.

Maximal Safety Controller

Once Dom( C) controller is obtained, we can use the notion of u-predecessors of a set to compute the maximal safety controller C. Definition 5.3.2. For a transition system Σ = (Q, U, F ), sets A, B ⊆ Q and input u ∈ U , we define the set Pre(A, u, B) of u-predecessors of a set B included in a set A, as follows Pre(A, u, B) = {q ∈ A | F (q, u) ⊆ B} Let us now enumerate all inputs in U and introduce the sets Z i = Pre(Dom( C), u i , Dom( C)) for all u i ∈ U, i = 1, . . . , card(U ), where card(U ) denotes the cardinality of the finite set U . Then the following result holds.

Theorem 5.3.2. Let C be the maximal safety controller for a LSM transition system Σ = (Q, U, F ) and lower-closed safety specification Q S ⊆ Q. Then for all u i ∈ U, i = 1, . . . , card(U ) the input u i ∈ C(q) if and only if q ∈ Z i .

Proof. Indeed, the fact that u i ∈ C(q) is equivalent to q ∈ Dom( C) and F (q, u i ) ∈ Dom( C), which is equivalent to

In the classical approach, to find Pre(A, u, B) we should check for every state q ∈ A if the set F (q, u) ⊆ B.

However, the following result provides guidelines towards a more efficient computation of the Pre(A, u, B) in case when Σ = (Q, U, F ) is a SM transition system, and sets A, B are lower-closed.

Theorem 5.3.3. Let Σ = (Q, U, F ) be a SM transition system, and sets A, B are lower-closed. Then the set Pre(A, u, B) is also lower-closed. Moreover, for any lower-closed set D ⊆ A the following holds: D ⊆ Pre(A, u, B) if and only if for all q ∈ Bas(D) the set F (q, u) ⊆ B.

Proof. Indeed, if q ∈ Pre(A, u, B) then q ∈ A and F (q, u) ⊆ B. Let q ≤ Q q. Since A is a lower-closed set, then q ∈ A. Moreover, we have from Corollary 5.2.1 that F (q , u) ⊆↓ F (q, u) ⊆↓ B = B. Hence, q ∈ Pre(A, u, B) and Pre(A, u, B) =↓ Pre(A, u, B).

greater than any state from Q C were already explored and marked with uncontrollable. Hence, the set Pre(A, u, B) coincides with the set ↓ Q C and Bas(Pre(A, u, B)) = Q C .

In Algorithm 5.4, we leave all elements, which are smaller than the basis of Pre(A, u, B), unexplored. So, we go through all states in A only if Pre(A, u, B) is empty. This laziness gives us a gain in efficiency while computing the maximal safety controller. Indeed, in classical synthesis approach where one explores all the states in Q S and all the inputs U , in our approach, all inputs are explored, but not necessarily all the states. Figure 5.7 illustrates the lazy synthesis of maximal safety controller for a simple transition system, such that it input set U = {u 1 , u 2 }. Given Dom( C) by Algorithm 5.3 we then compute two sets Z 1 = P re(Dom( C), u 1 , Dom( C)) and Z 2 = P re(Dom( C), u 2 , Dom( C)) using the Algorithm 5.4. At every iteration of the loop 3-7 we check if a state q ∈ Q E is controllable with u i . If yes, we

The right figure illustrates the result of Theorem 5.3.2, i.e. u i ∈ C(q) if and only if q ∈ Z i .

Lazy Synthesis for Input-State Monotone Transition Systems

In this part, we propose a lazy safety synthesis algorithm that exploits ordering not only on the state, but also on the input space. The synthesis of the maximal safety controller is done in two steps. First, we use only inputs with lower priorities to compute the maximal safety controller's domain Dom( C). Then we synthesize the maximal controller by exploiting the inputs priorities, making it possible to compute the maximal safety controller without exploring all the inputs. We start by providing some characterizations of the maximal safety controller for LISM transition systems.

Proposition 5.3.1. Consider a LISM transition system Σ = (Q, U, F ). Let C be the maximal safety controller enforcing the lower-closed safety specification Q S ⊆ Q. The following properties hold:

(i) Dom( C) is lower-closed with respect to the partial order Q ;

(ii) for all q 1 , q 2 ∈ Q, if q 1 Q q 2 then C(q 2 ) ⊆ C(q 1 );

(iii) for all q ∈ Q, C(q) is a lower-closed set with respect to the partial order U ;

Proof. (i), (ii) The result follows immediately from Corollary 5.3.1 and Corollary 5.3.2 and the fact that any LISM transition system is a LSM transition system.

(iii) Let q ∈ Q, u ∈ C(q) and u ∈↓ u. We have that F (q, u ) ⊆↓ F (q, u) ⊆↓ Dom( C) = Dom( C), where the first inclusion comes from the fact that Σ is a LISM transition system, the second inclusion comes from the fact that C is a safety controller and the last equality comes from the lower-closedness of Dom( C). Hence, we have

Domain of the controller

Let us define the set U min = min(U ) with respect to partial order U on the input set U . Then the following is true.

(1, 1) Proof. Let us define the controller C r of the reduced transition system Σ r and the safe set Q S as follows: for

follows immediately from the construction of the controller C r . Now let q ∈ Dom( C) and let u ∈ C(q). From (iii) in Proposition 5.3.1 we have that ↓ u ⊆ C(q), then there exists u ∈ U min such that u ∈ C(q). Then, u ∈ C r (q). Hence, q ∈ Dom(C r ) and Dom(C r ) = Dom( C) and C r is a safety controller for Σ r with a specification Q S . Now let us prove that for all q ∈ Q, C r (q) = C * r (q). The first inclusion C r (q) ⊆ C * r (q) follows from maximality of the controller

For the second inclusion, we have from maximality of C and since U min ⊆ U that C * r (q) ⊆ C(q) for all q ∈ Q.

Moreover, by construction of C * r , we have that C * r (q) ⊆ U min for all q ∈ Q. Then, C r (q) = C * r (q) for all q ∈ Q. Since

The previous result states that for computation of the domain of the maximal safety controller Dom( C), it is sufficient to use inputs with lower priorities.

Maximal safety controller

It is always possible to reorder the elements of the input set U = {u 1 , . . . , u N } as follows: for all 1 ≤ j ≤ i ≤ N we suppose that either u j U u i or (u i , u j ) ∈ Inc U (see Fig. 5.8 for the illustration). In this section, we exploit such an order to make synthesis for LISM transition systems more efficient. Algorithm 5.5 is based on the fact, that if a state is uncontrollable with an input u ∈ U , it is also uncontrollable with all the inputs u ∈ U such that u > U u, so if we failed to control a state with u, we do not need to explore u > U u for it. Let us now formally prove the result.

Algorithm 5.5: Maximal Safety Controller

Input: LISM transition system Σ = (Q, U, F ), the domain of maximal safety controller Dom( C).

Output:

Proof. To prove the result, we proceed by induction. For all i such that u i ∈ U min the statement is obvious and we have the base. Let i be such that u i / ∈ U min . Suppose that for all j < i, Z j = K j , and let us prove that

Indeed, since for all j < i, K j = Z j we have that K j ⊆ Dom( C) for all j < i, and as a consequence

From where K i ⊆ Z i is immediately satisfied. At the same time, for all q ∈ Z i we have that q ∈ Dom( C) and F (q, u i ) ⊆ Dom( C). Then from Proposition 5.3.1 we have that q ∈ Dom( C) and for all u j ≺ U u i , F (q, u j ) ⊆ Dom( C). Consequently q ∈ Pre(Dom( C), u j , Dom( C)) = Z j = K j for all j such that u j ≺ U u i . Then from the line 9 of Algorithm 5.5, we have that q ∈ S i and, as a consequence, from line 10, q ∈ K i .

Theorem 5.3.5. Let Σ = (Q, U, F ) be a LISM transition system and let Dom( C) be a domain of the maximal safety controller C for a lower-closed safety specification Q S ⊆ Q. Algorithm 5.5 returns the maximal safety controller C.

Proof. The statement follows immediately from Lemma 5.3.2, Theorem 5.3.2 and the fact that u i ∈ C(s) if and only if s ∈ K i (see lines 11-12 of the Algorithm 5.5).

Remark 5.3.1. In the case of a total order 1 on the input set U , the set K i ⊆ K j for all N ≥ j ≥ i ≥ 1 (see Fig. 5.9).

For LISM transition systems and directed safety specifications, one can use the monotonicity property to represent the maximal safety controller C efficiently. Indeed, we have from Proposition 5.3.1 that for a controllable state q ∈ Dom( C), C(q) is a lower-closed set. Hence, for the state q, instead of storing all the admissible control inputs u ∈ C(q), one can only store the elements of the basis of C(q). The latter significantly reduces the amount of

.9: Illustration of the maximal safety controller C for the case of a total order on the input set.

memory required to store the controller. Hence, instead of providing the maximal safety controller C, in practice, we provide the maximal input-lazy controller. However, we can reconstruct MS controller from MILS controller without any computations in a particular case of LISM systems.

Controller Synthesis for Intersections of Directed Safety Specifications

In the previous sections, we have presented lazy synthesis algorithms to deal with lower (input-)state monotone transitions systems and lower-closed safety specifications. Following the duality between upper and lower-closed sets, similar results for upper-closed safety specifications can be obtained using the same approaches.

This part aims to deal with more complex specifications described as intersections of upper and lower-closed sets. Let us mention that from Proposition 5.1.1, the intersection of lower (respectively upper) closed sets is again a lower (respectively upper) closed set. Hence, one can use the same approaches presented in the previous sections to deal with unions of lower (respectively upper) closed specifications.

In this section, we focus on the synthesis of controllers for the intersection of an upper and lower-closed set, which is a natural specification appearing in many applications such as vehicle platoons [START_REF] Nilsson | Correct-by-Construction Adaptive Cruise Control: Two Approaches[END_REF], microgrids [START_REF] Zonetti | A symbolic approach to voltage stability and power sharing in time-varying DC microgrids[END_REF], traffic networks [START_REF] Coogan | Traffic network control from temporal logic specifications[END_REF] and temperature regulation [START_REF] Meyer | Controllability and invariance of monotone systems for robust ventilation automation in buildings[END_REF].

The considered setup is the following. Given a (input-)state monotone transition system Σ = (Q, U, F ), a lower-

Let us define the following safety controllers:

• CLU is the maximal safety controller for the transition system Σ and the safety specification

Numerical Illustration: Adaptive Cruise Control

In this Chapter we again consider two vehicles moving along a straight road. Each vehicle is modeled as a point mass m with velocity changing according to the law

(5.4)

In the equation above, F represents a net action of braking and engine torque applied to the wheels, while the second term f 0 + f 1 v + f 2 v 2 describes aerodynamic and rolling resistance effects. In simulations

The net force F is viewed as a control input u for the follower vehicle and a disturbance for the lead one. It is assumed to be bounded by F min = -0.3mg ≤ F ≤ 0.2mg = F max , where g is a gravitational constant. Such a bound is consistent with non-emergency braking and acceleration. We slightly adapt equation (5.4) to prohibit a back motion for the follower:

(5.5)

For the leader we assume that its velocity w remains in a range [0, w max ]:

Combining (5.5) and (5.6) with the equation (5.7) which describes the distance between two vehicles, we obtain the final model of the system.

Control Objective and Numerical Results

Lower-closed Safety Specification

We start with the objective to synthesize a controller for the follower vehicle, to keep its velocity below v max = 30 m/s and to guarantee that the relative distance between the leader and the follower remains larger than d min = 10 m, while assuming that the leader car acts as a disturbance a ∈ [F min , F max ] and w max = 30 m/s. The following change of coordinates: h = -d, z = -w transform the system (5.5)-(5.7) into a monotone one. Moreover, after this change adaptive time-sampling technique. Unlike existing approaches, where transitions duration was determined with a given parameter, we proposed interrupting every transition before leaving the abstract state neighborhood. We then use Algorithm 2.2 to synthesize the maximal safety controller lazily by iteratively exploring only those states that border the uncontrollable domain. We also showed that one could restrict computations to the boundary states, even when abstraction is not neighbor-linked. Indeed, with a novel control refinement scheme that interrupts the closed-loop trajectory of the original system when it reaches a boundary state of the controllable domain, we can guarantee that the closed-loop trajectory of the original system does not overjump the boundary. And since for every boundary state, we have an abstract input that pushes the system back towards the interior, a safety behavior is ensured. Though the gain efficiency of the proposed lazy synthesis approach was not overwhelming, the idea to explore only boundary states still deserves to be part of others lazy synthesis approaches, for example, when we are dealing with multi-scale abstractions as in Chapter 4.

Chapter 4 showed how to reduce the size of the symbolic models by using abstractions with adaptive grids. The main idea is to start with a coarse partitioning on the state space and then locally refine it in uncontrollable areas.

We also used multi-scale time-sampling prioritizing transitions with a longer duration. We then benefit from a partial order on the input set U and the fact that the initial set Q init ⊂ Q is known to synthesize the maximal lazy safety controller C * . The term maximal comes from the fact that all safety controllable initial states are in Dom(C * ), and if the controller enables an input, it also enables all inputs which have the same priority and preserve safety. The term lazy refers to the fact that the controller enables only the most prioritized inputs among actions that maintain safety. Hence, C * represents a trade-off between maximal permissiveness and efficiency. Such a controller was first considered [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF], but the synthesis procedure was restricted to a deterministic transition system.

We merged Algorithm 2.3 and Algorithm 2.4 to provide a procedure applicable for non-deterministic abstractions as well. Usage of multi-scale abstractions with an adaptive grid showed a good performance since it allows the construction of accurate symbolic models with less computational effort. However, manipulation with adaptive grids requires more complex data structures (graphs, binary decision diagrams etc.) than simple matrices. The latter motivated us to use C++ instead of Matlab for the implementations.

Chapter 5 was devoted to monotone control systems and specifications given by directed sets. We first considered two classes of control systems: state monotone or input-state monotone dynamical systems. We then showed that an abstraction inherits monotonicity only if the state-space partitioning satisfies some restrictions. We distinguished lower and upper (input-)state monotone transition systems and lower and upper closed safety specifications but focused on lower ones due to symmetry of results. A finite lower-closed set can be represented by its basis.

And we proved that to compute the controllable domain, it is enough to explore only basis states. Moreover, it is sufficient to use inputs with lower priorities for lower input-state monotone transition systems. We then provided two algorithms for lazily computing the maximal safety controller for lower (input-)state monotone transition systems.

These algorithms benefit from the fact that for a lower state-monotone system, if a state q is controllable with an Appendix A

Reachability Analysis for Mixed-monotone

Dynamic Systems

The results of this Appendix were originally presented in [START_REF] Yang | On sufficient conditions for mixed monotonicity[END_REF] and provided here to ease the reading of the main part of the manuscript.

Consider a nonlinear system of the following type: The notation L([t, τ ], S) is used for the space of all measurable on [t, τ ] functions s, such that s(p) ∈ S, p ∈ [t, τ ] almost everywhere.

Let x f (t | x(0), û, ŵ) denote a trajectory of the system (1.1) satisfying the initial condition x(0) = x and corresponding to a given control û and a disturbance ŵ. Finally, let Reach(t |, X 0 , û) denote the robust reachable set, corresponding to a given control û, i.e.

Reach(t |, X 0 , û) = {x ∈ R nx | ∃ x 0 ∈ X 0 , ∃ w ∈ W(0, t), such that x f (t | x 0 , û, w) = x}.

Computation of the exact reachable set for nonlinear dynamic systems is an intractable problem in the general case, and, in practice, their over-approximations are sought after.