Journée scientifique projet DGA MRIS

Date et Lieu

Jeudi 22 juin 2017 -- LIX, Ecole Polytechnique, Palaiseau

Salle: Grace Hopper

Programme

9h00 - Accueil Café

9h30 - Luc Jaulin, Thomas Le Mézo et Benoît Zerr

Eulerian filter and Eulerian smoother

Eulerian state estimation can be seen as a problem of estimating trajectories in the case where temporal logic constraints are combined with state equations. Typical constraints are - "the robot A has met the robot B before the collision with robot C". - "After the robot crossed the river, its speed was always lower than 1m/s" In the presentation, it will be shown that Eulerian state estimation can be solved efficiently using, as a basic stone, the concept of largest positive invariant set associated to a nonlinear state equation. As a result, a new filter and a new smoother will be introduced to estimate efficiently a trajectory in an Eulerian context.

10h30 - Eric Goubault et Sylvie Putot

Forward inner-approximated reachability of non-linear continuous systems

We propose an approach for computing inner-approximations of reachable sets of dynamical systems defined by non-linear, uncertain, ordinary differential equations. This is a notoriously difficult problem, much more intricate than outer-approximations, for which there exist well known solutions, often based on Taylor models. The few methods developed recently for inner-approximation mostly rely on backward flowmaps, and extra ingredients, either coming from optimization, or involving topological criteria, are required. Our solution, in comparison, builds on rather inexpensive set-based methods, namely a generalized mean-value theorem combined with Taylor models outer- approximations of the flow and its Jacobian with respect to the uncertain inputs and parameters. We demonstrate with a C/C++ prototype implementation that our method is both efficient and precise on classical examples. The combination of such forward inner and outer Taylor-model based approximations can be used as a basis for the verification and falsification of properties of cyber-physical systems.

11h30 - Adina M. Panchea et Thibault Toralba

Towards reliable motion planning coordination for autonomous robots

In this presentation, an ongoing study is introduced and is thought of as a way to validate previous proposed reliable motion planners, e.g. BoxRRT*, on a real application which controls and coordinates autonomous robots. The complex application will be simplified by designing it in a modular way with the use of Robot Operating System (ROS) tools and libraries. Moreover, affordable and accessible items will be considered for the application, such as Logitech cameras, Arduino board or Xbee modules.

12h30 - Repas

Club Magnan

14h30 - Sergio Rajsbaum

Overview of Fault-Tolerant Distributed Runtime Verification (DRV)

Building a decentralised fault-tolerant runtime monitor is an especially difficult task since it involves designing a distributed algorithm that coordinates the monitors in order for them to reason consistently about the temporal behavior of the system being monitored. DRV techniques are less developed; they involve designing a distributed algorithm that monitors another distributed algorithm. In an asynchronous system where monitors may crash, it is impossible for the monitors to agree on the order of events in the system (due to the impossibility of solving consensus). Thus, it is unavoidable that monitors emit different opinions about the validity of the computation, that nevertheless, should be consistent with each other. Lower and upper bounds on the number of opinions that may have to be emitted, can be derived, as a function of the specification that is being monitored. Techniques at the crossroads where distributed algorithms and formal methods meet are needed.

15h30 - Benjamin Martin et Olivier Mullier

Rigorous computation of viability kernels

The study of viability kernels can be of critical importance for the verification of control systems. A viability kernel over a set of safe states is the set of initial states for which the trajectory can be controlled so as to stay within the safe set for an indefinite amount of time.

In this talk, we investigate several improvements of the rigorous method from Monnet et al. This method computes rigorously an inner and an outer approximation of the viability kernel of a control system using methods based on interval analysis. It consists of two phases: first a phase where an initial under-approximation of the viability kernel is computed via Lyapunov-like functions; second the initial under-approximation is improved by finding other states that can reach the under-approximation, without exiting the safe set, using numerical guaranteed integration.

Among the considered improvements, we will discuss an approach inspired by an approach for the computation of barrier function for computing a good initial under-approximation of the viability kernel in order to ease the improvement phase. The improvement phase is also enhanced by using some heuristics for selecting the right control.

17h00* - Thomas Le Mézo

Projet Guerlédan

Social event

Mercredi 21 juin 2017 -- 19h30 - TBA

Participants: