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. +
The objective is to improve Spot, a model checking library. Spot deals with a specific kind of graph in which each state is a set of variables with given values. These values can be seen as coordinates and a state can therefore be seen as a N-dimensional point. The state space is then a N-dimensional cloud and Spot does a depth first search on it. We want to generate states on the fly to improve the performances. For that, we use a kernel probability density estimation. The generated states are then used as starting points for threads which will explore the state space in parallel. +
L'objectif est d'améliorer Spot, une bibliothèque de Model Checking. Spot utilise un type de graphe spécifique dans lequel chaque état est un ensemble de variables avec des valeurs données. Ces valeurs peuvent être vues comme des coordonnées et un état peut donc être vu comme un point à N dimensions. L'espace d'états est alors un nuage à N dimensions et Spot effectue un parcours en profondeur sur celui-ci. Nous voulons générer des états à la volée pour améliorer les performances. Pour cela, nous utilisons une estimation de densité de probabilité par noyau. Les états générés sont ensuite utilisés comme points de départ pour des processus qui exploreront l'espace d'états en parallèle. +
A deterministic automaton can be minimized efficiently into an automaton that has a minimal number of states. The reduction algorithm presented here produces an automaton with a minimal number of states from a non deterministic automaton with weights defined in a field. This algorithm computes the base of the vector space generated by the series represented by the automaton and produces an automaton with a number of states equal to the dimension of this base. To find this base the algorithm has to solve a system of linear equations, this step requires the semiring to be a field. We also want to run our algorithm on fields that are not commutative which forbids the use of classical solvers for these systems. This report shows how we deal with these different constraints. We also present a modified algorithm to work with series over Z semiring which is not a field but has some sufficient properties. +
Vaucanson has been designed to satisfy the needs of the automaticians. There are, however, other fields where automata are widely used. This prospective report will focus on linguistics, and more precisely the automata needs of the natural language processing community since the applications differ from our usual ones. This way, we will be able to assess our range of applicability and usability. First, we will explore the different domains and detail the various needs. Then, we will be able to evaluate whether or not Vaucanson is usable for those domains and, finallydiscuss some potential work leads. +
Attribute grammars are well suited to describe (parts of) the semantics of programming languages: hooked on the syntactic production rules, they allow to express local relations that are later bound globally by a generic evaluator. However they fall short when working on large and complex languages. First attributes that are virtually needed everywhere need to be propagated by every single production rule. Second, this constraint hinders modularity, since adding a syntactic extension might require the propagation of new attributes in the rest of the language. This paper shows how to solve these problems by introducing a technique to automatically propagate attributes by completing the set of semantic rules. We formally define the propagation constraints such that it is optimized to avoid unnecessary addition of semantic rules. Attribute grammars are thus made more maintainable, modular and easier to use. +
Les grammaires attribuées sont plus adaptées pour décrire (des parties de) la sémantique d'un langage de programmation : accrochées sur les règles de production syntaxique, elles permettent d'exprimer des relations locales qui sont par la suite liées entre elles globalement par un évaluateur générique. Cependant elles ne passent pas à l'échelle quand on travaille avec des langages volumineux et complexes. Premièrement les attributs qui sont requis quasiment partout ont besoin d'être véhiculés par chaque règle de production. Deuxièmement, ces contraintes cassent la modularité car le fait d'étendre une grammaire nécessite la propagation des nouveaux attributs à travers le reste du langage. Ce papier montre comment résoudre ces problèmes en introduisant un système de propagation automatique des attributs qui complète l'ensemble des règles sémantiques. Nous avons défini formellement les contraintes de propagations de manière optimisée afin d'éviter l'ajout de règles sémantiques inutiles. Ainsi les grammaires attribuées sont devenus plus maintenables, modulaires et facile à utiliser. +
Atrial fibrillation is a common illness, which can be detected easily if you can localize the human atria in a MRI image. Manual segmentation is labor intensivetherefore here we adapt an automatic method developped for brain image segmentation. Using transfer learning, we retrain a convolutional neural network used for natural image categorization (VGG), and compare the advantages of using a pseudo-3D technique. We also explore ways to preprocess input data to improve final results. +
Our goal is to detect text zones on any type of identity documents from any country and that are recorded by smartphones cameras. Hence, we may segment latin letterscyrillic letters or ideograms. Moreover, some identity papers have watermarks or letters as background pattern that should be filtered. Furthermore, the context of the video (luminosity, background, ldots) has to be taken into account, in order to ensure that the binarized image has a minimal number of components to filter. In this way, the proposed processing, thanks to morphological operatorssegments the text and limits the number of components to process. +
Common Lisp og packages fg provide a functionality similar to og namespaces fg present in C++. They allow to encapsulate symbols that can be either exported or private. The exported ones must be explicitly declared at the package definition. This list is tedious to maintain when developing large projects. In this report will study ways to automatically maintain this list. Several approaches are proposed and compared. +
Our goal is to segment ancient maps of France, being cut and glued on a canvas. The colors in the canvas and in the maps are very close, making the boundary difficult to distinguish. However, pixel-perfect parts of the boundary are obtained thanks to morphological operators. To complete the segmentation, the image is separated, thanks to a maskinto three zones (map, canvas, and a "thick" boundary)which are used by a classification method to obtain results close to the actual boundary. Finally, the first results are corrected thanks to such new knowledge. +
Social media have been extensively used in the attempt to influence users with biased information and rumors. Recently, a new set of accounts know as troll farms have emerged, lauching coordinated disinformation campains. In this regard, we aim to identify the creation of troll farms by studying how they differ from common users and how they attempt to influence them. By leveraging graph analysis techniques we will look into how trolls propagate information through Twitter. Our goal being to build a system capable of recognizing troll farm accounts on trending topics on Twitter. +
VAUCANSON est une plateforme de manipulation d'automates finis et de transducteurs. Après plusieurs années de developpement, il fût constaté que l'interface mise en place pour manipuler les automates était trop complexe. Des travaux furent donc entrepris pour résoudre ce problème, amenant ainsi à l'introduction des "label kinds". Deux versions de la plateforme sont donc en developpement aujourd'hui: VAUCANSON 1.4, qui vise a terminer et compléter le travail effectué avant l'introduction des kinds et VAUCANSON 2.0, dernière version de la plateforme, pour le moment incomplète. Ce rapport a pour but de présenter une nouvelle fonctionnalité de VAUCANSON 1.4, les semi-anneaux Z/nZainsi que le travail en cours sur VAUCANSON 2.0. +
B
Entrainer un réseau de neurones convolutionnel dépends de l'utilisation d'une fonction de coût, qui offre une évaluation de la performance du réseau et permet l'optimisation de celui-ci. Différentes fonctions de coût évaluent la performance de manières différentes, et affectent donc différemment l'entraînement du réseau. Ce rapport a pour but de partager notre progrès dans l'évaluation de la performance de plusieurs fonctions de coût dans l'entrainement de réseaux de neurones convolutionnels pour la segmentation de tumeurs cérébrales. +
Vaucanson is an extensive C++ library for the manipulation of finite state machines. Compared to its main competitorOpenFST, Vaucanson has major performance issues. In order to improve the performance of Vaucanson, a set of tools is required to analyze the library's behavior in terms of CPU time requirements and memory usage. Up to March 2009, no existing tool was fully adapted to Vaucanson and practical to use. CBS is a C++ Benchmarking Suite that measures the performance of C++ projects and provides tools to displayanalyze and compare results in a human-readable form. It is used for in-depth Vaucanson profiling, and it helps the development team rewrite algorithms. +
This report summarizes three methods implemented in the model checking tool Spot. The first method aims at improving the conversion of a program model to a Kripke structure with partial order reduction, a technique where the order of some actions of the program is not considered relevant. This may reduce the size of the Kripke structure. The second method is a modification of the first, which makes it possible to use for LTL properties checking, with any LTL formula. The third method goal is to verify that no livelock may occur in a model, without the need of LTL property. We give benchmarks of all these methods, focusing on testing their common goal: reducing the amount of memory needed, which is an important bottleneck in the model checking field. +
Binary Partition Tree is an efficient structure to store region information for image processing, segmentation and information retrieval. It is a hierarchical structure to simplify operations and recognition on an image. It can use different region models and distance function calculation to create itself. Usually, we construct this tree on a segmented image for efficiency and time saving. All this parameters can variate and change the BPT representation of your image. The resistance of our tree to noise can also be studied, to find out what level of the tree is influenced by the noise. +
Pylene is an image processing (IP) library aiming for high genericity and performance. To accomplish its goals, it was created using C++ templates, allowing for great flexibility and no loss of performance. Pylene is one of the few IP libraries that successfully uses templates, which means it could become a staple in the IP field, but it would first have to overcome a big issue resulting from the usage of C++ templates. That issue is the usability of the library. C++ is not known for its ease of use, and by extension, this makes Pylene hard to use in concrete IP problems. Here, we try to overcome this problem through a Python version of the library. Seeing as though recreating all the library in Python would be nigh impossible, it seems sensible to instead try to bind the high level API to Python. This in itself brings up another issue: the available techniques do not answer our problems well enough, especially in regards to C++ template bindings. Since the idea behind templates of "knowing the type at compile time" doesn't exist in Python, we are faced with a gap between the static world of C++ templates, and the dynamic world of Python. We are presenting in this paper our solution to cross this static-dynamic difference: removing the templates through type-erasure and using contextual information for the type retrieval in Python. +
Spot is a C++ library that relies on the automata theoretic approach to model checking. To represent properties we use LTL-formulae, which are translated into automata. In Spot these automata are Transition-based Generalized Büchi Automata (TGBA). A major issue for a model checker is to be fast. A good way to reach that is to make automata as small as possible. Scientific litterature proposes a lot of algorithm to achieve our goal. Bisimulation and simulation work on '"`UNIQ--math-00000003-QINU`"'-automata. We see in this report how to adapt these algorithms to make them work on TGBA. We will see the profit which is given by the bisimulation implementation. And we deduce the importance to implement the simulation to reduce TGBA. +
L'architecture du projet Vaucanson a été con,cue initialement autour du design pattern Element. Ce dernier a l'énorme avantage de distinguer à la fois les concepts et les implémentations. C'est à dire que pour un type d'automate comme les automates booléens, on peut théoriquement avoir plusieurs implémentations qui se côtoient dans un même programme. Malgré toutes ces précautions, aujourd'hui, ajouter une nouvelle structure s'avère très délicat et remet en cause de nombreux points au sein du projet. C'est pour cette raison que durant ce séminaire nous tenterons de répondre à ces problèmes. Les problèmes de performances qu'a pu rencontrer le projet sont également une bonne motivation pour s'attaquer à ce sujet : il est aujourd'hui indispensable de proposer des nouvelles structures plus efficaces, notamment implémentées avec la bibliothèque Boost. +
Vaucanson est une bibliothèque générique de manipulation d'automates. Le cur de sa généricité réside dans le support de types d'automates variés mais aussi sa capacité à s'appuyer sur différentes structures de données. Actuellementnous avons différentes manières de manipuler des transitions. Cependant, aucune d'entre elles n'est réellement indépendante de la structure de données utilisée. Afin de pallier cela, nous allons nous tourner vers le design pattern Iterator. Nous évaluerons l'impact de ce design pattern sur les performances et sur l'utilisation de la bibliothèque en termes d'écriture d'algorithmes. +
The work performed last year underlined the fact that the overall performance issues of Vaucanson could be widely improved by an internal use of hash tables and, more particularly by the Multi Index from the Boost C++ library. We tried to make good use of the new functionalities provided by Boost. It results in the implementation of a new graph structure. We present in this report the different issues implied by these modifications on the graph implementation and we try to answer to the new issues about the genericity of Vaucanson. +
Suite aux séminaires de l'année dernière, il en ressort que les performances globales de Vaucanson pouvaient largement être améliorées par l'usage de tables de hachage et plus particulièrement les Multi Index de la bibliothèque Boost. Pour ce séminaire, nous chercherons à tirer parti des nouvelles fonctionnalités offertes par Boost. Ceci impliquera l'apparition d'une nouvelle implémentation de graphe. Nous présenterons au cours de ce séminaire les enjeux induits par ces changements sur l'implémentation et tenterons de répondre au problèmatiques soulevées par la généricité de Vaucanson. +
Vaucanson is a generic finite state machine manipulation platform. We have based our genericity on the ability to not only support various types of automata, but also to use different data structures to represent them. In its current state, we have various techniques to iterate over sets of transitions, however, none of them is really independent of the data structures. To overcome this problem, we have integrated the design pattern Iterator. Our goal is to assess the improvements given by this method in terms of performance and code writing. +
L'architecture du projet Vaucanson a été con,cue initialement autour du design pattern Element. Ce dernier a l'énorme avantage de distinguer à la fois les concepts et les implémentations. C'est à dire que pour un type d'automate comme les automates booléens, on peut théoriquement avoir plusieurs implémentations qui se côtoient dans un même programme. Malgré toutes ces précautions, aujourd'hui, ajouter une nouvelle structure s'avère très délicat et remet en cause de nombreux points au sein du projet. C'est pour cette raison que durant ce séminaire nous tenterons de répondre à ces problèmes. Les problèmes de performances qu'a pu rencontrer le projet sont également une bonne motivation pour s'attaquer à ce sujet : il est aujourd'hui indispensable de proposer des nouvelles structures plus efficaces, notamment implémentées avec la bibliothèque Boost. +
Deep neural networks are increasingly used for their capacity to correlate concrete parameters to deduce abstract characteristics. The bottleneck neural network is a specific form of those. This work presents the principle of this kind of network and its use for the reprocessing of Mel Frequency Cepstral Coefficients in a speaker recognition system. Therefore, it is a matter of studying the convergence of such network but also the change in overall system performance. +
The detection of white matter hyperintensities in an efficient way is an important issue in the medical field. Indeed, these hyperintensities are complicated to detect with the naked eye, even for medical personnel. An efficient detection of these hyperintensities would allow a better diagnosis of certain neuro-degenerative diseases but also to avoid certain medical errors. This is the issue we have tried to address in this report. We propose a solution based on a convolutional neural network accompanied by a preprocessing performed on these inputs +
Brain development can be evaluated using brain Magnetic Resonance Imaging (MRI). It is useful in cases of preterm birth to ensure that no brain disease develops during the postnatal period. Such diseases can be visible on T2-weighted MR image as high signal intensity (DEHSI). To assess the presence of white matter hyperintensities, this work implements a new robust, semi-automated frameworkbased on mathematical morphology, specialized on neonate brain segmentation. We will go over the related work, the implementation of the different steps and the difficulties encountered. In the end, the version developped during this internship is not completely finished but it is in good shape for a later finalization. +
Gliomas are a category of brain tumors that have different degrees of malignancy, shapes and textures. Manual segmentation by experts is a challenging task because of the heterogeneity of these tumors. Several methods of automated gliomas segmentation have been studied at MICCAI 2018 BraTS Challenge. We want to improve the segmentation results submitted last year by LRDE's team, using VGG architecture. This convolutional neural networkclassically used for natural image categorization, has been adapted for medical image segmentation through transfert learning and pseudo-3D techniques. Current improvements notably focus on preprocessing, using morphological operators, and will be submitted to this year's challenge. +
With the continuous improvement of quantum technologiesone might wonder if it is possible to take advantage of them for machine learning. In this paper we present a first approach of quantum computing as well as the implementation of a quantum perceptron we then explain the reasoning behind these algorithms. +
Climb is a generic image processing library. Still considered a prototype, Climb already provides tools that simplify the building of image processing chains such as morphers and the operator. In order to extend this aspect of Climb, a GUI has been developed. This GUI allows the construction of processing chains with no knowledge in programming, while providing a visual and interactive feedback to the user. This technical report describes the various components of this interface. Our approach uses the algorithms and tools defined in the library to construct the back-end logic and the interactive aspects of our graphical application. Since genericity is a key feature of Climb, we have been able to extend its scope beyond image processing, and thus show that we are able to use it in different situations such as the construction of a GUI. +
C
Transformers is a C++ manipulation framework built on Stratego/XT. Program Slicing is an important field of program transformation. We will explain what Program Slicing is, give a quick overview of various aspects of Program Slicing and show how Transformers can be turned into a C++ Program Slicing tool. +
C++ is a context-sensitive language that can be parsed using a context-free but ambiguous grammar. Disambiguation is then required to select the unique semantically-valid parse tree. Transformers, a framework for C++ program transformation, uses attribute grammars to achieve that stage. One of the hardest ambiguity in the language is related to metaprogramming. In so far as code is generated when templates are instanciated, types are not fully known at the declaration site. Therefore, type-checking is needed to perfectly handle templates, and it poses a real challenge. This report focuses on template disambiguationdetailing the problems and how to resolve it, in order to provide a better platform for source manipulation. +
Olena is one of the most advanced image processing libraries in terms of genericity. Its fully static design allows for high performance, although sometimes at the cost of overweighted syntax and longer compilation times. This makes it less convenient for incremental developmentexperimentation and rapid prototyping. We will present a different approach to generic image processing which, while using the same domain model as Olena, focuses on dynamicity aspects and offers a totally different use of the library. The cornerstone is the Common Lisp programming language which opens a perspective for interactive use, on-the-fly creation of image types and algorithms as well as a clearcustomizable and extensible syntax for common operations. +
Olena est l'une des bibliothèques de traitement d'images dont la généricité est la plus poussée. Son modèle entièrement statique permet de très bonnes performances, au prix d'une syntaxe alourdie et de temps de compilation importants. Ces aspects la rendent moins efficace pour le développement incrémentall'expérimentation et le prototypage rapide. Nous présenterons une approche différente du traitement d'images générique qui utilise la même modélisation du domaine qu'Olena mais se concentre sur les aspects dynamiques, offrant ainsi une utilisation totalement différente de la bibliothèque. La pierre angulaire est le langage Common Lisp qui permet une utilisation interactive, la création à la volée de nouveaux types d'images ou de nouveaux algorithmes, tout en offrant une syntaxe claire, personnalisable et extensible pour les opérations courantes. +
Ce travail utilise une architecture siamoise pour calculer une similarité. On donne en entrée deux échantillons sur deux sous-réseaux de neurones identiques avec les mêmes poids. Chaque sous-réseau prend en entrée des statistiques sur les données du signal. On peut ensuite calculer la distance entre les informations. Le DNN est capable de projeter les entrées dans un sous-espace de dimension plus basse en apprenant un invariant. On présente les résultats de cette application en s'appuyant sur plusieurs types de statistiques et on les compare aux mesures classiques utilisant PLDA ou la distance cosinus, appliquées à des i-vecteurs. +
Le complexe de Morse-Smale est un outil utile pour analyser la topologie d'une image. Cependant, son calcul est onéreux et il existe plusieurs algorithmes qui poss`dent des différences dans la définition du complexe. D'un autre côté, l'algorithme de coupe de ligne de partage des eaux est un algorithme morphologique qui découpe des images en niveaux de gris. Il interprète les images comme des graphes valués sur les arrêtes, les poids étant donnés par le gradient de l'image. Lidija Comic était la première á mettre en avant une possible équivalence entre l'algorithme de calcul du Morse-Smale et l'algorithme de ligne de partage des eaux, avec des marqueurs spécifiques sur les maxima et les minima de l'image. Dans ce document, nous parlons de cette possibilité et nous proposons une implémentation d'une version modifiée de l'algorithme de coupe de ligne de partage des eaux, qui fonctionne sur un graphe valué sur les sommets pour calculer le complexe de Morse-Smale. +
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. Dans ce rapport technique, 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. +
Olena is a generic image processing library developed at LRDE. It provides many morphological algorithms. Mathematical morphology offers several powerful tools in image processing and analysis. Similarities appear when writing morphological algorithms. Thereby, we can classify those tools and then build canvases of algorithms. This report presents what is a canvas and why canvases matter. We will see different manners to implement canvases with their pro and con arguments. Finally, we will explain which canvas implementation we have chosen for Olena and why. +
Olena est une bibliothèque générique de traitement d'images développée au LRDE. Elle propose un grand nombre d'algorithmes morphologiques. La morphologie mathématique, offre des outils très puissants de traitement et d'analyse d'images. Des similarités apparaissant dans l'écriture des algorithmes morphologiques, il est possible de les classifier etainsi, de proposer un certain nombre de "canevas" d'algorithmes. Ce rapport définie ce que sont les canevas et les avantages qu'ils apportent. Apres une brève introduction à la morphologie mathématique, cet exposé presentera différents canevas d'algorithmes retenus par Olena. +
FIXME +
FIXME +