Journée scientifique projet DGA AID
Date
November 3, 2020 -- Virtual meeting
Attendees
Schedule
14h00 - Début
Session 1: Verification methods
14h15 - Sergio Mover
Symbolic Semi-Algebraic Decomposition for Polynomial Dynamical Systems Slides
There exist different invariant generation techniques for polynomial dynamical systems. Semi-algebraic decomposition is an invariant generation technique that partition the state space of the system according to a set of predicates obtained considering the signs (<, >, =) of a set of polynomials. Similarly to predicate abstraction for discrete systems, the number of concrete states in the decomposition (i.e., the abstract system) is exponential in the number of polynomials and hence is expensive to explicitly compute and analyze (e.g., to prove a safety property or extract an invariant). We propose a symbolic encoding of the semi-algebraic abstraction formulation as a first-order logic formula that has a size linear in the number of abstraction predicates, hence avoiding the explicit enumeration of all the possible abstract transitions. Furthermore, the encoding as first-order logic formula allows us to reuse standard predicate abstraction techniques (e.g., computing the abstraction using All-SAT, verifying a safety property via "implicit" predicate abstraction model checking, ...). We show some preliminary experiments proving safety for non-linear dynamical systems.
14h45 - François Bidet
Reachability Analysis for Systems Affine in the Time Varying Bounded Uncertainties Slides
We present a new way to compute reachability of systems affine in uncertainties which are bounded but arbitrary time varying. Our method is based on decomposition of functions as difference of positive ones.
Authors: François Bidet, Éric Goubault, Sylvie Putot
Session 2: Robotic
15h15 - Luc Jaulin
Autonomous parachute Slides and Video
In this talk, I will present the realization by Kevin Bedin at ENSTA-Bretagne of a small-size, small-capacity, autonomous parachute. This project has been initiated by the AID, for the benefit of the 1st RPIM (1er Régiment de Parachutistes d’Infanterie de Marine). I will present the control laws that have been implemented in the parachute, how the wind can be estimated and how we can guarantee that the parachute will land within a given bounded area.
Authors: Kévin Bedin, Matthieu Philippe, Thomas Le Mézo
15h45 - Uli Fahrenberg
Distributed underwater robots Slides
We give an outlook as to what the near future of underwater robotics may look like. We propose that it will be distributed, that is, the near future of underwater robotics is underwater swarm robotics. We identify challenges which need to be addressed in order to advance the state of distributed underwater robotics. While the general challenges of distributed robotics are reasonably well-understood, the underwater environment poses additional constraints on communication, movement, vision, etc. which have made application development difficult. Using motivated examples of tasks and missions which may reasonably be accomplished in the near future, we sketch a possible way forward.
Authors: Julien Damers, Hervé de Forges, Uli Fahrenberg
Session 3: Neural networks
16h15 - Arthur Clavière
Certification of neural network-based systems Slides
We propose a system-level approach for verifying the safety of neural network controlled systems, combining a continuous-time physical system with a discrete-time neural network based controller. We assume a generic model for the controller that can capture both simple and complex behaviours involving neural networks. Based on this model, we perform a reachability analysis that soundly approximates the reachable states of the overall system, allowing to achieve a formal proof of safety. To this end, we leverage both validated simulation to approximate the behaviour of the physical system and abstract interpretation to approximate the behaviour of the controller. We evaluate the applicability of our approach using a real-world use case. Moreover, we show that our approach can provide valuable information when the system cannot be proved totally safe.
16h45 - Maria Luiza Costa Vianna
Neural Network Based Model Predictive Control for an Autonomous Vehicle Slides
The capacity of biologically inspired algorithms to solve complicated nonlinear problems motivated the development of controllers based on neural networks, now not only monitoring the environment signals but also interfering on them. In this work we compare different methods to train a neural network to replace a model predictive controller(MPC) in the control loop of an autonomous vehicle. We present an analysis carried with the objective of understanding how changing the different hyper parameters and the inputs of the neural network, as well as the complexity of the training dataset, affects its capacity to learn the MPC’s behavior. The objective is to choose the simplest architecture in order to facilitate the safety verification of the neural controller.
Authors: Sylvie Putot, Eric Goubault, Maria Luiza Costa