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
