Salle 4A301, Télécom Paris. Les 8 mars à partir de midi, et 9 mars jusqu’à 16h00.

Repas en 1A422.

## Présentations

**Tuesday 8th March**- 12am-1:30pm Welcome, lunch, salle 1A422 (salle de réception au dessus du restaurant administratif)

- 1:30pm-2pm Simon Rohou, « Codac : Catalog Of Domains And Contractors »

Recent works in the set-membership community have shown that interval and constraint-propagation methods can be used for efficiently solving difficult problems involving nonlinear equations, differential systems, delays, time uncertainties, or unknown initial conditions. Primitive operators designed for solving simple constraints or equations are made available by the community. Some of them are gathered in the Codac library (http://codac.io), that provides tools to combine them easily, thus allowing to tackle complex problems. The outputs are sets of feasible solutions, such as boxes, tubes, or subpavings. In this talk, we will see an example of use of the Codac library, by dealing with a realistic problem of robot localization. - 2pm-2:15pm discussion, break
- 2:15pm-2:45pm Alexandre Chapoutot, « Plateforme robotique en extérieur »

Le développement d’algorithme de navigation et d’exploration d’environnements extérieurs dits non structurés (à l’opposé des zones urbaines) demande une mise en oeuvre sur le terrain afin de mieux apprécier les défis scientifiques et techniques. Pour cela l’ENSTA Paris souhaite développer une zone d’expérimentation pour la robotique en extérieur permettant de combiner différents types de véhicules dans les domaines terrestres, aériens et potentiellement marin. Cette zone a également pour ambition d’être composée de différents types de terrains afin de couvrir une grande variété de situations. Par exemple, il y aurait une partie forestière, un pré, un bâtiment et également une volière de grande taille. L’objectif de cette présentation est de décrire les idées actuelles de développement de la plateforme robotique ainsi que de permettre la discussion pour de possible collaboration. - 2:45pm-3pm discussion, break

- 3pm-3:30pm Maria Luiza Costa Vianna, « Guaranteed characterization of the area explored by an autonomous robot«

Fully coverage of an area of interest using exteroceptive sensors is a common task for an autonomous robot, applications varying from Mine Counter Measurement(MCM) missions to lawn-mowing. Estimating the area explored by the robot is important for planning paths that lead to complete coverage and it enables to determine if an area-covering mission is complete. In addition, some missions might require the robot to revisit some area of interest. In this case, estimating how many times each part of the space has been covered by the robot’s sensors is also important for assessing the mission completion. In this presentation, we propose a method for characterizing the area explored by an autonomous robot relying on the topological properties of the covered area. We take into consideration the uncertainty in the robot’s trajectory using interval analysis. - 3:30pm-3:45pm discussion, break
- 3:45pm-4:15pm Lélio Brun, « From Lustre to C: a translation validation approach to verified compilation«

Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications. Tools like SCADE and Simulink/Stateflow are equipped with compilers that translate such specifications into executable code. They provide programming languages for composing functions over streams as typified by dataflow synchronous languages like Lustre. In this work, we turn an academic Lustre to C compiler, LustreC, into a certifying compiler. Along with the produced C code, we generate contracts and predicates in the specification language of the Frama-C tool. That way, we can give both an encoding of the transition system semantics of the Lustre nodes and a proof obligation that the executable code respects that semantics, to be automatically discharged by SMT solvers. Moreover, we also translate contracts formulated on the Lustre specifications level into contracts on the C code, in order to ensure that properties shown at high level, eg. using model-checking techniques, still hold at low level. - 4:15pm-4:30pm discussion, break
- 7:30pm Dinner, in Paris. Restaurant Zeyer, next to the Alesia metro station, 62 rue d’alesia

- 12am-1:30pm Welcome, lunch, salle 1A422 (salle de réception au dessus du restaurant administratif)
**Wednesday 9th March**- 9:30pm-9:45am Welcome (again), coffee break
- 9:45am-10:15am Alexandre Chapoutot, « Successive Convexification for Optimal Control with Signal Temporal Logic Specifications »

As the scope and complexity of modern cyber-physical systems increase, newer and more challenging mission requirements will be imposed on the optimal control of the underlying unmanned systems. This talk proposes a solution to handle complex temporal requirements formalized in Signal Temporal Logic (STL) specifications within the Successive Convexification algorithmic framework. The SCVXSTL approach consists of four steps: 1) Express the STL specifications using their robust semantics as state constraints; 2) Introduce new auxiliary state variables to transform these state constraints as system dynamics, by exploiting the recursively defined structure of robust STL semantics; 3) Smooth the resulting system dynamics with polynomial smooth min- and max- functions; 4) Convexify and solve the resulting optimal control problem with the \scvx algorithm, which enjoys guaranteed convergence and polynomial time subproblem solving capability. The proposed approach retains the expressiveness of encoding mission requirements with STL semantics, while avoiding the usage of combinatorial optimization techniques such as Mixed-integer programming. Numerical results are shown to demonstrate its effectiveness.

- 10:15am-10:30am discussion, break
- 10:30am-11:00am Vadim Malvone, « Several contributions to Multi-Agents«

Abstract: Game theory in AI is a powerful mathematical framework largely applied in the last three decades for the strategic reasoning in multi-agent systems. Seminal works along this line started with turn-based two-player games (under perfect and imperfect information) to check the correctness of a system against an unpredictable environment. Then, large effort has been devoted to extend those works to the multi-agent setting and, specifically, to efficiently reasoning about important solution concepts such as Nash Equilibria and the like. An important application of game theory in AI concerns formal-system verification. In particular, game theory has come to the fore as a powerful tool for the verification of reactive systems and embedded systems. Breakthrough contributions along this direction concern the introduction of logics for the strategic reasoning such as Alternating-time Temporal Logic (ATL), Strategy Logic (SL), and their extensions. In this talk, I present the main elements of this research area and some of my contributions. - 11:00am-11:15am discussion, break
- 11:15am-11:45am Luc Jaulin, » Actions of the hyperocta hedralgroup to compute minimal contractors«

The hyperoctahedral group Bn is the group of symmetries of a hypercube of R^n. For instance permutations, or symmetries along each canonical plane of all belong to Bn. Now, many sets of equations we meet in our applications contain hyperoctahedral symmetries. This is the case of the addition constraint x1+x2=x3 or the multiplication x1*x2=x3. The addition and multiplication constraints for matrices such as A+B=C or A*B=C also contain many hyperoctahedral symmetries. In robotics, many specific geometrical constraints such as for instance constraints involving distances or angles have hyperoctahedral symmetries. In this talk, I will present an algorithm which will allow us to build minimal contractors with a polynomial complexity associated with constraints with hyperoctahedral symmetries. - 11:45am-12:00pm discussion, break

- 12:00am-1:30pm Lunch, salle 1A422 (salle de réception au dessus du restaurant administratif)
- 1:30pm-2pm Quentin Brateau, « Acoustic source localisation in underwater environment using interval analysis«

The study of underwater acoustic wave propagation is used in many fields. It particularly provides solutions to localization and underwater navigation problems [1, 2]. In these cases, simulation can be a powerful tool for a better understanding of acoustic propagation. These simulations are based on models that rely on simplifying assumptions allowing the numerical resolution [3]. However, these assumptions are sometimes too restrictive and can cause inaccuracies, especially in the simulation of complex scenes. Simulation can also be used to solve more specific problems in underwater environments. For instance, acoustic source localization using receivers in an underwater scene is still a challenging problem and has both civil and military applications. Classical methods are based on the use of acoustic receiver arrays placed in the environment. Assuming a normal modes model for the propagation, collected data are then processed, for example, by SVD based approach [4] or matched field processing [5], which provides probabilistic results. The proposed approach to solve this problem is to use set theory. The method is to use simulated acoustic amplitude to solve the source localization problem. Using interval analysis, all possible source positions compatible with the recorded hydrophone signal can be enclosed [6]. In addition, possible sets for source position compatible with each receiver can be intersected to increase the certainty of the source location. Besides requiring a good knowledge of the scene, this method requires simulating the acoustic propagation as well as possible to correctly solve this localization problem. A comparative study is carried out on different models that allow the simulation of acoustic propagation, and a suitable model is chosen for the study. Simulated results are used to localize the acoustic source by using interval analysis that provides guaranteed results. The robustness of the proposed method against noise and measurement errors is assessed and discussed. - 2pm-2:15pm discussion, break

- 2:15pm-2:45pm Elena Ivanova, « Efficient Synthesis of Controllers using Symbolic Models »

Abstract: The first part of the talk will be dedicated to a control synthesis for cyber-physical systems using abstraction-based control synthesis approaches. These approaches first create a finite-state abstraction (or a symbolic model) for a continuous or hybrid system and then refine the controller synthesized for the abstraction to a controller for the original system. Abstraction-based control synthesis techniques allow us to handle complex dynamics of CPS models and non-trivial specifications but suffer from poor scalability. I will talk about how to improve the efficiency of ABS approaches when safety specification is considered. The second part of the talk will be dedicated to ongoing research on efficient approximations of the reachable sets.

- 2:45pm-3:00pm discussion, break

- 9:30pm-9:45am Welcome (again), coffee break