Laurent Fribourg

Adrien Le Coënt, Laurent Fribourg, Nicolas Markey et al.

We present a correct-by-design method of state-dependent control synthesis for linear discrete-time switching systems. Given an objective region R of the state space, the method builds a capture set S and a control which steers any element of S into R. The method works by iterated backward reachability from R. More precisely, S is given as a parametric extension of R, and the maximum value of the parameter is solved by linear programming. The method can also be used to synthesize a stability control which maintains indefinitely within R all the states starting at R. We explain how the synthesis method can be performed in a distributed manner. The method has been implemented and successfully applied to the synthesis of a distributed control of a concrete floor heating system with 11 rooms and 2^11 = 2048 switching modes.

Adrien Le Coënt, Julien Alexandre Dit Sandretto, Alexandre Chapoutot et al.

We present an algorithm of control synthesis for nonlinear switched systems, based on an existing procedure of state-space bisection and made available for nonlinear systems with the help of validated simulation. The use of validated simulation also permits to take bounded perturbations and varying parameters into account. It is particularly interesting for safety critical applications, such as in aeronautical, military or medical fields. The whole approach is entirely guaranteed and the induced controllers are correct-by-design.

Adrien Le Coënt, Laurent Fribourg

In this paper, we propose a new method for ensuring formally that a controlled trajectory stay inside a given safety set S for a given duration T. Using a finite gridding X of S, we first synthesize, for a subset of initial nodes x of X , an admissible control for which the Euler-based approximate trajectories lie in S at t $\in$ [0,T]. We then give sufficient conditions which ensure that the exact trajectories, under the same control, also lie in S for t $\in$ [0,T], when starting at initial points 'close' to nodes x. The statement of such conditions relies on results giving estimates of the deviation of Euler-based approximate trajectories, using one-sided Lipschitz constants. We illustrate the interest of the method on several examples, including a stochastic one.

Adrien Le Coënt, Laurent Fribourg

We have recently used a symbolic reachability method for controlling the stability of special hybrid systems called 'sampled switched systems'. We show here how the method can be extended in order to control the stability of more general hybrid systems with guard conditions and state resets. We illustrate the method through the example of a biped robot with 6 state variables, using a proportional-derivative (PD) controller. More specifically, we isolate a state region R such that, starting from a state located in R just after a footstep, the PD-control makes the robot state return to R at the end of the following footstep.

Daniel Martin Xavier, Ludovic Chamoin, Jawher Jerray et al.

The early stopping strategy consists in stopping the training process of a neural network (NN) on a set $S$ of input data before training error is minimal. The advantage is that the NN then retains good generalization properties, i.e. it gives good predictions on data outside $S$, and a good estimate of the statistical error (``population loss'') is obtained. We give here an analytical estimation of the optimal stopping time involving basically the initial training error vector and the eigenvalues of the ``neural tangent kernel''. This yields an upper bound on the population loss which is well-suited to the underparameterized context (where the number of parameters is moderate compared with the number of data). Our method is illustrated on the example of an NN simulating the MPC control of a Van der Pol oscillator.

Étienne André, Emmanuel Coquard, Laurent Fribourg et al.

The next generation of space systems will have to achieve more and more complex missions. In order to master the development cost and duration of such systems, an alternative to a manual design is to automatically synthesize the main parameters of the system. In this paper, we present an approach for the specific case of the scheduling of the flight control of a space launcher. The approach requires two successive steps: (1) the formalization of the problem to be solved in a parametric formal model and (2) the synthesis of the model parameters with a tool. We first describe the problem of the scheduling of a launcher flight control, then we show how this problem can be formalized with parametric stopwatch automata; we then present the results computed by the parametric timed model checker IMITATOR. We enhance our model by taking into consideration the time for switching context, and we compare the results to those obtained by other tools classically used in scheduling.

Étienne André, Emmanuel Coquard, Laurent Fribourg et al.

The next generation of space systems will have to achieve more and more complex missions. In order to master the development cost and duration of such systems, an alternative to a manual design is to automatically synthesize the main parameters of the system. In this paper, we present an approach on the specific case of the scheduling of the flight control of a space launcher. The approach requires two successive steps: (1) the formalization of the problem to be solved in a parametric formal model and (2) the synthesis of the model parameters with a tool. We first describe the problematic of the scheduling of a launcher flight control, then we show how this problematic can be formalized with parametric stopwatch automata; we then present the results computed by IMITATOR. We compare the results to the ones obtained by other tools classically used in scheduling.

Gilles Feld, Laurent Fribourg, Denis Labrousse et al.

High-power converters based on elementary switching cells are more and more used in the industry of power electronics owing to various advantages such as lower voltage stress and reduced power loss. However, the complexity of controlling such converters is a major challenge that the power manufacturing industry has to face with. The synthesis of industrial switching controllers relies today on heuristic rules and empiric simulation. The state of the system is not guaranteed to stay within the limits that are admissible for its correct electrical behavior. We show here how to apply a formal method in order to synthesize a correct-by-design control that guarantees that the power converter will always stay within a predefined safe zone of variations for its input parameters. The method is applied in order to synthesize a correct-by-design control for 5-level and 7-level power converters with a flying capacitor topology. We check the validity of our approach by numerical simulations for 5 and 7 levels. We also perform physical experimentations using a prototype built by SATIE laboratory for 5 levels.