Bonjour, nous avons le plaisir de vous inviter au séminaire des étudiants du LRDE. Il aura lieu le mercredi 16 janvier 2013 à partir de 10 heures en Amphi 3 (KB). ----------------------------------------------------------------------- Au programme : SPOT * 10h00 : Réduction par simulation pour les TGBA -- Thomas Badie * 10h30 : Méthodes de réduction par ordre partiel adaptatives -- Pierre Parutto VERIFICATION DU LOCUTEUR * 11h00 : Spherical Discriminant Analysis -- Victor Lenoir CLIMB * 11h30 : Parallélisation de Climb -- Laurent Senta * 12h00 - 14h00 : PAUSE DEJEUNER VAUCANSON * 14h00 : FSMXML pour Vaucanson 2.0 -- David Moreira OLENA * 14h30 : Calcul du flux optique dans des séquences avec des parties manquantes -- Sylvain Lobry * 15h00 : Inpainting rapide préservant la structure -- Coddy Levi Les Résumés des exposés : ************************** SPOT * 10h00 : Réduction par simulation pour les TGBA -- Thomas Badie L'approche par automates du model checking s'appuie traditionnellement sur des Automates de Büchi (BA) qu'on souhaite les plus petits possible. Spot, bibliothèque de model checking, utilise principalement des TGBA qui généralisent les BA. Nous avons déjà présenté une méthode de réduction par simulation (dite directe). Cette technique a permis de produire des automates plus petits que dans les précédentes versions. La simulation consiste à fusionner les états ayant le même suffixe infini. Nous montrons que nous pouvons aussi fusionner ceux ayant le même préfixe infini (c'est la cosimulation). On peut répéter la simulation et la cosimulation pour créer la simulation itérée. Cette méthode est incluse dans Spot 1.0 et est une grande amélioration de la simulation. On expérimente aussi une méthode qui consiste à modifier certaines conditions d'acceptations (appellées sans importances). Puisque celles qui sont sur les transitions entre composantes fortement connexes n'ont pas d'influence sur le langage, on peut les modifier pour aider la simulation. * 10h30 : Méthodes de réduction par ordre partiel adaptatives -- Pierre Parutto Le model checking explicite de systèmes concurrents souffre d'une croissance exponentielle du nombre d'états représentant un système. Les méthodes de réduction par ordre partiel sont un ensemble de méthodes permettant de combattre ce problème. Celles-ci permettent d'ignorer les états redondants lors de la génération de l'espace d'états. Parmi elles, nous avons choisi les algorithmes two phase et ample set comme base pour nos investigations. Ceux-ci ont été implémentés dans Spot, la bibliothèque C++ de model checking développée au LRDE, en utilisant l'interface DiVine. En se basant sur ces méthodes et sur le fait que les algorithmes dans Spot sont calculés à la volée, nous avons défini une nouvelle classe de méthodes appelées méthodes de réduction par ordre partiel adaptatives. L'idée est de se baser sur l'état courant de l'automate de la formule et non sur la formule tout entière. Les résultats obtenus sur notre suite de tests montrent que cette méthode donne de meilleurs résultats que les méthodes d'ordre partiel classiques. VERIFICATION DU LOCUTEUR * 11h00 : Spherical Discriminant Analysis -- Victor Lenoir Le rôle de la vérification de locuteur est de vérifier l’identité présumée d’un segment de parole. Actuellement, les meilleures performances sont obtenues par un mapping de chaque segment de parole d’un locuteur vers un vecteur appelé I-vector. Le score de la vérification de locuteur est calculé par une distance cosine entre ces deux vecteurs représentant chacun un locuteur. Ce rapport décrit une technique de réduction de dimension appelée Spherical Discriminant Analysis (SDA). Les objectifs de cette projection sont de maximiser la distance cosinus entre deux locuteurs différents et de minimiser la distance cosinus entre deux même locuteurs; il a été montré que le sous-espace de la SDA, qui est plus approprié pour la distance cosinus que la Linear Discriminant Analysis (LDA), obtient de meilleures performances en reconnaissance faciale. Nous allons comparer les performances obtenues par la SDA avec celles obtenues par la LDA. CLIMB * 11h30 : Parallélisation de Climb -- Laurent Senta Climb est une bibliothèque de traitement d’image générique développée en Common Lisp. Elle fournit une couche de génécité bas-niveau utiliséee pour définir de nouveaux algorithmes de traitement d’image. Il est aussi possible de créer des chaînes de traitements soit en utilisant un "Domain Specific Language" déclaratif ou bien à l’aide d’une interface graphique. Afin d’améliorer les performances de la bibliothèque, ces différents niveaux peuvent être parallélisés. Nous décrirons les différents aspects de ce processus de parallélisation. Pour chaque niveau, nous détaillons l’implémentation des traitements parallèles, leurs impacts sur l’utilisabilité de la bibliothèque ainsi que les gains de performance obtenus. VAUCANSON * 14h00 : FSMXML pour Vaucanson 2.0 -- David Moreira Vaucanson est une bibliothèque de manipulation d'automates et de transducteurs. La version 2.0 est aujourd'hui en cours de développement et le design a été revu pour avoir des parties statiques et dynamiques. Dans Vaucanson 1.4, les entrées/sorties utilisent intensivement le format XML spécifié par le groupe de Vaucanson, FSMXML. Mes travaux consistent à développer et rafraîchir des spécifications du format présent dans Vaucanson 1.4. Cette mise à jour nous permet la sauvegarde et la lecture d'automates aux Weight Sets particuliers tels que des expressions rationnelles ou même des automates pondérés. OLENA * 14h30 : Calcul du flux optique dans des séquences avec des parties manquantes -- Sylvain Lobry Calculer le flux optique peut être un premier pas vers l'inpainting vidéo. Pour cette application, nous devons manipuler des séquences avec des zones manquantes, celles à inpainter. Le flux optique peut être calculé de manière locale ou globale. Les méthodes globales ont généralement de meilleurs résultats. Dans le cas de séquences avec des zones manquantes, les méthodes globales ne peuvent pas être utilisées de manière directe à cause du manque d'informations dans ces régions. Nous présentons une méthode combinant des algorithmes locaux et globaux afin de calculer le flux optique dans ce type de séquences ce qui nous permet d'inpainter efficacement et simplement des vidéos. * 15h00 : Inpainting rapide préservant la structure -- Coddy Levi Le texte sujet à extraction via l'analyse de document peut être présent dans deux formes : foncé sur fond clair ou clair sur fond foncé, appelé Inverse Video. Nous présenterons les problématiques liées à l'extraction de l'inverse video dans Scribo en utilisant la chaîne de traitement déjà existante, les problèmes ainsi introduits et les pistes explorées pour l'amélioration des résultats. -- Daniela Becker Responsable administrative du LRDE