Bonjour, Vous êtes tous cordialement invités à assister au séminaire qui aura lieu le mercredi 2 juillet 2008 à 14 heures en Amphi 4 (KB). ----------------------------------------------------------------------- Le programme : *Olena, Vérification du Locuteur et Spot* http://publis.lrde.epita.fr/Seminar-2008-07-02 OLENA 14h00 : Cartes de distances -- Etienne Folio 14h30 : Les types de couleur dans Milena -- Caroline Vigouroux VÉRIFICATION DU LOCUTEUR 15h00 : Système de discriminants linéaires pour la vérification du locuteur -- Antoine Legrand SPOT 15h45 : Traduction d’une LTL étendue en TGBA dans Spot -- Damien Lefortier 16h15 : Front-end Promela dans Spot -- Guillaume Sadegh ----------------------------------------------------------------------- Les Résumés des exposés : ************************** OLENA Cartes de distances -- Etienne Folio Une carte de distances est une représentation sous forme d’image d’une fonction distance à un objet. Ces cartes sont utilisées dans de nombreuses applications, en particulier en analyse d’images de documents qui nous serviront d’illustration. Certaines méthodes de calcul de cartes moins génériques que d’autres peuvent s’avérer plus rapides : par exemple, des cartes calculées par propagation de fronts permettent de déterminer des plus courts chemins mais ne fonctionnent que lorsque le support est connu pour être non-convexe. Cette présentation fait un tour d’horizon des différents algorithmes de calculs de cartes de distances, met en évidence leurs atouts et faiblesses et explique les choix retenus. Les types de couleur dans Milena -- Caroline Vigouroux Le projet Olena fournit une bibliothèque générique pour le traitement d’images, Milena. Nous voulons que cette bibliothèque procure de nombreux types de valeur tels que l’utilisateur puisse toujours choisir le type adapté pour son application. Par exemple, nous fournissons de nombreux encodages en niveau de gris, de nombreux espaces de couleur, etc. Nous présentons la manière dont nous mettons en oeuvre les types de couleurs dans Milena. Il existe différents espaces de couleur (RGB, HSI, et bien d’autres) et il existe plusieurs encodages possibles pour les mêmes espaces de couleur (rgb_3x8, rgb_f, etc.). Nous voulons rendre les choses plus faciles pour l’utilisateur. Donc, notre objectif est de rendre possible l’utilisation des espaces de couleur sans se soucier des mécanismes internes. Par exemple, dans les formules de conversion, on ne veut pas faire apparaître les détails d’implémentation (division par 255). VÉRIFICATION DU LOCUTEUR Système de discriminants linéaires pour la vérification du locuteur -- Antoine Legrand Dans la reconnaissance du locuteur, les modèles GMM occupent une place très importante dans le développement des systèmes performants. Les méthodes de discrimination linéaire à base de SVM donnent actuellement de meilleurs résultats. On s’intéressera ici à un système de discriminant linéaire (le SVM-GLDS). Celui-ci utilise directement, sans passer par un modèle GMM, des statistiques issues de l’ensemble des paramètres de la parole pour définir le modèle de reconnaissance. On évaluera les performances d’un tel système sur la base de données NIST-SRE en le comparant avec les autres systèmes à base de SVM-GMM. SPOT Traduction d’une LTL étendue en TGBA dans Spot -- Damien Lefortier Spot repose sur l’approche automate du model checking. La bibliothèque permet de vérifier des propriétés exprimées en logique temporelle à temps linéaire (LTL) sur une modélisation d’un système représentée par un automate de Büchi généralisé basé sur les transitions (TGBA). Spot propose actuellement deux algorithmes de traduction de LTL en TGBA, une des deux étapes principales de l’approche automate. Nous présentons une nouvelle traduction en TGBA d’une logique LTL qui a été étendue en y ajoutant des opérateurs représentés par des automates finis. Cette traduction permet à Spot de vérifier des propriétés qui n’étaient pas exprimables auparavant. Front-end Promela dans Spot -- Guillaume Sadegh Spot est une bibliothèque de model checking. Pour vérifier des modèles, Spot utilise un format d’entrée représentant des automates de Büchi généralisés basés sur les transitions (TGBA). Ce format est peu pratique pour des utilisateurs, par son manque d’abstraction et par la taille des automates à représenter, souvent composés de millions d’états. Promela (Process Meta- Language) est un langage de spécification de systèmes asynchrones, utilisé par le model checker Spin. Il permet de représenter des systèmes concurrents dans un langage impératif de haut niveau. Nous allons présenter plusieurs approches pour l’ajout d’un front-end Promela dans Spot, qui devront permettre une exploration à la volée du graphe d’états, afin d’éviter de conserver en mémoire tous les états. -- Daniela Becker