[Annonce] [Séminaire LRDE] : mercredi 7 juin 2006

Bonjour, Vous êtes tous cordialement invités à assister au séminaire qui aura lieu le mercredi 7 juin à 14 heures en amphi P01 (KB). ----------------------------------------------------------------------- Le programme : *BDD, ALGORITHMES GENETIQUES & MARKOV* http://www.lrde.epita.fr/cgi-bin/twiki/view/Publications/Seminar-2006-06-07 BDD 14h00 : BDD distribués et Java -- Guillaume Guirado 14h30 : Répartition des DDD en Erlang -- Samuel Charron ALGORITHMES GENETIQUES 15h00 : Programmation génétique & Corewar -- Jérémy Marc MARKOV 15h45 : Vérification du locuteur -- Charles-Alban Deledalle 16h15 : Model-checking qualitatif approché -- Jean-Philippe Garcia Ballester 16h45 : Chaînes de Markov continues en présence d'incertitudes -- Nicolas Neri ----------------------------------------------------------------------- Les Résumés des exposés : ************************* BDD * BDD distribués et Java -- Guillaume Guirado Les BDD (Diagrammes de Décision Binaires) ont été très largement étudiés depuis leur introduction à la fin des années 80. De très nombreuses implémentations ont d'ailleurs été proposées. Cependant, rares sont les bibliothèques permettant de distribuer notre diagramme sur un cluster. Partant de ce constat, l'implémentation, dans un langage moderne, d'une bibliothèque de gestion de BDD permettant la répartition sur un grand nombre de machines est nécessaire. Cela permettra d'augmenter considérablement la mémoire disponible, et donc de résoudre des problèmes plus complexes. Pour cela, nous avons choisi le langage Java. Durant la présentation, nous verrons les principales propriétés des BDD et leurs opérations. Ensuite, nous analyserons les résultats d'une implémentation non répartie, avant de finalement exposer les choix, forces et faiblesses, de notre bibliothèque répartie. * Répartition des DDD en Erlang -- Samuel Charron Les DDD (Data Decision Diagrams) généralisent le concept de BDD, en permettant de ne pas se limiter aux fonctions booléennes. Cependant, ils n'apportent pas de solution supplémentaire au problème de mémoire. La répartition de BDD a déjà été longuement étudiée sans donner de résultat réellement satisfaisant. Une étude sur les propriétés des DDD nous a permis de réaliser la répartition. Nous utilisons pour cela Erlang, un langage intégrant des primitives de communications et de parallélisation Lors de ce séminaire, nous vous présenterons les DDD. Ensuite, une introduction à Erlang et a l'implémentation réalisée sera effectuée. Enfin, nous comparerons plusieurs algorithmes de répartition existants sur les BDD en y ajoutant d'autres algorithmes nouveaux. ALGORITHMES GENETIQUES * Programmation génétique & Corewar -- Jérémy Marc Les algorithmes génétiques existent depuis les années 80 et constituent une catégorie à part dans l'algorithmique évolutionnaire. Directement inspirés de la nature, ou plus exactement de la biologie, ils ont pour but d'approcher les solutions optimales en faisant varier les paramètres caractéristiques des individus. Lorsque ces individus sont des programmes, qui plus est en assembleur de type Corewar, la tâche devient nettement plus ardue. En effet il devient complexe d'exhiber ces paramètres et difficile de les modifier sans risquer d'altérer considérablement la cohérence de l'individu. Nous présenterons certaines de ces problématiques, puis proposerons plusieurs solutions que nous comparerons et expliquerons. MARKOV * Vérification du locuteur -- Charles-Alban Deledalle La vérification du locuteur consiste à détecter si un segment de parole est réellement prononcé par un individu présumé. Cela est mis en opposition à l'identification dont le but est de reconnaître l'auteur du message. Au cours de ce séminaire nous examinerons trois approches. La première approche, probabiliste (état de l'art), utilise les modèles de mixture gaussienne. Puis nous proposerons deux solutions basées sur les méthodes SVM. La différence entre ces deux dernières se situe au niveau des noyaux et des caractéristiques utilisés. Notre travail s'inscrit dans le prolongement de l'évaluation NIST, et dans le cadre de l'évaluation ISCSLP en cours. * Model-checking qualitatif approché -- Jean-Philippe Garcia Ballester Le model-checking consiste à vérifier certaines propriétés sur un modèle donné. Il existe plusieurs méthodes pour résoudre ce problème, dont une méthode approchée, permettant de réduire le temps de calcul. Cette méthode est quantitative : ce qui nous intéresse est la probabilité que la formule soit vraie. Mais il y a des cas où le qualitatif est suffisant : ce qui nous intéresse est de savoir si cette probabilité est supérieure ou inférieure à un certain seuil. Nous présenterons d'abord le model-checking, et l'algorithme implémenté dans APMC, puis une optimisation de celui-ci dans le cas de la vérification qualitative de propriétés. Nous finirons par des tests, théoriques et expérimentaux. * Chaînes de Markov continues en présence d'incertitudes -- Nicolas Neri Le 26 Mars 2006 lors de la 12e conférence internationale TACAS, Khoushik SEN et al. ont présenté un article sur la vérification de programmes en utilisant les chaînes de Markov finies à temps discret pour lesquelles la probabilité exacte des transitions n'est pas connue. Ce séminaire présentera les travaux en cours sur l'extension de l'algorithme de Khoushik SEN et al. pour les chaînes de Markov à temps continu présentant des incertitudes. Le but sera de trouver un ensemble de variables satisfaisant certaines contraintes et de vérifier la faisabilité de celles-ci grâce à la résolution des BMIs. -- Daniela Becker