Abstract
From LRDE
.
La vérification de modèle vise à vérifier qu'un système répond à la spécification donnée en explorant tous ses états possibles. Pour y parvenir, il existe plusieurs techniques. Le Multi-Core Nested Depth-First Search (CNDFS) a un faible besoin en mémoire et fonctionne bien avec les automates de Büchi les plus simples. La Multi-Core On-The-Fly SCC Decomposition (UFSCC) a un besoin en m'moire plus important et fonctionne bien avec les automates de Büchi généralisés. La méthode symbolique a un besoin en mémoire plus faible mais dépend beaucoup de l'ordre des variables. Les performances de ces algorithmes peuvent être très différentes et choisir le meilleur en fonction d'un modèle spécifique sans les tester tous n'est pas quelque chose de facile. Ici, nous essayons d'utiliser de l'apprentissage automatisé pour prédire la meilleure méthode à utiliser pour un modèle donné. Pour celanous entraînons une forêt aléatoire, une méthode d'apprentissage d'ensemble qui utilise une multitude d'arbres de décision, en utilisant seulement les premiers états de l'espace d'état. +
... Insert an abstract in French here ... +
A
Spot is an extensible model checking library using transition-based generalized Büchi automata (TGBA). It contains many state-of-the-art algorithms. In this paperwe focus on two algorithms that create automata with more transitions than necessary. These constructions can be enhanced by computing a feedback arc set (FAS): a set of edges which, when removed from the graph, leave a directed acyclic graph. Ideally, we want a minimal FAS, but this problem is NP-hard. We adapted and improved a heuristic proposed by Eades et al. that approximates a minimal FAS in linear time. We show that the integration of this heuristic in the complementation of deterministic Büchi automata and in the conversion of Rabind automata to Büchi automata reduces the size of the output up to 31% in our experiments. These results depend greatly on the number of cycles and accepting states in the input automaton. +
Spot is a C++ library for model checking. For verification, Spot uses an input-format which describes a Transition-based Generalized Büchi Automata (TGBA). However, this format doesn't seem accessible for users with its poor abstraction and the need for often representing automaton with millions of states. Promela (Process Meta-Language) is a verification modeling language used by the Spin model checker. It lets users to describe a parallel system for verification in a high level programming language. We will present different ways to add a Promela front-end in Spot, which will allow to explore the state-graph on-the-fly, in order to avoid storing all the states. +
Thanks to the HOA format there are less and less barriers between '"`UNIQ--math-00000005-QINU`"'-automata with different acceptance conditions. Spot, a library for '"`UNIQ--math-00000006-QINU`"'-automata manipulation, supports arbitrary acceptance condition and performs some conversions between them. We augmented the set of supported acceptance conversions with new algorithms that convert (when possible) all common classes of non deterministic '"`UNIQ--math-00000007-QINU`"'-automata to deterministic co-Büchi. Boker and Kupferman solved this conversion whith asymptotically tight constructions. We implement their methods with some optimizations and adjustments: we made it work with Streett-like acceptance, any acceptance in disjunctive normal form (including Rabin-like) and also transition-based acceptance. Using these conversions gives a new way to check whether an LTL formula is a persistence formula. +
Image recognition main objective is to enable computers to recognize shapes without needing any human intervention. However, one problem in this field is automatic recognition regardless to image transformations like rotation or scales changes. Image invariants based on moments have received a particular attention since they respect fully or partially the constraints listed above. Various shape-based invariant algorithms are popular in Document Image Analysis and especially for Optical Character Recognition systems since they provide relevant features used to differentiate characters. Nevertheless, they also find an interesting application in Document Layout Analysis by providing information that can be used to distinguish text from non-text elements. Thus, we will introduce the concepts of image invariants and evaluate the performances of six state-of-the-art shape-based image invariants for text / non-text classification. An attempt of an image invariant algorithm inspired from the principle of compressive sensing is also offered. +
For the last few years, connected operators have gained a certain popularity in image processing field, they have been widely used for filtering, image segmentation, object detection...However, they encountered several issuesthe most important being contrast dependence, one can only retrieve either dark or bright objects. Auto-dual operators allow computation on dark and bright components in the same time and as a consequence, do not suffer from the drawback of classical connected operators. Howeverauto-dual operators are more difficult to implement and current algorithms are computationally expensive. We propose a new algorithm to compute auto-dual operators based on Tarjan's union-find which is faster that current state-of-the-art contour tree algorithms. +
Spot is a model checking library centered around the automata-theoretic approach, and can be used to verify properties expressed using LTL (Linear Temporal Logic) formulæ on models represented as TGBA (Transition-based Generalized Büchi automata). The library offers three algorithms to translate LTL formulæ to TGBA, one of the main stages of the approach. We present a forth translation algorithm introduced by Tauriainen which uses TAA (Transition-based Alternating Automata) as an intermediate representation. We also compare it to the three algorithms already present in Spot. +
The Tree of Shapes is an useful image transform used to process digital images in a self-dual way. We recently introduced a new algorithm to compute this tree in '"`UNIQ--math-00000005-QINU`"'-dimensional gray scale images with a quasi-linear time complexity. However, no proof nor benchmark were given. In addition, this algorithm requires to increase dramatically the size of the input image. Such increase comes with an important cost in term of memory usage and computation times. We discuss the initialization of the algorithm and provide a proof. We also address its memory and computation time issues when used on two dimensional images. +
This report focuses on an active learning algorithm for the class of visibly one-counter automata,and its implementation in python and C++. The algorithm allows creating such automata using queriesto a teacher, with no knowledge on the final automaton. We then discuss the possible improvements of the algorithm regarding the algorithm execution speed and the automaton represention. We also give an overview of how benchmarks could be perform on such a semi-automatic program. +
Vaucanson est une bibliothèque C++ de manipulation d'automates finis. Le feedback utilisateur montre que Vaucanson est lent et que l'interface de la bibliothèque qui permet de manipuler les automates directement est complexe. Pour améliorer Vaucanson, l'équipe de développement met en place une interface simplifiée sur la structure de données Automata et réinstaure une modélisation saine de l'implémentation sous-jacente. Une conséquence de ces changements est que les algorithmes disponibles dans Vaucanson doivent être adaptés à la nouvelle interface. L'adaptation de ces algorithmes donne l'opportunité d'étudier l'impact des changements récents sur les performances et l'accessibilité de Vaucanson. Grâce à la simplicité de la nouvelle interface, les optimisations possibles deviennent plus visibles. +
Le principe d'un algorithme de ligne de partage des eaux est de partionner en régions (bassins) une image en niveaux de gris. Plus particulièrement, l'algorithme de "watershed cut" opère des coupes dans un graphe formé à partir d'une image et dont les arêtes sont valuées. Une premiére approche a été de considérer l'image comme un graphe 4-connexe dont les sommets sont les pixels. Il est alors apparu que cette approche pouvait masquer des minima locaux. Une seconde solution, à base de complexe simplicial, a donc été étudiée. Ce travail de recherche utilise la bibliothèque Milena, la bibliothèque générique de traitement d'images en C++ développée au laboratoire. +
The main purpose of the watershed algorithm is to segment a gray-level image into regions (basins). More specifically, the "watershed cut" algorithm performs some cuts in an edge-valued graph built from an image.First we have considered an image as a 4-connected graph, where the vertices represent the pixels. Yet we have noticed that this representation can miss some local minima. A second approach, based on a simplicial complex, has been studied. This work relies on Milena, the generic C++ library dedicated to image processing library developed at the LRDE. +
La conception des automates dans Vaucanson occupe une place centrale concernant la généricité de la bibliothèque. Nous voulons pouvoir étendre cette modélisation pour supporter de nouveaux types et spécialiser des comportements afin d'améliorer les performances. L'introduction récente du concept de kind à la bibliothèque ainsi que la définition d'une nouvelle interface des automates ont pour objectifs de rationaliser les structures de données déjà présentes dans Vaucanson, comme les graphes utilisant Boost Multi Index. Le kind d'un automate est le type d'étiquettes qu'il porte sur ses transitions, une lettre ou un mot par exemple. L'utilisateur peut alors, à travers une hiérarchie d'itérateurs respectant la nouvelle interface, itérer de manière efficace sur les transitions portant une occurrence de ce kind spécifié comme prédicat (itérer sur les transitions portant la lettre a par exemple). Le gain est visible car l'utilisateur était contraint d'itérer sur le support d'un polynôme avant ces améliorations. +
Vaucanson is an extensive C++ library for the manipulation of finite state machines. User feedback shows that Vaucanson is slow and that the library interface for direct automaton manipulation is complex. To enhance Vaucansonthe development team is making major changes to simplify the interface over the Automata data structure and reinstate a sane modeling for the underlying implementation. A consequence of these changes is that the algorithms available in the Vaucanson library must be adapted to the new interface. Adapting algorithms is an opportunity to study the impact of the recent interface and implementation changes on performance and accessibility. Because the new interface over automata is simplerpossible optimizations are more apparent. +
The design of automata in Vaucanson plays a central role concerning the genericity of the library. We want to be able to extend the model to support new types and to specialize behaviours in order to improve performances. The recent introduction of the kind concept in the library together with the definition of a new automata interfaceare targeting the rationalisation of already existing data structures in Vaucanson — Boost Multi Index based graphs for example. The kind of an automaton is the type of the labels on the transitions like a letter or a word. Through an iterator hierarchy respecting the new interface, the user can efficiently iterate over the transitions labeled by a specific occurrence of the kind specified by a predicate — iterating over all the transitions labeled by an '"`UNIQ--math-00000005-QINU`"' for example. The gain is noticeable because the user had no choices but to iterate over a polynomial before those improvements. +
Explicit model checking of concurrent systems suffers from the exponential blow-up in the number of states of the represented system. The partial order reduction methods are a set of methods to tackle this problem. They act by preventing the generation of redundant states while creating the state space. Among all these methods are the two phase and ample set algorithms that serve as the basis for our investigations. We implemented those algorithms in Spot, the C++, model-checking library developed at the LRDE, using the Divine interface. Building on these classical methods and taking advantadge of the on-the-fly property of Spot's algorithms, it is possible to devise a new class of methods called adaptive partial order methods that use the current state of the formula automaton and not the whole formula. This new method gives better results than the classical partial order methods on our test suite. +
Contract programming is a paradigm that allows developers to ensure that some conditions are satisfied when a function is called (preconditions), or when it returns (postconditions). It makes debugging easier and it is a good way to document what a function accepts as argument or ensures on the result. In oriented-object languages, it is also possible to check a set of conditions on every call and return of any member function of a class (class invariants), and conditions are inherited from parent classes. The Transformers project aims at providing source to source transformations on C and C++ sources. A C extension to support contracts in C has already been written, when C++ parsing wasn't working yet. We will show how to write a C++ grammar extension to bring contracts in the C++ with the Transformers project, and then how to transform this extended C++ into standard C++. +
La programmation par contrats est un paradigme permettant de réduire le temps de débogage des programmes, en spécifiant des conditions qui doivent être vérifiées à l'entrée d'une fonction (emph préconditions) ou à sa sortie (emph postconditions). Dans les languages orientés objet, il est également possible de vérifier un ensemble de contraintes à chaque appel ou sortie d'une fonction membre (invariants de classe), et les conditions sont héritées à partir des classes parentes. Le projet Transformers a pour but de faire de la transformation source à source sur des sources C et C++. Une extension pour introduire les contrats dans le C a déjà été écrite alors que l'analyse syntaxique du C++ n'était pas encore fonctionnelle. Nous allons montrer comment écrire une extension de la grammaire du C++ dans le projet Transformers pour introduire le principe de contrat dans le C++, puis transformer le code étendu en C++ standard. +
Les transducteurs sont utilisés dans beaucoup de contextes, comme la reconnaissance de parole ou le calcul de la similitude entre proteines. Cette recherche montre l'implémentation dans Vcsn de plusieurs algorithmes permettant de manipuler des transducteurs afin de résoudre ces problèmes. Tout d'abord, un algorithme permettant de transformer un transducteur en automate pondéré qui peut être facilement évalué est présenté. L'algorithme de synchronisation a ensuite été implémenté, ce qui a amené au calcul du transducteur des distances d'édition, et son évaluation. +
Transducers are used in many contexts, such as speech recognition or in order to measure the similarity between proteins. This research shows the implementation in Vcsn of several algorithms allowing to manipulate the transducersand thus solve these problems. First an algorithm to transform a transducer into a weighted automaton that can be easily evaluated is presented. The synchronization algorithm was then implemented, leading to the computation of the edit-distance transducer and its evaluation. +
Nash equilibria computation in finite games is a problem which is known to be PPAD-complete, which means it currently seems impossible to find an efficient solution ; worst case complexity of well known algorithms is in '"`UNIQ--math-00000007-QINU`"' for any game of size '"`UNIQ--math-00000008-QINU`"'. For this reasonresearch in this domain currently focuses on '"`UNIQ--math-00000009-QINU`"'-equilibria, situations which approximately satisfy the conditions of a Nash equilibrium. The emphFictitious Play algorithm fits in this approach. At each iteration of this algorithm, each of the players “strengthens” the strategy that has the highest utility in the current context. For some specific game classes this algorithm converges to a Nash equilibrium, therefore providing an efficient approximation method. However, convergence can only be proved for a small amount of game classes. It is therefore useful to study other algorithms (based on Fictitious Play) in order to find other convergence cases. In this study, we will focus on the alternate Fictitious Play algorithm, in which only one player at a time strengthens one of his strategies : the player which is the “further” from his maximum payoff. +
Alternating automata add a universal branching to the existential branching from non-deterministic automata. Büchi alternating automata are exponentially more concise than non-deterministic Büchi automata. Additionally, they are well suited to translate linear temporal logic as their size is proportional to the translated formula. This work aims to add alternating automata support to Spot. This will make Spot compatible with other tools producing or using aternating automata, and allow future algorithms working on alternating automata to be implemented. +
Une des parties d'une chaîne de reconnaissance de caractères est la classification des caractères à proprement parler : ils peuvent être en majusculesminuscules ou bien être des chiffres. Dans notre casnotre OCR calcule un descripteur à base d'ondelettes pour chacune des images de caractère. Ce sont ces descripteurs que nous classifions. L'étape de classification est actuellement basée sur un algorithme des k plus proches voisins (k-NN) multi-classe. Sachant que l'étape d'évaluation dépend fortement de la taille de la base d'entraînement, cette dernière peut être modifiée afin d'améliorer les scores. Notre travail se concentre sur ces possibles améliorations de la base d'entraînement. vspace*1.05cm +
Vaucanson est une bibliothèque dont un des buts est de permettre un accès facilité à des automates et aux algorithmes qui leur sont associés. Elle met donc à notre disposition plusieurs algorithmes standard (et d'autres moins conventionnels) tels que la déterminisation, le calcul des états accessibles etc. L'un de ces algorithmes est la composition de transducteurs. Celui-ci n'est pas d'une nature aisée à aborder et son implémentation dans Vaucanson est perfectible. Améliorer l'implémentation d'un tel algorithme est alors un bon moyen de mettre à l'épreuve certains choix de conception dans Vaucanson. +
Spot est une bibliothèque de model checking developée au LRDE. Sa force est d'utiliser les Automates de Büchi Generalisés basés sur les transitions (TGBA), plutôt que les Automates de Büchi basés sur les Transitions (TBA) très utilisés dans les autres model checkers. Les TGBA nous permettent de produire des automates très petits représentant une formule rendant toutes les étapes suivantes du model checking plus rapide. Comme Spot met l'accent sur l'utilisabilité et la personnalisation des outils, une attention particulière est portée sur l'interfaçage avec d'autres programmes. La question de transformer un TGBA en TBA (appelé dégeneralization) sans perdre en performance est donc centrale. Cette présentation a pour but de montrer une analyse des outils de dégénéralisation présents dans Spot et de proposer des moyens pour les améliorer. +
En vérification formelle à l'aide d'ω-automates, la construction d'automates plus petits réduit beaucoup le temps d'exécution et la consommation mémoire d'opérations coûteuses telles que le produit synchronisé. La minimisation d'ω-automates étant un problème NP-complet, nous concentrons notre travail sur les opérations de réduction. Spot possède déjà une méthode de réduction par simulation fonctionnant pour tous les automates existentiels ayant n'importe quelle condition d'acceptation. Cette méthode utilise une simulation à un pas reposant sur la signature des états. L. Clemente et R. Mayr proposent une méthode de réduction par simulation à n pas ne fonctionnant que pour les automates de Büchi et montrent que l'augmentation de ce nombre de pas peut améliorer la réduction. Nous essayons une généralisation de l'opération de réduction existante dans Spot pour qu'elle fonctionne avec des simulations à n pas reposant sur la signature des états. Nous présentons également comment étendre la réduction existante afin qu'elle fonctionne également pour les automates alternants. +
Calculer le flux optique a de nombreuses applications telles que l'estimation de mouvement ou un premier pas vers l'inpainting vidéo. L'équation du flux optique ne peut pas être résolue telle quelle à cause du problème de fenêtrage (deux inconnues pour une seule équation). Un ensemble d'algorithme essaie de résoudre cette équation en se basant sur une stratégie globalec'est-à-dire en essayant d'avoir des petites variations dans le flux. Le premier d'entre eux est l'algorithme d'Horn-Schunck. Celui-ci, même s'il marche dans de nombreux cas, a plusieurs inconvénients, y compris celui d'être lent et de ne pas pouvoir trouver les grands déplacements. Dans le but de résoudre ces problèmesplusieurs stratégies ont été développées. Nous présenterons la méthode et analyserons les bénéfices apportés en appliquant une stratégie multi-échelle à l'algorithme d'Horn-Schunck. +
Vaucanson 2 est une jeune plate-forme de manipulation d'automates née des cendres de Vaucanson. Ce redémarrage à zéro a été fortement encouragé par quelques problèmes de conception : difficultés à gérer trop de templates et trop de niveaux d'imbrication de ceux-ci, qui tendent à obfusquer le code quand les concepts templates ne sont pas clairement définis ; des limitations de performances due à une approche de "généralisation" ; etc. Vaucanson 2 entend apprendre des erreurs de son prédecesseur, et dans ce but, un vrai travail de conception doit être fait. Les templates doivent être utilisés pour la performance (évitant un usage abusif de fonctions virtuelles) afin de pouvoir préférer la généricité plutôt que la généralité, tout en conservant une flexibilité lors de l'exécution. Vaucanson 2 prétendra aussi à une compilation dynamique de code (types d'automates et algorithmes) et de le charger en tant que bibliothèque dynamique. Ces simples problèmes amènent à des architectures de distribution complexes et d'effacement de type, qui doivent être testés dans un environnement simulé. +
L'algorithme de Safra permet de construire des automates de Rabin déterministes à partir d'automates de Büchi non-déterministes. Il existe une variante à cette méthode qui permet de construire des automates à parités déterministes. Cependant, ces méthodes produisent des automates avec 2^O(nlogn) états. Il existe des améliorations qui permettent de réduire le nombre d'états dans beaucoup de cas. Nous présentons deux nouvelles stratégies pour aider à réduire le nombre d'états final. La première stratégie utilise les composantes fortement connexes et utilise cette information pour suivre des chemins de Safra différents. La deuxième stratégie utilise l'information retournée par la bisimulation pour retirer des états équivalents. Ceci permet d'éviter de parcourir plusieurs chemins équivalents et ainsi de réduire le nombre d'états final. On montre que nos stratégies permettent souvent de construire des automates déterministes avec moins d'états et que ces automates reconnaissent toujours le même language. On donne des benchmarks pour voir le gain apporté par nos stratégies et on utilise un outil appelé ltl2dstar qui produit des automates de Rabin déterministes à partir de formules LTL pour comparer nos résultats. +
We propose a new edge-based method dedicated to image segmentation. The last few years have shown the development of image processing with connected filters. Indeedcontour-preserving properties of connected operators are highly desired for image segmentation. The connected operators-based segmentation methods usually proceed in two steps. They first compute an attribute on the connected components and filter the components of which attribute do not satisfy a criterion. In these methods, attributes are actually computed on the pixels of connected components. We propose a new union-find based algorithm that enables evaluation of attributes on connected component edges so that we can finally compute an attribute on their contours. We therefore introduce edges-based attributes and propose some of them that evaluate a connected components energy. We finally perform an edge-based attribute filtering to produce a new image segmentation method. +
Probabilistic model checkers usually rely on deterministic automata as the uniqueness of each path simplifies the probabilistic calculation. Unfortunatelythere are not many LTL translators that produce deterministic automata. Moreover, the automata produced by Spot, a model checker library, are not always deterministic. A classical powerset construction cannot always determinize '"`UNIQ--math-00000003-QINU`"'-automata. However, by memorizing the accepting paths, Safra's construction is able to convert a nondeterministic Büchi automaton into a deterministic Rabin automaton. This change of acceptance condition is necessary as deterministic Büchi automata are less expressive than the nondeterministic version. By implementing this construction, Spot will be able to determinize any automata and compute its complement. In this report, we will see how to efficiently implement the Safra construction and how to expand it to also determinize transition-based generalized Büchi automata. +
SCOOL is a domain-specific language (DSL) designed to make high-level C++ development easier. Based on SCOOP, a paradigm mixing generic and object-oriented programming, it features static resolution of member function calls and powerful concept checking. Previously, a standard container library had been made in pure C++ using SCOOP. Howeverthis implementation required high control of the C++ techniques of SCOOP. With SCOOL, we can achieve this by leaving the hard work to the C++ translator. Focusing on the development of the library with SCOOL and the essential changes to the language and its compiler, we will compare the native and DSL solutions and assess that SCOOL is well-fitted for generic application prototyping. +
Cxx has achieved to support classic object-oriented and generic programming, but some modelisation problems remain recurrent and difficult to solve. Scoop is a static Object-Oriented paradigm. The paradigm provides virtual methods, argument covariance, virtual types and multi-methods statically typed without extending the language. Scoop uses its own Cxx library in order to make easier to design a library with this paradigm. +
FIXME +
FIXME +
L'extraction des différentes structures d'un document numérisé se base sur la mise en place d'une chaîne de traitements constituée d'un certain nombre d'étapes primordiales afin d'optimiser la qualité du rendu final. L'étude de la mise en page du document, à savoir la localisation des lignes de texte et des paragraphesconstitue le coeur même de la chaîne puisque le rendu obtenu est étroitement corrélé avec les zones de texte données en entrée à l'OCR. Ainsi, nous présenterons une méthode hybride d'analyse de mise en page développée dans le cadre du projet SCRIBO. +
Vaucanson est une bibliothèque C++ de manipulation d'automates finis. Par rapport à son concurrent principal, OpenFST, Vaucanson souffre d'importants problèmes de performances. Afin d'améliorer les performances de Vaucanson, il est nécessaire d'avoir des outils appropriés pour analyser le comportement de la bibliothèque en termes d'utilisation de temps CPU et de gestion de la mémoire. Jusqu'en Mars 2009, il n'existait pas d'outils de ce type pratiques à utiliser avec Vaucanson. CBS (C++ Benchmarking Suite) est une suite d'outils d'analyse de performances pour projets C++. Ces outils permettent de mesurer, d'afficher, et de comparer l'utilisation de ressources (temps, mémoire), dans un format accessible à l'utilisateur. Ils sont utilisés pour analyser Vaucanson afin de réécrire les algorithmes les moins efficaces. +
L'extraction de structures dans un document numérisé se base sur la mise en place d'une chaîne de traitements constituée de briques élémentaires. L'analyse haut-niveau d'un document nécessite des informations structurelles sur celui-ci et se basera donc sur cette chaîne de traitements. Elle consistera à extraire des informations plus abstraites de nature structurelle sur un document, pour obtenir des "indices" sur la structure du document. À l'aide de ces indices et de schémas de structure, il est ensuite possible de réaliser des traitements de haut-niveau tels que l'identification du flot de lecture, l'extraction d'éléments spécifiques ou la reconstruction d'un document dans un autre format. +
La segmentation d'image est le processus d'identification du contour des objets qui composent une image. Ces dernières années, l'utilisation de Réseaux Neuronaux Convolutionnels Profonds à des fins de segmentation d'image a fortement augmenté, avec des résultats supérieurs à ceux d'approches plus classiques. Nous explorerons l'implémentation et les applications potentielles des filtres de la théorie de la Morphologie Mathématique dans la structure d'un Réseau Neuronal Convolutionnel Profond. +
Ce travail applique les réseaux de neurones artificiels à convolution (CNN) à la reconnaissance du locuteur. Le CNN est utilisé pour approximer une mesure de la distance entre deux i-vectors (vecteurs représentant les composantes de la voix d'une personne). Contrairement à la distance cosinus, fréquemment utilisée comme mesure de distance entre deux vecteurs, la fonction approximée par un CNN peut être non-linéaire. La performance de ce modèle sera comparée à celles de la distance cosinus et du classificateur PLDA. +
Olena est l'une des bibliothèques de traitement d'images dont la généricité est la plus poussée. Celle-ci vient principalement d'une vision différente de la notion d'image via des concepts clés tels que les fenêtresaccumulateurs, dispatch par traits ainsi que les morphers. On va s'attacher à en faire une description détaillée ainsi que montrer comment les implémenter en Lisp. +
L'arbre des formes est une transformée d'image utile pour effectuer des traitements sur des images discrètes de façon auto-duale. Un algorithme (non publié)travaillant sur des images n-dimensionnelles dans l'espace des complexes cellulaires, nous permet déjà de construire un arbre des formes en temps quasi-linéaire. Cependant, cet algorithme reste souvent largement plus lent que d'autres approches en temps theta(nlog(n)) sur des images naturelles en 2D ou 3D, le nombre de cellules à traiter dans l'espace des complexes étant très élevé. En vue d'améliorer ces temps de calculs, nous présentons une approche pour paralléliser l'algorithme de calcul d'arbre quasi-linéaire en exhibant des propriétés topologiques et algorithmiques qui ne peuvent être facilement obtenues par les autres approches existantes. +
Approximation de la distance entre i-vecteurs par Perceptron Multi-Couches dans les systèmes de reconnaissance du locuteur +
Actuellement, l'espace des i-vecteurs est la représentation standard des paramètres de la parole dans les systèmes de reconnaissance du locuteur. Le calcul du score est généralement basé sur la distance cosinus, ou sur l'analyse discriminante linéaire probabiliste. Le but de ce sujet est de remplacer ces approches par un Perceptron Multi-Couches (PMC). Le PMC a montré en effet de bonnes performances pour approximer des fonctions non linéaires. L'idée principale étant de trouver une meilleure fonction que la distance cosinus. Les performances du perceptron multi-couches seront comparées aux autres méthodes comme la distance cosinus, l'analyse linéaire discriminante probabilisteou encore la machine de Boltzmann restreinte qui sera présenté par Jean Luc. +
Ce rapport se concentre sur l'explication d'un algorithme d'apprentissage actif sur la classe des automates visiblement á un compteur, et son implémentation en python et C++. L'algorithme en lui meme permet de créer ce type d'automates en disposant seulement d'un professeursans connaitre l'automate d'arrivée. Nous discutons ensuite des améliorations possibles de l'algorithme concernant sa vitesse d'execution et la représentation d'un automate. Nous donnons aussi une idée de comment est-ce qu'un tel programme semi-automatique peut etre évalué par un benchmark. +
Climb est une bibliothèque de traitement d'images générique ayant pour objectif le prototypage rapide. L'implémentation de deux algorithmes d'arbre de composantes impacte Climb de plusieurs façons : la définition des valeurs est étendue, de nouveaux ensembles de sites sont ajoutés et les outils de développement sont améliorés. Un détour est pris afin de comprendre le patron de conception de chaînage popularisé par la bibliothèque jQuery. La méthode est modifiée afin de s'adapter au traitement d'images ainsi qu'à Common Lisp. Elle est également étendue via une notation parallèle ainsi qu'avec une meilleure gestion du fil d'exécution. +