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