LRDE Alumni Seminar: 30 juin 2004, EPITA, Salle Formation (Paritalie 5ème étage)

14h00 : Introduction à l'approche automate pour la vérification de propriétés LTL -- AlexandreDuretLutz (LIP6, équipe Systèmes Répartis Coopératifs)

Le terme model checking regroupe plusieurs techniques de vérification formelle. Ces techniques permettent de vérifier de façon entièrement automatique que l'ensemble des comportements possibles d'un système vérifie une propriété donnée.

La première partie de cet exposé présentera l'approche automate du model checking pour des propriétés exprimées en logique temporelle linéaire (LTL). Cette approche (vieille de 20 ans) s'appuie sur des automates de Büchi, qui sont des automates reconnaissant des mots de longueur infinie.

Dans une seconde partie on montrera comment traduire une formule LTL en un automate de Büchi. La construction s'appuie sur la méthode des tableaux, qui à l'origine est une technique de preuve utilisée en logique depuis 50 ans.

Transparents.

15h30 : Segmentation d'images d'histologie par contours actifs sous l'influence de contraintes de formes et de textures -- SylvainBerlemont^? (Institut Pasteur, Laboratoire d'Analyse d'Images Quantitative)

Le domaine de l'analyse d'images biologiques introduit de nouvelles problématiques en segmentation et reconnaissance des formes. En particulier, les objets d'intérêt ne présentent généralement pas de contours nets; par conséquent, les approches traditionnelles par détection de contours basées sur le gradient de l'image échouent.

Plus récemment, des méthodes variationnelles de contours actifs qui ne dépendent pas du gradient ont vu le jour. Le modèle initial, Active Contours Without Edges [Chan2001], sépare deux classes sans connaissance a priori sur celles-ci. La minimisation de la fonctionnelle de Mumford-Shah (sur laquelle ce modèle est basé) devient un problème de recherche d'un front de courbure minimale.

Dans cette approche, le formalisme des Level Sets [sethian87] est utilisé pour modéliser le front d'évolution. A la différence des méthodes plus classiques de contours actifs paramétriques [kass88], ce formalisme a l'avantage d'accepter des changements de topologie implicites et ainsi, détecter un nombre a priori quelconque d'objets. De plus cette méthode ne dépend pas de l'initialisation du front.

Ici, nous étudions la possibilité d'ajouter à la fonctionnelle des termes de contraintes de forme et de texture pour orienter la détection vers des structures spécifiques.

16h30 : Evolution d'un controleur neuronal pour un animat volant ailes battantes -- JeanBaptisteMouret^? (LIP6, AnimatLab)

Ce travail se place dans le contexte de l'approche animat, visant à la synthèse d'agents simulés ou de robots dont les lois de fonctionnement sont autant que possible inspirées de celles des animaux. Jusqu'à présent, la majorité des travaux autour de cette approche s'est concentrée sur la réalisation ou la simulation de robots roulants, marcheurs, ou nageurs. Cependant, une part non négligeable du règne animal est actuellement à peine explorée : celle des animaux volants.

Les oiseaux sont capables à la fois d'effectuer du vol stationnaire, comme les hélicoptères, et de planer, tels des planeurs. De nombreuses applications pour un oiseau artificiel sont, par conséquent, envisageables. Le projet Robur, dans lequel ce travail s'inscrit, s'intéresse à l'application de l'approche animat aux oiseaux, en tentant de comprendre et reproduire les mécanismes neuronaux et cognitifs mis en jeu pour le vol à ailes battantes.

Quatre grandes problématiques sont abordées dans le cadre de ce travail :

• la compréhension des mécanismes permettant le vol à ailes battantes et des méthodes permettant de les reproduire sur un oiseau artificiel;
• la mise au point de fonctions d'adaptation (fonctions de fitness) permettant de créer des contrôleurs pour animats à ailes battantes en utilisant des algorithmes évolutionnistes;
• l'évolution à l'aide d'un algorithme génétique multi-critères de réseaux de neurones à dynamique interne générant des comportements rythmiques;
• l'utilisation de tels réseaux de neurones pour contrôler un animat à ailes battantes.

Après avoir décrit les principes du vol à ailes battantes, nous présenterons les grandes lignes constituant les algorithmes génétiques multi-objectifs et leur application à l'évolution de réseaux de neurones. Une fonction d'apdatation, basée sur des critères aérodynamiques, permettant l'évolution de contrôleurs de vol utilisant des fonctions sinusoïdales sera ensuite présentée. Ces contrôleurs doivent permettre à un oiseau artificiel simulé de voler horizontalement à vitesse constante. Cette fonction d'apdatation sera complétée pour être utilisée pour l'évolution d'un contrôleur neuronal générant un rythme adapté au maintient de l'animat à l'horizontal à vitesse constante. Nous concluerons en évoquant les nombreuses perspectives offertes par ce travail et le projet Robur.
to top