Facing the frightening Covid-19 pandemic, temptation to use unproven medications is great. Nevertheless, whatever the emergency, it is critical to develop relevant scientific approaches, namely through randomized trials. Surprisingly and unusually, the New England Journal of Medicine published data from a compassionate use of remdesivir for patients with severe Covid-19. [START_REF] Grein | Compassionate use of remdesivir for patients with severe covid-19[END_REF] From a medical point of view, it is understandable to attempt to provide a possibly effective treatment in severely ill individuals but organizing the systematic dispensation of experimental treatment outside a well-designed protocol is more disputable.

The scientific and medical relevance of single-arm studies are limited and we will not list here all methodological limitations that the interpretation of such studies is faced. In the "study" cited above, it seems that the inclusion process was in part managed by the drug provider with unclear criteria. Given the world-wide distribution of patients, not considering the heterogeneity of medical practices is also an important bias. Highlighting the reduction of mortality on the basis of a debatable external comparison also raises question while the right choice of such comparator is probably the only way to provide results' credibility. [START_REF] Cucherat | From single-arm studies to externally controlled studies. Methodological considerations and guidelines[END_REF] While present data are important to consider when developing new hypotheses, their wide dissemination may contribute to confusion among the general public, as was recently the case from similar studies with hydroxychloroquine. Thus, the present data mainly provide a signal for a hypothetic remdesivir repurposing rather than to demonstrate its benefit for the treatment of Covid-19 patients.

The real hope for Covid-19 treatment is elsewhere. Despite the epidemic situation, a real control group remains crucial. One concern, is whether it is ethical or not to give patients a placebo. Because the disease is not 100% lethal, it remains ethical to conduct randomized studies using placebo arm. [START_REF] Kalil | Treating COVID-19-Off-Label Drug Use, Compassionate Use, and Randomized Clinical Trials During Pandemics[END_REF] From the beginning of January 2020, an exponential number of clinical trials have been developed mainly randomizedtrials exploring a large variety of drugs or treatment procedures (Figure 1A). Among the top ten drugs or procedures evaluated, an impressive number of studies concern hydroxychloroquine in various populations. Several trials are also testing a multiplicity of antivirals including remdesivir but more original approaches such as cell therapies are also developed (Figure 1B). Because some of these trials have an adaptive design that may help to early detect a beneficial or deleterious effect of drugs, it is urgent to wait their results before to disseminate data on possible inappropriate use of treatments.

Dominique DEPLANQUE Professor of medical Pharmacology

Univ. Lille, Inserm, CHU Lille, CIC 1403 -Clinical Investigation Center, F-59000 Lille, France dominique.deplanque@univ-lille.fr

Figure 1 .

 1 Figure 1. Interventional studies to fight Covid-19 since January 2020 In the Figure 1A, are represented the interventional studies (randomized or not) declared on clinicaltrial.gov from the beginning of January to April 14 th 2020. Figure 1B illustrates the number of randomized trials declared according to the Top 10 drugs used in the same period.

Randomized trials are the real hope for Covid-


Thomas Morzadec

Damien Marchal

Christian Duriez

Toward Shape Optimization of Soft Robots

In this paper we present our work on shape optimization for soft robotics where the shape is optimized for a given soft robot usage. To obtain a parametric optimization with a reduced number of parameters, we rely on an approach where the designer progressively refines the parameter space and the fitness function until a satisfactory design is obtained. In our approach, we automatically generate FEM simulations of the soft robot and its environment to evaluate a fitness function while checking the consistency of the solution. Finally, we have coupled our framework to an evolutionary optimization algorithm, and demonstrated its use for optimizing the design of a deformable leg of a locomotive robot.

I. INTRODUCTION

Designing a soft robot is a challenging task. Compared to rigid robotics, a first difficulty is that the kinematics of soft robots is not intuitive or well-understood, complicating the design process. A second difficulty with soft robotics is that softness can be achieved with various soft materials like silicone [START_REF] Tolley | A resilient, untethered soft robot[END_REF], [START_REF] Martinez | Robotic tentacles with three-dimensional mobility based on flexible elastomers[END_REF] micro-structured materials [START_REF] Schumacher | Microstructures to control elasticity in 3d printing[END_REF] or specifically designed geometrical arrangement of rigid parts as with tensegrity structures [START_REF] Caluwaerts | Design and control of compliant tensegrity robots through simulation and hardware validation[END_REF], allowing a wide range of variations in design. Combined with the recent developments of 3D printing, new possibilities of manufacturing materials have appeared, allowing the fabrication of deformable objects exhibiting complex deformation kinematics by controlling the in-fill [START_REF] Chen | Synthesis of filigrees for digital fabrication[END_REF], [START_REF] Wu | Infill optimization for additive manufacturing -approaching bone-like porous structures[END_REF].

In addition to the material itself, actuation systems are very diverse with approaches including cables [START_REF] Hassan | Design and development of a bio-inspired, under-actuated soft gripper[END_REF], pneumatics [START_REF] Shepherd | Multigait soft robot[END_REF], [START_REF] Martinez | Elastomeric origami: Programmable paperelastomer composites as pneumatic actuators[END_REF], shape memory alloys [START_REF] Villanueva | A biomimetic robotic jellyfish (robojelly) actuated by shape memory alloy composite actuators[END_REF] or chemical reaction [START_REF] Mosadegh | Pneumatic networks for soft robotics that actuate rapidly[END_REF]. Any subtle change in the geometry, the choice of material as well as the actuators' or sensors' positions may impact the deformation behavior and thus the overall robot's kinematics. In addition, soft robotics is a recent field of research where researchers are still actively exploring robot designs and their usages but there is a lack of established know-how to design soft robots. Thus, there is dire need of assistance tools to help designers. Some tools, like SOFA [START_REF] Faure | Sofa: A multimodel framework for interactive physical simulation[END_REF] and its SoftRobots plugins, allow modelling, simulation and control of soft robots [START_REF] Coevoet | Software toolkit for modeling, simulation and control of soft robots[END_REF]. The framework contains FEM based simulation of deformable material, deformable inverse kinematics, contact modelling and model order reduction. It has been used to model and control a large variety of soft robots. This framework allows the designers to simulate the physical behavior of the robots before their actual fabrication. It is far from straightforward for a designer to understand how to adapt the shape of the robot to satisfy some targeted

1 INRIA, 2 CNRS
capabilities, resulting in a trial-and-error approach to develop and test alternative designs.

In the present paper we introduce our work on a shape optimization toolkit in SOFA and the results of our experiments done by numerical simulation as well as their comparison to a physical bench test.

II. RELATED WORK

From a mathematical point of view, shape optimization consists in minimizing a function φ defined on the space of subsets of a bounded domain of R 2 or R 3 (i.e. the shapes) with values in R (i.e. the fitness of the shape). Shape optimization is an active field of research with multiple applications: mechanical design [START_REF] Allaire | Conception optimale de structures[END_REF], shape modelling, 3D printing [START_REF] Wu | Infill optimization for additive manufacturing -approaching bone-like porous structures[END_REF] or robotics [START_REF] Zhang | Design and development of a soft gripper with topology optimization[END_REF], [START_REF] Cheney | Evolving soft robots in tight spaces[END_REF]. With the development of 3D printing, shape optimization has been applied to the creation of in-filled structures [START_REF] Chen | Synthesis of filigrees for digital fabrication[END_REF] or surface patterns [START_REF] Wu | Infill optimization for additive manufacturing -approaching bone-like porous structures[END_REF] which exhibit custom mechanical behavior. In work [START_REF] Prévost | Make It Stand: Balancing shapes for 3D fabrication[END_REF] optimization techniques were used to design complete mechanisms that can be built. In [START_REF] Megaro | Designing cable-driven actuation networks for kinematic chains and trees[END_REF], the authors provide co-design tools to help design cable-driven kinematic chains and trees for animatronics.

Methods based on partial differential equations, like level set methods (see for example [START_REF] Osher | Level Set Methods and Dynamic Implicit Surfaces[END_REF]), are commonly used to morph a shape in an externally generated velocity field. These methods can perform shape optimization if the velocity field is obtained, for example, from the shape derivative of the fitness function (see [START_REF] Henrot | Shape Variation and Optimization: A Geometrical Analysis[END_REF]). But sometimes, there is no access to derivatives and optimization is based on the evaluation of the fitness function φ itself. Other optimization methods, like evolutionary strategies, can be used in such a case. The calculation of derivatives is replaced by the evaluation of not only one but a population of a few shapes [START_REF] Bernardoni | A new compliant mechanism design methodology based on flexible building blocks[END_REF].

In robotics, evolutionary approaches aim at the emergence of complex mechanical behavior in embodied behavioral agents. The approach is named Embodied Evolution [START_REF] Ficici | Embodied evolution: A response to challenges in evolutionary robotics[END_REF]. In particular, the performance of the mechanical design of the "embodied agent" (the robot) in interaction with its environment is optimized. It is also referred as Morphological Evolution. This approach has been applied to soft robotics in [START_REF] Cheney | Unshackling evolution: Evolving soft robots with multiple materials and a powerful generative encoding[END_REF], where the shape and the distribution of artificial muscles are optimized to make locomotion emerge. A population of individuals is set and evolves, according to their evaluation using a voxel-based mechanical simulation. The shape is encoded with Compositional Pattern Producing Networks (CPPN) and the evaluation is made with the software Voxelyze [START_REF] Hiller | Dynamic Simulation of Soft Multimaterial 3D-Printed Objects[END_REF]. In [START_REF] Cheney | Evolving soft robots in tight spaces[END_REF], the same authors added interaction between the robot and its environment. On the other hand, the evaluation of shapes or mechanical objects can also be based on a physical bench test without the need of a model [START_REF] Brodbeck | Morphological evolution of physical robots through model-free phenotype development[END_REF]. This has the main advantage of avoiding the pitfalls of simulations. Since the fabrication of large population of candidate robots is still a time-consuming process, authors proposed to automate the fabrication and testing as in [START_REF] Rieffel | Evofab: A fully embodied evolutionary fabricator[END_REF].

These methods seek the optimization algorithm or the evolutionary process to provide new design ideas. The search space is quite big (in particular when evaluation is made by simulation) and the designer may not impose precise constraints on it. The situation could be the opposite: the designer could have the global idea of the soft robot to be designed. In such a case, the optimization is still useful to adapt the robot's body shape to specific constraints or to optimize some behaviors.

The contribution of this work is to provide one solution for this situation with an approach in which the designer is able to define the space of shapes and explore it with a reduced number of parameters.

III. SHAPE OPTIMIZATION

The starting point of our approach is that, given a soft robot design within its operational environment we want to explore alternative designs as well as optimize some of its properties. We use a black-box optimization technique that does not require the objective function to be continuous or differentiable. In practice, the optimization relies on the evaluation of this fitness function. This evaluation is done in several steps: the shape is generated out of a set of parameters, then we automatically create a mesh, launch a simulation in SOFA, and finally make an evaluation based on the simulated physics.

A. Shape Modelling

To model the shapes we use procedural modelling based on implicit functions similar to ones we can find in [START_REF] Lefebvre | Icesl : A gpu accelerated modeler and slicer[END_REF]. This approach enables the easy generation of families of complex shapes from a reduced set of parameters. Readers unfamiliar with modelling with function fields may consult [START_REF] Keeter | Hierarchical volumetric object representations for digital fabrication workflows[END_REF]. It contains an overview of the possible shapes defined as field functions, the combining operators to implement Constrcuctive Solid Geometry operations and how to implement geometric deformations and transformations. In addition to field functions, it is useful to incorporate shapes defined by other approaches such as voxel grids or parametric surfaces and curves. This is possible by computing an approximation:

• from a vectorized representation (parametric curve or surface, triangle mesh) ones can get a 2D and 3D grid representation through rasterization. • from a 2D or 3D grid one can compute a distance grid with the fast marching algorithm. • from a 2D or 3D distance grid as input, an interpolating scheme can be used to get a field function. To evaluate a shape we use the Finite Element Method to simulate the mechanical behavior of the robot. The FEM implemented in SOFA expects tetrahedral meshes. We use the CGAL library to convert the implicit function describing the shape to a tetrahedral mesh, pointing out the sharp edges and corners to CGAL, to be sure that they are preserved.

Once this is done a SOFA scene is made which also contains the modelling of the other soft robot's components like the actuators, the sensors as well as its environment.

B. Optimization

The choice of the fitness function is crucial. Describing the main objective will probably not be too difficult for the designer (for example: optimize energy transmission, optimize stiffness or compliance, reduce weight). But it may appear that optimizing a unique objective leads to undesirable side behaviors or to numerical scenes which are more and more eccentric and less and less reliable. Consequently, we need to define some constraints that penalize these undesirable behaviors. The penalization of constraints will be added to the fitness function. The optimization of a fitness function with penalties included in the fitness function is not a multi-level optimization. Multi-level optimization needs specific algorithms. Optimizing a fitness function with penalties works in practice, at least in our example, because we don't try to minimize penalties, but to have them below a given threshold.

Remark: The reliability of a simulation not only depends on the shape, but also on some numerical parameters, such as the size of the mesh or the time step value. These parameters cannot be automatically adapted to every case without a significant cost on the performance, as it would require several evaluations of the same individual. These parameters are thus fixed. We also have an option to test two or three different mesh resolutions for the same case, to obtain an idea of the influence of these parameters. Moreover, some heuristics can detect when a simulated individual is obviously not reliable (inversion of elements, buckling, undesirable self-collision).

In such cases, we can again use a penalization.

To understand the choice of the optimization algorithm, let's focus now on the properties of the problem. We want to minimize a fitness function that can be multimodal, i.e. with many local optimum. It could be ill-conditionned, in particular if parameters are numerous and if penalty constraints are used. Its evaluation can be sometimes very sensitive to the parameters. Finally, the problem is not separable, i.e. the n-dimension function cannot be optimized in a sequence of n independent 1-D optimization processes.

For all these reasons, it appears that the evolutionary strategy called CMA-ES (covariance matrix adaptation evolution strategy) is particularly suited for this kind of complex optimization problem.

IV. EVALUATION ON THE DESIGN OF A SOFT LEG

The legs of the robot are soft legs made of silicone, animated by servo motors. When running, the motor cycles, resulting in compressing and releasing the deformable part of the leg. This release of energy is a very nice property because it helps the leg to support the weight of the robot body when the leg is in extension and results in a more constant torque on the motors during the gait. In practice, we want to design the legs so that they match the capacities of the motors while optimizing the energy accumulation-release property.

Consequently, we have applied our design optimization method to find the shape of the deformable part of the leg. In the following we present the different steps of the method applied on this example. Then, we set up a physical test bench to validate the numerical results.

A. Procedural modelling of the leg

We modelled the Sofia's leg as the extrusion of a 2D profile. The extrusion thickness is fixed. This 2D profile is the difference of two 2D shapes, each defined by splines (one for the external profile of the leg, the other for the inside border of the hole). Each spline is discretized on a grid and then we get the discretized signed distance function from it via a fast marching algorithm. We thus get two (2D) signed distance functions d 1 , d 2 . The 2D-difference is defined by the the function f = max(d 1 , -d 2 ). Finally, the extrusion of thickness e is obtained by the function max(|z -e 2 | -e 2 , f ). In our case, the motor rotates in both directions. Consequently, we impose axial symmetry between the left and right sides (see Figure 2). The splines' control points are procedurally generated allowing the user to decide how many control points to use. In practice, the top and the bottom part of the external spline are fixed, so three pairs of control points are fixed (two for the top, one for the bottom). We tried two configurations: three free pairs for the hole and one for the external spline (four total pairs), or five for the hole and four for the external spline. The pairs of control points are uniformly distributed between two extremities. These extremities are fixed for the external spline but free for the hole.

B. Optimization with design constraints

The optimization is conducted on FEM simulations. We suppose that the shape is attached at its top part. A virtual motor wheel is attached to the bottom of the leg. Note that to perform equivalent tests in simulation and with the experimental set up (see section IV-C), we imposed that the motor rotates slowly. In practice, this leads to underestimation of the damping. At each time step, the relative power and torque provided by the virtual motor are evaluated. The simulation provides the forces applied by the virtual wheel to the leg and the velocities of the attachment points: the torque is the sum of the vector products between the forces and the vectors between the attachment points and the center of the wheel, and the power is the sum of the scalar products between the forces and the velocities of the attachment points. We record the maximal torque, and we integrate the power, separating the positive from the negative part. The "positive" part is the energy provided by the motor to store the potential energy of deformation inside the leg. The "negative" part is the energy released by the leg.

The objective is: given a torque threshold T thr , we want to design a shape such that first, the maximal torque required from the motor does not exceed the torque threshold and second, the amount of released energy is maximized.

1) Fitness function: Let E denotes the amount of released energy and E 0 be its order of magnitude for a reference shape (we chose E 0 = 0.10J because E = 0.40J for the initial shape). Let T thr be the maximum permissible torque, and let T max be the maximum torque provided by the virtual motor.

We have a first fitness function φ 1 = -E E0 and a second expression with the constraint φ 2 = max( Tmax-T thr T thr , 0). Minimizing φ 2 and φ 1 corresponds respectively to T max ≤ T thr and E being maximized. In this formula, E E0 is the term to optimize, and the second term is a penalty: max( Tmax-T thr T thr , 0) = 0 means T max ≤ T thr . We multiply this term by k, so that the penalty is greater than 1 if T max > (1.0 + 1.0/k)T thr . Since diminishing the penalty is much more important than maximizing E/E 0 , in practice we use the fitness function:

φ = φ 1 + (kφ 2 ) 2 .
(1)

Remark: φ 1 and φ 2 are built to be dimension free with the value of φ 1 expected to be between 1 and 10 at convergence, and the values of φ 2 expected to be zero. In practice, we used k = 10 so that the penalty function becomes significant when the maximal torque exceeds the threshold by more than 10%. Thus it is not ensured that the result will strictly respect the threshold. To ensure it, or reduce the margin, the penalty value should be increased but this may prevent the convergence of the optimization.

2) Other penalties: Undesirable side effects may appear while maximizing E. Therefore, we had to refine the fitness function to penalize them. First, to be realistic, we need to take into account self-collisions. However, they are undesirable since they could cause wear to the real leg. We thus add a penalty term in the fitness function penalizing self-collision. At each time step, the normal self-collision forces are added together for that step, and the maximum of these sums is recorded. The self-collisions are thus penalized similarly to the maximal torque, but the threshold is zero. The corresponding penalty function is then added to the function φ. Secondly, it may happen that, when compressed, the leg buckles and leaves the xy-plane. This is penalized too, by comparing the maximal distance of the points in the mesh to the xy-plane, to a threshold, around 20% of the thickness of the leg. Similarly, the corresponding penalty function is added to the function φ.

Finally, as mentioned in Section III, we wanted to identify a "reliability criterion" for the simulation. In practice, we used the total integral of the relative power during the whole rotation. This value should be close to zero as the damping is underestimated (see above) and the integration scheme (semiimplicit Euler) should only lead to small energy loss. But, in practice, if for some reason the scene is not reliable and cannot be correctly simulated, this value is far from zero. In such case, penalization allows the algorithm to reject these shapes from the optimization.

At that point, we can define the fitness function. Let F be the set of our admissible shapes. We defined above a fitness function φ : F → R. The space F is parametrized by the y-coordinates of the pairs of control points, and their distance to the y-axis, for the external and internal splines. In order to resize the parameters, we actually impose bounds to the distances, and the y-coordinates are relatively uniformly distributed between two ends. These ends are fixed for the external spline, but free for the internal one. Thereby, we get a function [0, 1] n → F, where n is related to the number of control points, and consequently a function Φ : [0, 1] n → R, that can be minimized by the CMA-ES algorithm. For this, we have to choose CMA-ES parameters like population size and searching radius, that will not be discussed here.

C. The physical bench test

In order to validate our numerical results, we set up a bench test. Since the motion in the numerical simulation is very slow, in order to underestimate the damping, we first made a quasi-static experiment, evaluating the torque in many positions, to estimate the maximal torque, and check that it is consistent with the numerical evaluation. Readers should note that because of this difference, numerical and physical experiments do not have the same behavior in the video. We used a system of two pulleys with a belt to multiply the maximal torque delivered by the motor. However, it appears that the bench test was not strong enough to actuate the shapes whose maximal torques were supposed to be at least 0.20N.m. The maximal torque is reached during the compression phase of the shape. Unfortunately, we could not reproduce exactly the numerical experiment, because we could not run the motor at a slow constant speed. Consequently, we did not evaluate the energy transfer.

V. RESULTS

We ran several experiments with different maximal torque thresholds. The results are gathered in the following tables. For each experiment, we started from the same initial handmade shape. This initial shape is defined by 4 free pairs of control points. However, the number of control points is constant during the experiment. Thus, in case we want to optimize the shape with 9 pairs of control points, the algorithm first adds some pairs, with very little modification of the shape. The two metrics in our experiments are the maximal torque and the amount of energy released (in cJ and cN.m).

A. Simulation results

In Figure 4 we show the results we obtained when varying the torque threshold and the number of pairs of control points. Numerical results are presented in Table I. From the results, we can see that the torque thresholds are reached. In some (not reported) experiments, it happened that the torque threshold was surpassed, typically by 10%, because the penalty function is such that it becomes greater than 1.0 only when the threshold is surpassed by 10%. Refining the penalty function could correct this bias. We also noticed that the quality of the result is independent of the

B. Bench test results

To get insight on the approach, we tested the shape produced by our algorithm with a physical bench test. As previously mentioned, we did not reproduce the numerical experiment with the bench test, since we were not able to run the motor at a constant slow speed. Instead, we just evaluated the torque in many positions to check the coherency of the measures of maximal torques. Each experiment was repeated a few times, and the extremal measures are reported.

VI. DISCUSSION

Two points of the method and the results need to be discussed.

• The definition of the fitness function obviously has an important impact on the results. It is important to penalize all the constraints to avoid unexpected behaviors. Yet, these constraints are sometimes not obvious at the beginning of the design process. For instance, in our case, we ran several optimizations before getting the final fitness function, in particular because we progressively added new constraints. • One of the good properties of the FEM models is that increasing the mesh resolution converges towards a single solution. However, in the particular case of the leg studied in this article, it happens that the optimal solutions are often around forms, which, when they deform during the imposed motion, are at the limit of self-collision. Then, a small change in mesh resolution can create a self-collision when there was none before, which has a big impact on the fitness function.

VII. CONCLUSION AND FUTURE WORK

In this paper we present our work on soft robot optimization. To make this possible we presented how we model soft robots' shapes using a procedural approach and how this integrates with the simulation framework to evaluate the fitness function of the generated shape.

Several points were raised during the discussion and there are many ways to improve this rather preliminary work. In the future, we plan to integrate tools to facilitate the implementation of formatting functions and to provide a solution to better deal with self-collision cases. In addition, we would like to test the method for more difficult design tasks and therefore further increase the computational requirements. However, it will also be important to keep in mind that in a practical case, it will be necessary for the optimization to be done in reasonable time to actually be used in a design pipeline.

VIII. ACKNOWLEDGEMENT

Fig. 1 .

 1 Fig. 1. The Sofia soft robot

Fig. 2 .

 2 Fig. 2. From left to right. The 2D parametrization. The 2D difference of the two 2D shapes. The resulting extruded shape. The resulting meshed version of the leg.

Fig. 3 .

 3 Fig. 3. The physical bench test. On the right we can see the tested leg and on the left the motor and the force sensor.

Fig. 4 .

 4 Fig. 4. Initial shape (labelled 0) for the optimization and different shapes (labelled 1 to 6) obtained by numerical experiments (see table I)

  Fig. 4. Initial shape (labelled 0) for the optimization and different shapes (labelled 1 to 6) obtained by numerical experiments (see table I)

The authors wish to thank all the members of the DE-FROST team for their support, especially B. Carrez, S. Escaida Navarro, A. Kruszewski, T. Morales Bieze, and M. Thieffry who set up the bench test, and E. Coevoet for IT support, as well as SOFA's developers for their open-source framework. We also thank N. Bredeche for advising us to use CMA-ES, and C. Toure and N. Hansen who helped us to use it. This work has been financed by the Conseil Regional Haut-de-France and by the European Union through the European Regional Development Fund (ERDF).


* Adnane Saoud

Elena Ivanova

Antoine Girard

Efficient Synthesis for Monotone Transition Systems and Directed Safety Specifications

In this paper, we introduce an efficient algorithm for control policy synthesis for monotone transition systems and lower (upper) safety specifications. For a monotone transition system the sets of states and inputs are equipped with partial orders, moreover, the transitions preserve the ordering on the states. We propose a lazy algorithm that exploits priorities on the states and inputs. To compute the maximal controlled invariant set, only inputs with the lowest priorities are used. Then, starting from the states with the highest priorities, transitions are computed on-the-fly and only when a particular region of the state space needs to be explored. Once this set is computed, controller synthesis is straightforward by exploring different inputs and using their priorities. We prove the completeness of our algorithm w.r.t the classical safety algorithm. Finally, we illustrate the advantages of the proposed approach on a vehicle platooning problem.

I. INTRODUCTION

Abstraction-based synthesis techniques have been an ongoing research area in the last decade (see e.g. [START_REF] Tabuada | Verification and control of hybrid systems: a symbolic approach[END_REF], [START_REF] Belta | Formal methods for discrete-time dynamical systems[END_REF] and the references therein). In symbolic control approaches, a discrete abstraction is constructed from the original dynamical system. When the concrete and abstract systems are related by some behavioral relation such as simulation, alternating simulation or their approximate or directed versions, the discrete controller synthesized for the abstraction can be refined into a controller for the original system. The description of a dynamical system as a discrete abstraction principally enables the use of various techniques developed in the area of supervisory control of discrete event systems.

Symbolic models are often obtained through discretization of the state and input spaces. Due to those discretizations, most symbolic approaches do not scale well.

To tackle this problem different approaches have been proposed. In [START_REF] Girard | Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models[END_REF], [START_REF] Hsu | Multi-layered abstraction-based controller synthesis for continuous-time systems[END_REF], abstractions were computed using multi-scale state-space discretization. In [START_REF] Weber | Optimized state space grids for abstractions[END_REF], [START_REF] Saoud | Optimal multirate sampling in symbolic models for incrementally stable switched systems[END_REF] optimal abstraction parameters were derived to minimize the size of symbolic models. The authors in [START_REF] Camara | Safety controller synthesis for switched systems using multi-scale symbolic models[END_REF], [START_REF] Hsu | Lazy abstraction-based control for safety specifications[END_REF], [START_REF] Hussien | Lazy controller synthesis using threevalued abstractions for safety and reachability specifications[END_REF], [START_REF] Kader | Safety controller design for incrementally stable switched systems using event-based symbolic models[END_REF] Other approaches have been developed by using compositional methods for abstraction or for controller synthesis [START_REF] Swikir | From dissipativity theory to compositional synthesis of symbolic models[END_REF], [START_REF] Kim | Constructing control system abstractions from modular components[END_REF], [START_REF] Meyer | Safety control with performance guarantees of cooperative systems using compositional abstractions[END_REF], [START_REF] Saoud | Compositional abstraction-based synthesis for cascade discrete-time control systems[END_REF].

While existing lazy approaches in the literature exploit only priorities on the inputs, in this paper, we also use the priorities 1 on the states to present an efficient synthesis algorithm for monotone transition systems (which are a subclass of transition systems that preserve priorities on the states) and directed safety specifications. The class of monotone transition systems is of practical interest since it arises from monotone dynamical systems, which frequently appears in engineering applications such as traffic networks [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF], biological networks [START_REF] Angeli | Monotone control systems[END_REF] and power systems [START_REF] Zonetti | A symbolic approach to voltage stability and power sharing in time-varying DC microgrids[END_REF]. We show that for the considered problem the maximal controlled invariant is a lower closed set and that it can be computed using only inputs with lower priorities. Then we present an efficient approach to compute the domain of the controller using the concept of basis, which serves as a simpler representation of lower closed sets. Once the maximal controlled invariant is found, we exploit priorities on the inputs to compute the maximal safety controller. Finally, we demonstrate the practicality of our approach on a vehicle platooning problem.

In spirit, the closest works in the literature are [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF], [START_REF] Sadraddini | Safety control of monotone systems with bounded uncertainties[END_REF]. In [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF], sparse abstractions were proposed for monotone dynamical systems and directed specifications. We complement their idea by providing an efficient synthesis algorithm for directed safety specifications. In [START_REF] Sadraddini | Safety control of monotone systems with bounded uncertainties[END_REF], the authors compute controlled invariants for monotone systems using constraint programming. Their notion of s-sequence is relatively close to the characterization of lower closed controlled invariants presented in our work. In this paper, we only focus on lower safety specification, but the results for upper safety specifications can be obtained using the same approach.

The paper is organized as follows. In Section II, some required preliminaries are provided. In Section III, we introduce the class of monotone transition systems. In Section IV, we present an efficient synthesis algorithm for monotone transition systems and lower safety specifications. Finally, in Section V, an illustrative example is proposed in order to show the efficiency of the proposed approach.

II. PRELIMINARIES

A. Partial orders

A binary relation ≤ L ⊆ L × L is a partial order if and only if for all l 1 , l 2 , l 3 ∈ L we have:

(i) l 1 ≤ L l 1 , (ii) if l 1 ≤ L l 2 and l 2 ≤ L l 1 then l 1 = l 2 and, (iii) if l 1 ≤ L l 2 and l 2 ≤ L l 3 then l 1 ≤ L l 3 . If neither l 1 ≤ L l 2 nor l 2 ≤ L l 1
holds, we say that l 1 and l 2 are incomparable. The set of all incomparable couples in L is denoted by Inc L . We define

≥ L so that l 1 ≥ L l 2 if and only if l 2 ≤ L l 1 . For a partially ordered set L, half closed-open intervals are (x, y] L = {z | x < L z ≤ L y}. Given a partially ordered set L, for a ∈ L let ↓ a = {x ∈ L | x ≤ L a} and ↑ a = {x ∈ L | a ≤ L x}. When A ⊆ L then its lower closure is ↓ A = a∈A ↓ a. A subset A ⊆ L is said to be lower closed if ↓ A = A.

B. Transition systems

Definition 1:

A transition system is a tuple S = (X, X 0 , U, ∆, Y, H) where X is a set of states, X 0 ⊆ X is a set of initial states, U is a set of inputs, ∆ ⊆ X × U × X is a transition relation, Y is a set of outputs, and H : X → Y is an injective output map.
A transition system is said to be finite if X and U are finite. We introduce notation x ∈ ∆(x, u) as an alternative representation for a transition (x, u, x ) ∈ ∆, where state x is called a u-successor of state x, for input u ∈ U . This notion could be generalized toward sets in the natural way: for A ⊆ X and W ⊆ U , ∆(A, W ) = a∈A u∈W ∆(a, u). Similarly we define Pre(A, W ) = {x ∈ X | ∃u ∈ W, ∆(x, u) ⊆ A}. For the transition system S, we assume that for all x ∈ X and for all u ∈ U , ∆(x, u) = ∅. This means that for any state all the inputs are admissible.

III. MONOTONE TRANSITION SYSTEMS

A. Monotone transition systems

Let a transition system S = (X, X 0 , U, ∆, Y, H) where the set of outputs is equipped with a partial order ≤ Y . Using the injectivity of the output map H, a partial order ≤ X can be defined on the state space X as follows: for

x 1 , x 2 ∈ X, x 1 ≤ X x 2 if and only if H(x 1 ) ≤ Y H(x 2 ).
In the paper, we consider a class of transition systems for which transitions (and then trajectories) preserve some partial order on the states.

Definition 2: A transition system S = (X, X0, U, ∆, Y, H) is said to be monotone if for all x 1 , x 2 ∈ X and for all u 1 , u 2 ∈ U , if x 1 ≤ X x 2 and u 1 ≤ U u 2 , then for any x 1 ∈ ∆(x 1 , u 1 ), there exists

x 2 ∈ ∆(x 2 , u 2 ) satisfying x 1 ≤ X x 2 .
Now, let us give some characterizations of monotone transition systems. We first introduce an auxiliary lemma.

Lemma 1: Let a partially ordered set X, and let subsets A, B ⊆ X. The set A is included in lower closure of the set B (i.e. A ⊆↓ B) if and only if for any a ∈ A, there exists b ∈ B such that a ≤ X b.

Proposition 1: For a transition system S = (X, X 0 , U, ∆, Y, H) the following statements are equivalent:

(i) S is a monotone transition system;

(ii) for all x 1 , x 2 ∈ X and

u 1 , u 2 ∈ U , if x 1 ≤ X x 2 and u 1 ≤ U u 2 then ∆(x 1 , u 1 ) ⊆↓ ∆(x 2 , u 2 ); (iii) for all x ∈ X, u ∈ U we have: ∆(↓ x, ↓ u) ⊆↓ ∆(x, u).

B. Abstraction of a monotone control system

Let a monotone discrete-time control system Σ of the form:

x(k + 1) = f (x(k), u(k), d(k)), x(0) ∈ X 0 .
where x(k) ∈ X is a state, u(k) ∈ U is a control input and d(k) ∈ D is a disturbance input. It was shown in [START_REF] Kim | Symbolic control design for monotone systems with directed specifications[END_REF] how to construct a sparse abstraction S related to the original system Σ by an upper alternating simulation relation. This relation is useful for controller refinement when dealing with lower closed specifications. Moreover, the abstraction S satisfies the monotonicity property given in Definition 2.

In the following, we provide an efficient synthesis algorithm allowing to deal with monotone transition systems and lower closed safety specifications.

IV. CONTROLLER SYNTHESIS FOR SAFETY SPECIFICATIONS

A. Maximal safety controller Consider a transition system S and a safety specification X S ⊆ X (which can be easily obtained from a subset Y S ⊆ Y of safe outputs, X S = H -1 (Y S )). We consider a synthesis problem that consists in determining a controller that keeps the trajectories of the system inside a safe set X S . Let us remark that if a controller keeps the trajectories of the system S into X S , the output specification Y S = H(X S ) is satisfied by construction. The safety specification is said to be lower closed if X S is a lower closed set (which can be obtained from a lower closed set of outputs Y S ). Given a transition system S = (X, X0, U, ∆, Y, H), a controller for S is a set-valued map C : X ⇒ U . We define the domain of the controller as dom

(C) = {x ∈ X | C(x) = ∅}.
Definition 3: A safety controller C for the transition system S and the safe set X S satisfies:

• dom(C) ⊆ X S ; • ∀x ∈ dom(C) and ∀u ∈ C(x), ∆(x, u) ⊆ dom(C).
There are in general several controllers that solve the safety problem. A suitable solution is a controller that enables as many actions as possible. This controller C * is said to be a maximal safety controller, in the sense that for any other controller C and for all x ∈ X, we have

C(x) ⊆ C * (x).
Definition 4: Given a transition system S and a safety specification X S ⊆ X. A subset A ⊆ X S is said to be a controlled invariant if for all x ∈ A there exists u ∈ U such that ∆(x, u) ⊆ A.

It was shown in [START_REF] Tabuada | Verification and control of hybrid systems: a symbolic approach[END_REF] that there exists a maximal controlled invariant given by Z * = dom(C * ), which is the union of all controlled invariants.

In this part, we give some characterizations of the maximal safety controller for monotone transition systems and lower closed safety specifications X S ⊆ X. We first introduce the following instrumental lemma.

(1, 1) (1, 2) (1, 3) (2, 1) (2, 2) (2, 3) (3, 1) (3, 2) (3, 3) Fig. 1: Illustration of the partitioning of the input set U = {1, 2, 3} 2 .
The input set U is equipped with the partial order ≤ defined on R 2 . The input set U is partitioned as follows:

U 1 = U min = {(1, 1)}, U 2 = {(1, 2), (2, 1)}, U 3 = {(1, 3), (2, 2), (3, 1)}, U 4 = {(2, 3), (3, 2)}, U 5 = {(3, 3)}.
Lemma 2: Let the monotone transition system S = (X, X 0 , U, ∆, Y, H). Let C * the maximal safety controller for the system S and the lower closed safety specification X S ⊆ X. Let the controller C : X ⇒ U defined for x ∈ X by: C(x) = x ∈(↑x) C * (x ). We have:

(i) ↓ dom(C * ) = dom(C); (ii) dom(C) = dom(C * ).
Proposition 2: Consider a monotone transition system S = (X, X 0 , U, ∆, Y, H). Let C * be the maximal safety controller enforcing the lower closed safety specification X S ⊆ X. The following properties hold:

(i) dom(C * ) is a lower closed set; (ii) ∀ x 1 , x 2 ∈ X, if x 1 ≤ X x 2 then C * (x 2 ) ⊆ C * (x 1 ); (iii) ∀ x ∈ X, C * (x) is a lower closed set.

B. Control synthesis for monotone transition systems and directed safety specifications

In this section, we propose an efficient safety algorithm which exploits priorities on states and inputs. The synthesis of the maximal safety controller is done in two steps: first we use only inputs with lower priorities to compute the maximal controlled invariant set Z * . We then synthesize the maximal controller by exploring different inputs and using their priorities. In the rest of the paper, we only consider finite monotone transition systems. Let us remind that a state

x 1 ∈ X (a control u 1 ∈ U ) has a higher priority than a state x 2 ∈ X (a control u 2 ∈ U ) if and only if x 2 ≤ X x 1 (u 2 ≤ U u 1 ).
1) Domain of the controller: Given the partial order on the inputs ≤ U , we can introduce for U ⊆ U , the operator

min(U ) = {u ∈ U | ∀u 1 ∈ U , u ≤ U u 1 or (u, u 1 ) ∈ Inc U }.
Using this operator the input set U can be partitioned into finite number of sets U = ∪ N i=1 U i defined as follows:

U min = U 1 = min(U ) and U i+1 = min(U \ U i ), i ∈ {1, . . . , N -1}, where U i = ∪ i j=1 U j .
An illustration of the input partioning technique is given in Figure 1.

For a monotone transition system S = (X, X 0 , U, ∆, Y, H) we define its reduced transition system by S r = (X, X 0 , U 1 , ∆, Y, H), where U 1 ⊆ U is the set of minimal inputs.

Proposition 3: Let the transition system S = (X, X 0 , U, ∆, Y, H). Let C * be the maximal safety controller for the system S and the lower closed safety specification X S ⊆ X. Let the reduced transition system S r = (X, X 0 , U 1 , ∆, Y, H) and C * r the maximal safety controller for the transition system S r and safety specification X S . We have dom(C * ) = dom(C * r ). The previous result states that to compute the maximal controlled invariant set Z * = dom(C * ), it is sufficient to use inputs with lower priorities.

In the sequel, we define the notion of a basis which is adapted from [START_REF] Finkel | Well-structured transition systems everywhere![END_REF]. Indeed the concept of basis serves as a simpler representation of lower closed sets.

Definition 5: Let A be a finite partially ordered set. Let Z ⊆ A be a lower closed set. A set B = {s 1 , . . . , s N } ⊆ A is said to be the basis of Z, denoted B = Bas(Z), if Z = i=1,...,N ↓ s i and for all s i , s j ∈ B, if

s i = s j then (s i , s j ) ∈ Inc A .
The existence and uniqueness of a finite basis of a lower closed set follows from the fact that the relation ≤ A is a well-quasi-order [START_REF] Finkel | Well-structured transition systems everywhere![END_REF], [START_REF] Higman | Ordering by divisibility in abstract algebras[END_REF]. An illustration of the concept of basis is given in Figure 2. In the following result, we give a characterization of lower closed controlled invariant sets based on the notion of basis.

Proposition 4: Let the reduced transition system S r = (X, X 0 , U 1 , ∆, Y, H) and the lower closed safety specification X S ⊆ X. Let Z ⊆ X S be a lower closed set. Z is a controlled invariant for the system S r and the safe set X S if and only if the following property holds:

∀x ∈ Bas(Z), ∃u ∈ U 1 s.t ∆(x, u) ⊆ Z
(1) We now give the main result of the paper, which states that the maximal controlled invariant set is the maximal by inclusion lower closed set satisfying condition [START_REF] Tabuada | Verification and control of hybrid systems: a symbolic approach[END_REF].

Theorem 1: Let the reduced transition system S r = (X, X 0 , U 1 , ∆, Y, H) and the lower closed safety specification X S ⊆ X. The maximal controlled invariant set for the system S r and the specification X S is the maximal lower closed Z ⊆ X S satisfying (1).

Intuitively, the previous result means that the computation of the maximal controlled invariant for monotone transition systems and lower safety specifications can be efficiently done using Proposition 4. Indeed, the invariance condition for a set Z ⊆ X S needs to be checked only on the elements of the basis (see equation ( 1)), instead of all the elements of the set Z (see Definition 4), in the case of classical safety synthesis.

2) Computation of the maximal controlled invariant set: In this section, we propose a lazy fixed-point algorithm to compute the maximal controlled invariant. The algorithm is based on condition (1) and deals only with the elements of the basis in each iteration. To compute the maximal controlled invariant, the inputs to Algorithm 1 are S = S r which represents the reduced transition system, Z ex = X S is the safety specification and Z c = ∅ (this input to the algorithm will not be used for the computation of the maximal controlled invariant set Z * but for the computation of the maximal controller, as it will be shown in the next section). Algorithm 1 works as follows: the for loop in line 5 iterates over all elements of the basis B. Initially, this is the basis of the set X S . Once an element s ∈ B satisfies condition (1) for a given control input u ∈ U 1 (which is equivalent to the condition given in line 9 since Z c = ∅), we move to the next element of B, without exploring other inputs. If all control inputs have been explored but none leads to the acceptance condition, the element s is removed and the basis B is updated (lines 14 and 16). Once all elements in B satisfy condition (1) in line 7, the algorithm terminates and the maximal controlled invariant set Z * is returned. One can check that this maximal controlled invariant is lower closed by construction Z * =↓ B. The maximality comes from the fact that we start from the elements with the highest priority (elements of the basis of X S ) and keep removing elements that did not satisfy condition (1) until the fixedpoint is reached.

Let us remark that the abstraction is computed on the fly during the synthesis algorithm. Therefore, the elements with lower priorities are only explored when necessary.

3) Maximal safety controller: In this section, we propose an approach that lazily computes the maximal safety controller by exploiting priorities on the inputs. First we introduce some notations: for i ∈ {1, . . . , N }, we define the set Zi = Pre(Z * , Ui)

∩ Z * = {x ∈ Z * | ∃ u ∈ Ui, ∆(x, u) ⊆ Z * }. Let us remark that Z 1 = Z * . Similarly, we define the set Z i = Pre(Z * , U i ) ∩ Z * , where U i = j=i:N U j .
Lemma 3: For any i ∈ {1, . . . , N } the set Z i defined above is a lower closed set. Now, similarly to the result of Proposition 4, we will characterize the set Z i using its basis.

Proposition 5: Let the set Z i defined above. For a lower closed set Z ⊆ Z * , we have Z ⊆ Z i if and only if the following property holds:

∀x ∈ Bas(Z), ∃ u ∈ U i s.t ∆(x, u) ⊆ Z * (2)
We have from Lemma 3 that Z i is lower closed set. Then, from Proposition 5, Z i is the maximal set in Z * satisfying condition [START_REF] Belta | Formal methods for discrete-time dynamical systems[END_REF]. Hence, to compute the set Z i , i ∈ {2, . . . , N }, we rely on Algorithm 1, where the used inputs to the algorithm are S i = (X, X 0 , U i , ∆, Y, H), Z ex = Z * and Z c = Z * . Remark 1: Since we start the computation from the set Z * , all the basis B generated by the algorithm satisfies ↓ B ⊆ Z * . Then, the condition in line 7 of Algorithm 1 can be written as: there exits u ∈ U i such that ∆(x, u) ⊆ Z * , which is equivalent to condition (2) of Proposition 5.

We now present the key result for the efficient computation of the maximal safety controller C * .

Proposition 6: Let the sets Z i , i ∈ {1, . . . , N }, defined above, the following properties holds: (i) for all i ∈ {2, . . . , N }, Z i ⊆ Z i-1 ;

(ii) for all i ∈ {1, . . . , N }, Z i = Z i .

To compute the maximal safety controller, Algorithm 2 works as follows: the sets Z i , i ∈ {2, . . . , N } are computed iteratively, starting from Z * . At each step i ∈ {2, . . . , N }, the algorithm starts from the set Z i-1 and firstly computes the set Z i (line 5), (Initially, the algorithm starts from the set Z * = Z 1 and computes the set Z 2 ). Once this set is computed, for all x ∈ Z i-1 \ Z i the algorithm selects all the inputs u ∈ U i-1 satisfying ∆(x, u) ⊆ Z * (line 7). Hence, the controller given by Algorithm 2 can be defined for all x ∈ Z i-1 \ Z i by:

C(x) = {u ∈ U i-1 | ∆(x, u) ⊆ Z * }. (3)
and for all x ∈ dom(Z N ) by

C(x) = {u ∈ U N | ∆(x, u) ⊆ Z * }. (4)
Remark 2: We can remark from (i) in Proposition 6 that to compute the set Z i , i ∈ {2, . . . , N }, the explored set Z ex in Algorithm 1 can be given by Z ex = Z i-1 , instead of Z ex = Z * (see line 5 in Algorithm 2), which allows the synthesis to be more efficient. We are now ready to show the completeness of the controller given by Algorithm 2 w.r.t the maximal safety controller C * .

Proposition 7: Let the transition system S = (X, X 0 , U, ∆, Y, H) and the lower closed safety specification X S ⊆ X. Let C * be the maximal safety controller for the system S and specification X S , and let C defined as in ( 3) and ( 4). We have that C * (x) = C(x) for all x ∈ Z * .

Remark 3: Let us emphasis that when the partial order on the inputs ≤ U satisfies the following property: for all i ∈ {2, . . . , N } and for any

(u i-1 , u i ) ∈ U i-1 × U i , we have u i ≤ u i-1 .
The synthesis is more efficient. Indeed, for all x ∈ Z i-1 \ Z i , we have the existence of u ∈ U i-1 such that ∆(x, u) ⊆ Z * . Hence, from (iii) in Proposition 2 and since U i-2 ⊆↓ u, we have that U i-2 ⊆ C * (x). Then, at each step i ∈ {1, . . . , N }, only the set of inputs U i needs to be explored, instead of U i in the general case, which allows to speedup the synthesis of the maximal safety controller.

V. NUMERICAL EXAMPLE

A. Model description and control objective

We consider a vehicle modeled as a point mass m moving along a straight road. The dynamics of the vehicle is adapted from [START_REF] Ioannou | Autonomous intelligent cruise control[END_REF] and given by:

m v = α(u, v) = u -f 0 -f 1 v -f 2 v 2 if v > 0 max(u -f 0 , 0) if v = 0 (5
) where v ≥ 0 represents the velocity of the vehicle, m > 0 its mass, u is the net engine torque applied to the wheels and the term f 0 + f 1 v + f 2 v 2 include the rolling resistance and aerodynamics (f 0 , f 1 , f 2 ∈ R + ). In this equation, u is the control input and satisfies u ∈ [U min , U max ], where U min < 0 < U max . Moreover, we include a lead vehicle w ∈ W (considered as a bounded disturbance) in the system description, the dynamics of the global system is given by: The objective is to synthesize a controller for the follower vehicle, giving values of input u such that the velocity remains between 0 and v max , and the relative distance between the leader and the follower remains larger than d min ≥ 0, while assuming that the velocity of the leader w belongs to the set W = [0, v max ]. One can check that since the constraint v ≥ 0 is directly satisfied from (5), the safety specification is a lower closed set.

ḋ = w -v m v = α(u, v). ( 6
)
From this continuous-time system, we generate a discretetime model using the sampling period τ = 0.5s, while conserving the monotonicity property of the system.

For the construction of the symbolic abstraction, we use the same partitioning technique presented in [START_REF] Saoud | Contract based design of symbolic controllers for interconnected multiperiodic sampled-data systems[END_REF] with n x and n u as state and input discretization parameters.

B. Numerical results

In this section, we numerically illustrates the benefit of the proposed approach. The values shown in Table I are taken from [START_REF] Saoud | Contract based design of symbolic controllers for interconnected multiperiodic sampled-data systems[END_REF]. The implementations has been done in MATLAB, Processor Intel Core i7-8700, 3.20 Hg, RAM 16 GB.

We compute the maximal controlled invariant Z * using Algorithm 1 and synthesize the maximal safety controller C * using Algorithm 2. Figure 3 represents the resulting maximal safety controller C * using the following values of abstraction parameters: n u = 500 for the input discretization and n x = (300, 150) for the state-space discretization. The color bar represent the given input set U = [U min , U max ] where the blue color corresponds to the minimal input U min = -4031.9 mKg/s 2 and the yellow color corresponds to the maximal input U max = 2687.9 mKg/s 2 . For a given state (d, v) of the vehicle, Figure 3 shows the maximal allowed control input. Let us mention that following Remark 3, if an input u ∈ U is allowed by the maximal safety controller C * , then all inputs satisfying u ≤ U u are allowed by C * . Let us also mention that for each state, the controller has only to save the basis of the enabled inputs, which allows to reduce the size of the controller when implementing it in an embedded platform.

We evaluate the performance of the proposed approach w.r.t the classical safety synthesis using 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. The results of run time comparison are represented in Table II. In the second case we fix n x = (61, 31) and vary the input discretization parameter n u . The computational results are given in Table III. In Tables II andIII, T cl and T la represent the time needed to compute the maximal safety controller C * , in seconds. The last column T cl /T la represents the ratio between the classical and lazy synthesis approaches. Tables II andIII highlight the practical speedups that can be attained using the lazy approach, while ensuring completeness w.r.t the classical safety algorithm.

VI. CONCLUSION

In this paper, we have presented an efficient approach to controller synthesis for monotone transition systems and directed safety specifications. The synthesis of the maximal safety controller is done in two steps: first we use only inputs with lower priorities to compute the maximal controlled invariant set. Once this set is computed, we use a lazy approach to efficiently explore different inputs while using their priorities. Numerical results highlight the practical speedups that can be attained using the proposed approach, while ensuring completeness w.r.t the classical safety algorithm.

In future work we will develop more general algorithms allowing to extend the approach to other types of directed specifications, such as reachability, stability or more general properties described by temporal logic formula.

APPENDIX

Proof of Proposition 1

Proof: (i) ⇐⇒ (ii): Let x 1 , x 2 ∈ X and u 1 , u 2 ∈ U with x 1 ≤ X x 2 and u 1 ≤ U u 2 . From Lemma 1, we have that ∆(x 1 , u 1 ) ⊆↓ ∆(x 2 , u 2 ) iff for any x 1 ∈ ∆(x 1 , u 1 ), there exists x 2 ∈ ∆(x 2 , u 2 ) with x 1 ≤ X x 2 . Hence, (i) ⇐⇒ (ii).

(ii) =⇒ (iii): Let x ∈ X, u ∈ U , x 1 ∈ (↓ x) and u 1 ∈ (↓ u). We have x 1 ≤ X x and u 1 ≤ U u. Hence, from (ii) we have that ∆(x 1 , u 1 ) ⊆↓ ∆(x, u), for any x 1 ∈ (↓ x) and any u 1 ∈ (↓ u). Then, ∆(↓ x, ↓ u)) ⊆↓ ∆(x, u).

(iii) =⇒ (ii): Let x 1 , x 2 ∈ X and u 1 , u 2 ∈ U with x 1 ≤ X x 2 and u 1 ≤ U u 2 . We have that x 1 ∈ (↓ x 2 ) and u 1 ∈ (↓ u 2 ). Hence, from (iii), we have that

∆(x 1 , u 1 ) ⊆ ∆(↓ x 2 , ↓ u 2 ) ⊆↓ ∆(x 2 , u 2 ).

Proof of Lemma 2

Proof: From construction of the controller C, it follows immediately that ↓ dom(C * ) = dom(C). Let us prove that dom(C * ) = dom(C). Let x ∈ X, since x ∈ (↑ x) we have that dom(C * ) ⊆ dom(C). To prove the second inclusion, it is sufficient to show that C is a safety controller for the transition system S and the safety specification X S . We have that dom(C) =↓ dom(C * ) ⊆↓ X S = X S , where the first equality comes from (i), the second inclusion comes from the fact that C * is a safety controller and the last equality comes from the lower closedness of X S . Hence, the first condition of Definition 3 is satisfied. Now let x ∈ dom(C) and u ∈ C(x). From construction of the controller C, we have the existence of x ∈ X such that x ≤ X x , x ∈ dom(C * ) and u ∈ C * (x ). Then, we have that ∆(x, u) ⊆↓ ∆(x , u) ⊆↓ dom(C * ) = dom(C), where the first inclusion comes from (ii) in Proposition 1 and the second inclusion comes from the fact that C * is a safety controller. Then, condition (ii) in Definition 3 is satisfied and C is safety controller. Since C * is the maximal controller we have that dom(C) ⊆ dom(C * ).

Proof of Proposition 2

Proof: (i) We have from (ii) in Lemma 2 that dom(C * ) = dom(C). Then, ↓ dom(C * ) =↓ dom(C) = dom(C * ), where the last equality comes from (i) in Lemma 2. Hence, dom(C * ) is a lower closed set.

(

ii) Let x 1 , x 2 ∈ X with x 1 ≤ X x 2 . Let u ∈ C * (x 2 ). Then, ∆(x 2 , u) ⊆ dom(C * ). Hence, we have that ∆(x 1 , u) ⊆↓ ∆(x 2 , u) ⊆↓ dom(C * ) = dom(C * )
, where the first inclusion comes from the fact that S is a monotone transition system and the last equality comes from (i). Hence, by maximality of C * , we have that u ∈ C * (x 1 ). Then, C * (x 2 ) ⊆ C * (x 1 ).

(iii) Let x ∈ X, u ∈ C * (x) and u ∈↓ u. We have that ∆(x, u ) ⊆↓ ∆(x, u) ⊆↓ dom(C * ) = dom(C * ), where the first inclusion comes from the monotonicity of the transition system S, the second inclusion comes from the fact that C * is a safety controller and the last equality comes from the lower closedeness of dom(C * ). Hence, we have ∆(x, u ) ⊆ dom(C * ). Then, by maximality of C * , u ∈ C * (x).

Proof of Proposition 3

Proof: Let us define the controller C r of the reduced transition system S r and the safe set X S as follows: for x ∈ X, C r (x) = C * (x) ∩ U 1 . First let us prove that dom(C r ) = dom(C * ). The inclusion dom(C r ) ⊆ dom(C * ) follows immediately from the construction of the controller C r . Now let x ∈ dom(C * ) and let u ∈ C(x). From (iii) in Proposition 2 we have that ↓ u ⊆ C * (x), then there exists u ∈ U 1 such that u ∈ C * (x). Then, u ∈ C r (x). Hence x ∈ dom(C r ) and dom(C r ) = dom(C * ). Now let us prove that for all x ∈ X, C r (x) = C * r (x). The first inclusion C r (x) ⊆ C * r (x) follows from maximality of the controller C * r . For the second inclusion, we have from maximality of C * and since

U 1 ⊆ U that C * r (x) ⊆ C * (x) for all x ∈ X. Moreover, by construction of C * r , we have that C * r (x) ⊆ U 1 for all x ∈ X. Then, C r (x) = C * r (x) for all x ∈ X. Since dom(C r ) = dom(C * ), we have that dom(C * r ) = dom(C * ).

Proof of Proposition 4

Proof: Let Z =↓ Z, we first assume that Z is a controlled invariant. Using the fact that Bas(Z) ⊆ Z, condition (1) is directly satisfied. Now let us prove the second implication. Assume that condition (1) is satisfied, and let us prove that Z is a controlled invariant. For x ∈ Z, there exists x ∈ Bas(Z) such that x ≤ X x . Since x ∈ Bas(Z), we have from (1) the existence of u ∈ U 1 such that ∆(x , u) ⊆ Z. From monotonicity of the transition system S and since x ≤ X x , we have that ∆(x, u) ⊆↓ ∆(x , u) ⊆↓ Z = Z. Hence, Z is a controlled invariant.

Proof of Theorem 1

Proof: Given the transition system S r and the lower closed safety specification X S . We have from (i) in Proposition 2 that the maximal controlled invariant for S r and the safe set X S , Z * = dom(C * ) is a lower closed set. Hence, from Proposition 4, it follows immediately that the maximal controlled invariant set for the system S r and the specification X S is the maximal lower closed set Z ⊆ X S satisfying (1).

Proof of Lemma 3

Proof: Let i ∈ {1, . . . , N }, x ∈ Z i and x ≤ X x. From definition of Z i we have the existence of u ∈ U i such that ∆(x, u) ⊆ Z * . Then, we have ∆(x , u) ⊆↓ ∆(x, u) ⊆↓ Z * = Z * , where the first inclusion comes from the monotonicity of the transition system S, the second inclusion comes the construction of the set Z i and the last inclusion comes from (i) in Proposition 2 (Z * = dom(C * ) is a lower closed set). Then, Z i is a lower closed set.

Proof of Proposition 5

The proof is similar to the one of Proposition 4 and then omitted.

Proof of Proposition 6

Proof: (i) Let i ∈ {2, . . . , N } and x ∈ Z i . Hence, x ∈ Z * and the exists u ∈ U i such that ∆(x, u) ⊆ Z * . Since U i-1 ≤ U U i , we have the existence of u ∈ U i-1 such that u ≤ U u. Then, ∆(x, u ) ⊆↓ ∆(x, u) ⊆↓ Z * = Z * , where the first inclusion comes from the monotonicity of the transition system S, the second inclusion comes the construction of the set Z i and the last inclusion comes from (i) in Proposition 2. Hence, x ∈ Z i-1 .

(ii) For i ∈ {1, . . . , N }, the proof follows immediately from (i) and the fact that Z i = ∪ j=i:N Z j .

Proof of Proposition 7

Proof: From the construction of C in (3) and ( 4) we have that C(x) ⊆ C * (x) for all x ∈ Z * . Let Z i be defined as above, We have from (i) in Proposition 6 that:

Z * = Z 1 ∪Z 2 ∪. . .∪Z N = (Z 1 \Z 2 )∪. . .∪(Z N -1 \Z N )∪Z N ,
Let x ∈ Z * and u ∈ C * (x). If x ∈ Z N , then using the fact that U N = U , it follows from (4) that u ∈ C(x). Now if there exists i ∈ {2, . . . , N } such that x ∈ Z i-1 \ Z i = Z i-1 \ Z i , where the last equality comes from (ii) in Proposition 6. Hence, we have that u / ∈ U i . Then, u ∈ U i-1 . Moreover, C * is the maximal safety controller, then using the fact that ∆(x, u) ⊆ Z * , we have from construction of the controller C in (3) that u ∈ C(x). Then, C * (x) = C(x) for all x ∈ Z * .

  used lazy synthesis algorithm by exploiting priorities on the inputs. *This project has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement No 725144). This research was partially supported by Labex DigiCosme (project ANR-11-LABEX-0045-DIGICOSME) operated by ANR as part of the program "Investissement d'Avenir" Idex Paris Saclay (ANR-11-IDEX-0003-02).

4 Fig. 2 :

 42 Fig. 2: Illustration of Definition 5. A lower closed set B and its basis Bas(B) = {s 1 , s 2 , s 3 , s 4 }.

Algorithm 1 : 2 B 3 B 4 while B pr = B do 5 for all s ∈ B do 6 B 7 for all u ∈ U do 8 U 12 U 15 B

 123456781215 Z = InvariantSet(S, Z ex , Z c ) Input: Transition system S = (X, X 0 , U, ∆, Y, H), explored set Z ex , controllable set Z c . Output: Invariant set Z 1 begin := Bas(Z ex ); pr = ∅; us := ∅; int = ∅; 9 if ∆ (s, u) ⊆ (↓ B) ∪ Z c then 10 int = U int ∪ {u}; 13 if U int = U then14 B us := B us ∪ {s}; pr := B; 16 B := Bas (↓ (B) \ B us ) ; 17 return ↓ B;

Algorithm 2 : 2 C 3 Z

 223 Maximal Safety Controller Input: Transition system S = (X, X 0 , U, ∆, Y, H), Safety specification X S Output: Controller C 1 begin (X) := ∅; * := InvariantSet(S 1 , X S , ∅);4 for i = 2 : N do 5 Z i := InvariantSet(S i , Z i-1 , Z * ); 6 for s ∈ Z i-1 \ Z i do 7 C(s) := {u ∈ U i-1 | ∆ (s, u) ⊆ Z * };8 for s ∈ Z N do 9 C(s) := {u ∈ U N | ∆ (s, u) ⊆ Z * }; 10 return C;

Fig. 3 :Remark 4 :

 34 Fig. 3: Maximal safety controller C *

TABLE I :

 I Vehicle and safety parameters

	Parameter	Value	Unit
	M	1370	Kg
	f 0	51.0709	N
	f 1	0.3494	N s/m
	f 2	0.4161	N s 2 /m 2
	U min	-4031.9	mKg/s 2
	Umax	2687.9	mKg/s 2
	d min

TABLE II :

 II Runtime comparison when varying the state-space

	discretization parameter
	Number of states	T la (s)	T cl (s)	T cl /T la
	(61,31)	0.41s	6.84s	16.79s
	(122,62)	1.04s	26.85s	25.85s
	(244,124)	3.71s	107.55s	28.98s
	(488,248)	14.11s	432.22s	30.64s
	(976,496)	54.58s	1695.00s	31.05s

TABLE III :

 III Runtime comparison when varying the input dis-

	cretization parameter
	Number of inputs T la (s)	T cl (s)	T cl /T la
	10	0.48s	7.17s	14.8s
	20	0.49s	13.87s	29.19s
	40	0.64s	27.47s	43.2s
	80	0.98s	54.81s	56.06s
	160	1.66s	109.47s	65.85s

Given a partially ordered set X, we say that a state x 1 ∈ X has a highest priority than a state x

∈ X if the state x 1 is bigger than x 2 with respect to the given partial order on the states. The notion of priority is defined similarly for a partially ordred set of inputs.