Journée scientifique conjointe Chaire ISC et projet DGA AID

Date et Lieu

Vendredi 13 mars 2020 -- ENSTA Paris, Palaiseau

Salle: R317 (salle de classe de l'U2IS)

Programme de la journée

9h00 - Accueil Café

09h30 -- Luc Jaulin

Underwater navigation with stable cycles (Slides)

In an environment where almost no landmarks exists for localizaton, as it it the case for many underwater applications, we show that using the concept of stable cycle, we can move from zones to zones without getting lost. For this purpose, we propose the concept of 'stable cycle' used by many animals for navigation. We prove the stability of these cycles using the concept of Poincaré map and interval analysis. Some real experiments show the feasibility of the approach for underwater navigation.

10h30 -- Ismail Lakhim Bennani

joint work with Goran Frehse and Marc Pouzet

Falsification of Hybrid Systems using Automatic Differentiation (Slides)

The falsification problem is a property-based testing problem where the goal is to find an input and an output of the system that contradict its specification. Hybrid systems are programs that combine continuous-time dynamics with discrete control. In these programs, values are continuous-time quantities and numerical variables are defined by ODEs. They are often used as models of embedded systems because they can express software (discrete control) and its environment (dynamical system).

The state-of-the-art in falsification consists of tools that interpret a specification as a function from an input and an output (usually timeseries, that is, sampled dynamics) to a float. The output of such a function is called robustness, it can be used as a score for a particular simulation run. These tools then solve the falsification problem using black-box optimization where the score function is the composition of the system and its quantitative specification. They use standard techniques such as Simulated Annealing or the Nelder-Mead algorithm.

At the moment, my PhD focuses on trying to improve optimization by using gradient-based techniques. A first idea was to implement automatic differentiation for hybrid programs so as to compute the derivatives of the robustness with respect to the inputs of the system. We are also exploring using automatic differentiation to trigger mode switches in a program so as to ensure code coverage throughout test runs.

11h30 -- Xavier Thirioux

Taylor series revisited (Slides)

We propose a renovated approach around the use of Taylor expansions to provide polynomial approximations. We introduce a coinductive type scheme and finely-tuned operations that altogether constitute an algebra, where our multivariate Taylor expansions are first-class objects. As for applications, beyond providing classical expansions of integro-differential and algebraic expressions mixed with elementary functions, we demonstrate that solving ODE and PDE in a direct way, without external solvers, is also possible. Finally, for ODE specifically, we also discuss the computation of certified errors within our scheme.

12h30 - 14h00 -- Repas au Club Magnan

14h00 -- Ghilès Ziat

Efficient Tracking of Propagation Success (Slides)

Continuous solvers heavily rely on interval analysis, and generally use propagators that reach hull consistency (or box consistency). When propagation can not remove anymore values from the search space, it is said to have reached consistency. However, in this case, no information about the satisfiability of the resulting space is given and, moreover, consistency can be reached even though values were removed from the search space. We propose in this work an extension to a well known propagation algorithm, namely HC4, in order to track and describe qualitatively its results. Our base descriptors can be computed within a neglectible overhead, as they reuse the same mechanisms as HC4. We believe these descriptors can be very useful in practice for the design of solvers as they make possible an early detection of a consistent/inconsistent state. We go one step further by defining some more precise descriptors, which can be more costly but can be used to reduce the search space even more. We have implemented our techniques within a prototype solver and measured its performances on a standard benchmark of continuous problems. Experiments demonstrate the interest of our approach.

14h45 - Olivier Mullier and Ghilès Ziat

joint work with Julien Alexandre dit Sandretto, Christophe Garion, Xavier Thirioux

Trajectory validation of drone swarms, using AbSolute and DynIbex (Slides part 1)

This work addresses the problem of trajectory verification for drones swarms. Trajectories are finite and represented as a sequence of contiguous boxes over-approximating the concrete trajectories of the drones. The space the drones evolve in is bounded and may include obstacles which are or arbitrary shape. The main property we aim to prove is the absence of collisions between drones and obstacles, and drones between each others. We solve the problem by using Constraint Programming techniques with abstract domains from Abstract Interpretation. We use a form of disjunctive completion for which we provide a split operator and an efficient propagation mechanism. This solution is implemented in the AbSolute solver, has been tested on randomly generated trajectories and on real trajectories generated by the DynIbex tools. Experiments show promising results.

15h45 -- Adrien Le Coënt

joint work with Julien Alexandre dit Sandretto and Alexandre Chapoutot

Guaranteed co-simulation of continuous-time dynamical systems (Slides)

We tackle the problem of guaranteed simulation of continuous-time dynamical systems. The always increasing complexity of current engineering systems leads to models of higher and higher dimensions, yet typically involve multiple subsystems or even multiple physics. Given this modularity, we more precisely explore co-simulation of such dynamical systems, with the aim of reaching higher dimensions of the simulated systems. In a co-simulation setting, the global system is divided in sub-systems, for which different simulation units (and possibly schemes) are used, but exchange values of their outputs at some communication (macro) steps. In this talk, we present a guaranteed interval based approach for co-simulation of continuous time systems. Provided that a suitable decomposition of the system is given, we propose an algorithm which first proves the existence, and returns an enclosure of global solutions, using only local computations. This mitigates the curse of dimensionality faced by global (guaranteed) integration methods. Local computations are then realized with a safe estimate of the other sub-systems until the next macro step. We increase the accuracy of the approach by using an interval extrapolation of the state of the other sub-systems. We finally propose some possible further improvements including adaptive macro step size. Our method is fully guaranteed, taking into account all possible sources of error. We illustrate our approach on multiple examples of the literature, and show some possible applications in e.g. symbolic optimal control synthesis.

16h45 -- vie du groupe

17h00 -- fin de la réunion

Participants

Social event

Jeudi 12 mars 2020 -- 19h30 -