Informations
Le lundi soir 20:00 Restaurant à la maison de l'océan. Et non pas le mardi soir comme initialement prévu. Ce restaurant se trouve sur le port, à 10 minutes à pied de la station de tram 'Château'.

Programme

9:30. Accueil café.

10:00. L. Jaulin, B. Desrochers and D. Massé. Slides.
Titre. Bisectable Abstract Domains for the resolution of equations involving complex numbers.
Abstract. The idea of interval arithmetic is to enclose the exact value of a real number inside an interval. Then, computing with intervals will allow us to enclose the true value for a variable we want to compute. In this talk, I recall the importance of having a lattice structure for the set of intervals and show that several interval algorithms could be adapted to other types of domains as soon as these domains have a lattice structure with respect to the inclusion and that we could bisect them. As an illustration, we introduce a new type of domains, the boxpies, which correspond to the intersection between one box and one pie. We show that boxpies can be used efficiently to characterize the solution set of constraints involving complex numbers.

10:30. A. Chapoutot. Slides.
Titre: Vers une formalisation d’un système de suivi de trajectoires
Résumé: L'objectif de cette présentation est une tentative de définir de manière détaillée un exemple de suivi de trajectoires pour une plateforme mobile terrestre. Cette définition s’appuiera sur des modèles mathématiques tels que les systèmes dynamiques contrôlés et des automates hybrides. Cette mathématisation du problème devrait permettre la définition de propriétés à prouver et de lister les possibles moyens techniques et méthodologiques pour effectuer ces preuves.

11:00. T. Le Mézo. Slides.
Title : A new interval approach to solve the Initial Value Problem
Abstract : We propose an original guaranteed interval-based method to compute Initial Value Problem (IVP) for ordinary differential equations (ODE). Our method uses the geometrical properties of the vector field given by the ODE and a state space discretization to compute an enclosure of the trajectories set that satisfies the IVP.

11:30. B. Martin. Slides.
Titre: Calcul du noyau de viabilité par patron de trajectoire cyclique.
Résumé: Une trajectoire cyclique pour un robot est une trajectoire qui partant d'un état initial ramène le robot en un temps non nul dans ce même état initial. D'un point de vue de la viabilité, si il est possible pour un robot d'effectuer une trajectoire cyclique sans rencontrer d'obstacles, alors l'état initial peut être considéré comme faisant parti du noyau de viabilité du robot. L'idée de l'approche présentée ici est d'utiliser un patron de trajectoire cyclique sous la forme d'une fonction g = 0, et d'utiliser un solveur de contraintes par intervalles pour calculer une sous approximation du noyau de viabilité. Le problème en question est un problème de contraintes quantifiées pour lesquels, suivant un ensemble de conditions initiales, va déterminer si toutes les trajectoires induites possibles sont viables. Ce travail préliminaire à également pour but de discuter des extensions possibles comme la génération de patrons de trajectoires où l'amélioration du noyau de viabilité par intégration garantie.

12:15. Repas au self de l'ENSTA Bretagne.

14:00. F. Fages. Slides.
Title: Continuous Valuations of Temporal Logic Specifications with applications to Parameter Optimization and Robustness Measures
Abstract: In computational systems biology, building mathematical models satisfying a specification of the cell behaviours observed experimentally, is a common task of the modeler that techniques like model- checking help solving, in the qualitative but also in the quantitative case. In this talk we go one step further by defining a continuous degree of satisfaction for temporal logic formulae with constraints. We show how such a satisfaction measure can be used as a fitness function with state-of-the-art stochastic optimization methods in order to find biochemical kinetic parameter values satisfying a temporal specification of the behaviour. We also show how it can be used to define a measure of robustness of a biological system with respect to some temporal specification and set of perturbations. We shall conclude on some open issues in formal verification and synthesis of biochemical reaction systems.

14:45 S? Rohou. Slides.
Title : Guaranteed Computation of Robots Trajectories
Abstract: We propose a new method of guaranteed integration based on tube programming. The main idea is to formalize the problem as a constraint network, the variables of which being trajectories. Then, a constraint-based resolution is performed. In the field of mobile robotics, the resulting method is shown to be much simpler and more general than existing approaches dealing with guaranteed integration.

15:15. C. Aubry. Slides.
Title : Loop detection in a robot trajectory, interval based and Kalman approach comparison.
Abstract : Detecting loops in a mobile robot trajectory is an important topic for SLAM (Simultaneous Localization And Mapping). It brings another information to the problem that could help to reduce positioning error when moving back to a known place. This talk will present a method to find loops in a trajectory where only proprioceptive measurement are known. Comparison will be done between an interval method versus a Kalman resolution of the problem. Results will be illustrated on a real robotic experiment.

15:45. B. Martin. Slides.
Titre: Preuve par méthodes algébriques de la viabilité du problème du 'Station Keeping'
Résumé: Cette présentation fait suite à la réunion précédente et à pour but de montrer la finalisation de la preuve par méthodes algébriques de la viabilité du problème illustratif du 'Station Keeping'. En exploitant une reformulation polynomiale du système, un invariant algébrique pour chaque 'mode' de contrôle (fonction rationnelle et fonction logarithmique) a été déterminé. Dans le cas du système avec basculement de mode, l'utilisation de ces invariants et une analyse d'atteignabilité permet de déduire la viabilité du système.

16:15. B. Desrochers. Slides.
Title : Thick set inversion
Abstract : We deal with set inversion in the case where the function f and the set Y to be inverted are both uncertain. The uncertainty is treated under the form of intervals. More precisely, the function f is known to belong to an interval of functions and the set Y is inside an interval of subsets of Rn. The introduction of new tools such as thick intervals and thick boxes will allow us to propose an efficient algorithm to solve the problem. Some elementary test cases that cannot be handled easily by existing method show the efficiency of the approach.

17:00. Visite du club robotique.