Abstract
From LRDE
T
Lors de cette présentation, un algorithme de resynchronisation sera décrit ainsi que son implémentation dans Vaucanson. De plus, des explications sont données sur l'ajout des transducteurs a délai borné, ainsi que sur les difficultés qui peuvent être rencontrées lors de l'extension de la hierarchie de classes de Vaucanson. +
FIXME +
Dans ce rapport technique, nous nous attardons sur le jeu de la tablette de chocolat. On dispose d'une tablette de chocolat dont le carré inférieur gauche est empoisonné. Les joueurs jouent à tour de rôle. Un coup consiste à choisir un carré de chocolat et à le manger ainsi que tous les carrés qui sont à sa droite et au dessus de lui. Le joueur qui mange le carré empoisonné perd la partie. Dans cet exposé, nous nous intéresserons particulièrement au cas où les dimensions du jeu sont de classe cardinale infinie. On présentera également, pour une meilleure compréhension, les nombres ordinaux et leur ordre associé. +
La transformation rapide des courbes de niveaux (FLLT) construit une représentation d'une image indépendante du contraste. Cet algorithme construit un arbre suivant les inclusions des formes. Pour un filtre, être invariant suivant le contraste est un plus. Par exemple, en analyse de document, cette représentation a le précieux avantage d'extraire facilement et rapidement les caractères indépendamment du fait qu'ils soient plus clairs ou plus foncés que leur voisinage. Ce document présente l'introduction de l'algorithme dans notre bibliothèque de traitement d'images et montre les résultats de quelques filtres connectés que peut engendrer cette représentation. +
Le but du projet Transformers est de créer un ensemble d'outils de manipulation de C et C++. Une fois achevé, il simplifiera la création d'outils de transformation ou d'analyse pour le C++. Il permettra aussi d'expérimenter des extensions du langage. Les étudiants du groupe Transformers ont travaillé pendant des annéespassant chaque année le résultat de leur travail à la génération suivante. De nombreux outils ont été créés, chacun d'eux résolvant (ou tentant de résoudre) un problème auquel nous sommes confrontés en essayant de manipuler du C++. Des dizaines de rapports ont été écrits : certains sont obsolètes, mais d'autres sont des ressources précieuses. Il est maintenant temps de prendre du recul, de regarder le travail accompli et ce qui ne fonctionne pas encore, afin de décider si et comment nous voulons poursuivre ce projet. +
The goal of the Transformers project is to create a C and C++ manipulation framework. Once achieved, it will simplify the creation of transformation or analysis tools for the C++ language. It will also allow experiments with language extensions. Transformers' students have been working for years on the project, handing over, each yearthe results of their work to the next generation. Lots of tools have been created, each of them solving (or attempting to) a problem that we face when trying to manipulate C++ code. Tens of reports have been written. Some are outdated, but some of them are still a valuable resource. It's now time to take a step back and to have a look at what has been accomplished and what does not work yet in order to decide if and how we want to go forward on this project. +
Spot is centered around the automata approach to model checking. The library can be used to verify that every behavior of a model, a transition-based generalized Büchi automata (TGBA), satisfies a given property, expressed using an linear temporal logic (LTL) formula. Spot offers two translation algorithms of LTL into TGBA, one of the two main stages of the approach. We present a new translation into TGBA of a LTL logic which has been extended by adding operators represented by finite automaton. This translation allows Spot to verify properties that were not expressible before. +
Spot is a model checking library centered around the automata approach, which 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 two translation algorithms from LTL formulæ into TGBA, one of the main stages of the approach. We present an extension of one of these algorithms to an extended LTL where operators are represented by finite automata, allowing Spot to verify properties that were not expressible before. We also present how we could integrate some features of PSL (Property Specification Language) in our extension. +
In a previous paper we introduced the two-automaton emptiness check in the Spot library, that would check for the emptiness of the intersection of the languages of two '"`UNIQ--math-00000003-QINU`"'-automata without building their productcircumventing a limitation in Spot on the number of acceptance sets of the automata. This operation, when the intersection is actually not empty, is usually followed by an accepting run search on the product that would return an example of such a word that is in the languages of both automata. We introduce a new method that computes an accepting run from the data gathered during the two-automaton emptiness check, allowing us to use this new method in algorithms that require the counterexample. +
Spot is library that handles '"`UNIQ--math-00000009-QINU`"'-automata whose acceptance conditions are expressed with at most 32 acceptance sets. Since the acceptance condition of the product of two automata has to use the sum of their setswe cannot produce a product whose operands use more than 32 sets in total. A typical operation on automata is to compute '"`UNIQ--math-0000000A-QINU`"' to know if '"`UNIQ--math-0000000B-QINU`"' intersects '"`UNIQ--math-0000000C-QINU`"'. When it is implemented as '"`UNIQ--math-0000000D-QINU`"', the computation of the product throttles the amout of acceptance sets A and B can use. We propose a new function '"`UNIQ--math-0000000E-QINU`"' which does the emptiness check of '"`UNIQ--math-0000000F-QINU`"' without actually building an automaton and hence without any limit on the acceptance conditions. The ltlcross tool can now compare automata using a total of more than 32 acceptance sets. +
U
Spot est une bibliothèque extensible pour le model checking qui utilise les automates de Büchi généralisés à transitions acceptantes. Il contient de nombreux algorithmes de pointes. Dans ce papier, on se concentre sur deux de ses algorithmes qui construisent des automates avec plus de transitions que nécessaire. En pratique ces constructions utiliseraient moins de transitions si elles pouvaient calculer un feedback arc set (FAS), c'est-à-dire un ensemble de transitions à retirer du graphe pour le rendre acyclique. Dans l'absoluon veut un FAS minimal, mais ce problème est NP-difficile. On adapte et améliore une heuristique proposée par Eades et al. qui permet une construction en temps linéaire. On montre comment cet algorithme bénéficie à la complémentation d'automates de Büchi déterministes et la traduction d'automates de Rabin en automates de Büchi. En fonction de l'automata traité on remarque une amélioration montant jusqu'à 31%. Ces résultats varient beaucoup selon le nombre de cycles et d'états acceptant. +
Ces dernières années, les opérateurs connectés ont gagné une certaine popularité dans le domaine du traitement d'images, ils ont en effet été largement utilisés dans le cadre de filtrage, de segmentation, de détection d'objets...Néanmoins, plusieurs défauts ont été mis en évidence, le plus important étant la dépendance au contraste, on ne peut que détecter soit les objets clairs, soit les objets foncés. Les opérateurs auto-duaux permettent d'opérer sur les objets clairs et foncés à la fois et ne souffrent donc pas du défaut des opérateurs connectés classiques. En revanche, les opérateurs auto-duaux sont plus difficiles à mettre en place et les algorithmes actuellement disponibles sont coûteux en temps de calcul. Nous proposons un nouvel algorithme pour calculer les opérateurs auto-duaux basés sur l'union-find de Tarjan; celui-ci offrant de meilleures performances que l'algorithme d'arbre de contours à l'état de l'art. +
Grâce au format HOA, il y a de moins en moins de barrières entre des ω-automates avec différentes conditions d'acceptation. Spot, une bibliothèque manipulant les ω-automates supporte des conditions d'acceptations arbitraires et propose déjà quelques conversions entre elles. Nous rajoutons de nouveaux algorithmes de conversions capables de convertir (quand c'est possible) n'importe quelle condition d'acceptation classique vers du co-Büchi déterministe. Boker and Kupferman ont mis au point des méthodes asymptotiquement optimales réalisant ces conversions. Nous avons implémenté leurs méthodes avec quelques optimisations et adaptations: nous supportons les conditions d'acceptations dites "Streett-like", celles écrites sous forme normale disjonctive (y compris celles dites "Rabin-like") ainsi que les acceptations basées sur les transitions ("transition-based"). Ces algorithmes peuvent être utilisés pour vérifier si une formule LTL est de la famille "persistence". +
Une implementation efficace de déterminisation d'automates de Büchi généralisés à transitions acceptantes +
Dans le model checking probabiliste, l'utilisation d' ω-automates déterministes permet de faciliter les calculs probabilistes grâce à l'unicité de chaque chemin. Malheureusement, il existe peu de traducteurs LTL qui produisent des ω-automates déterministes. De plus, ceux produits par Spot, une bibliothèques de model checking, ne le sont pas forcément. La powerset construction n'arrive pas toujours à déterminiser les automates de Büchi. Cependant, en mémorisant les chemins acceptants, la construction de Safra arrive à convertir les automates nondéterministes de Büchi en automates déterministes de Rabin. Le changement de condition d'acceptation est nécessaire car les automates de Büchi déterministes sont moins expressifs que leurs variantes nondéterministes. L'implémentation de cette construction permettra à Spot de déterminiser tous types d'automates et de calculer leurs compléments. Dans ce papier, on verra comment implémenter de manière efficace cette construction et comment l'étendre à la déterminisation d'automates de Büchi généralisés à transitions acceptantes. +
SCOOL est un langage dédié (DSL) destiné à faciliter le développement C++ de haut-niveau. Fondé sur le paradigme SCOOP mélangeant programmation générique et orientée-objet, il se démarque par une résolution statique des appels de fonctions membres et un système de concepts puissant. Précédemment, une bibliothèque de conteneurs standards a été réalisée en C++ grâce à SCOOP. Cette implémentation demandait cependant une forte maîtrise des mécanismes de SCOOP. Avec SCOOL, nous pouvons y arriver sans se préoccuper des détails, laissés au traducteur C++. En se concentrant sur le développement de la bibliothèque en SCOOL et sur les changements nécessaires au langage et à son compilateur, nous comparerons les solutions originales et à base de DSL et déterminerons si SCOOL est adapté au prototypage d'applications génériques. +
Cxx a réussi à supporter à la fois la programmation orienté objet classique et la programmation générique, cependant certains problèmes récurrents restent toujours difficiles à résoudre. Scoop est un paradigme orienté objet. Il fournit des méthodes virtuelles, les arguments covariants, les types virtuels et les multi-méthodes typées statiquement sans avoir besoin d'étendre le langage. Scoop utilise sa propre bibliothèque Cxx pour facilier la conception d'une bibliothèque utilisant ce paradigme. +
The text-localization system developed by the laboratory currently uses a wavelet-based descriptor to separate text from background in natural images. Benchmarks show that this descriptor is fast and accurate when performing this task. Our main objective is to extract shape information when performing classification using the same descriptor as the one used to separate text from background. Such data is useful improving the accuracy of other steps in the text localization system. Moreover, because the descriptor used to extract shape information has already been computedthis approach is not CPU consumin. More than shape information, the wavelet based descriptor can be extended again to create a simple O.C.R. (Optical Character Recognition). However in order to extract this data without changing the structure of the descriptor, some changes must be done in the classification process and in the learning process. Various methods to achieve these goals are presented and compared in order to see what kind of information could be extracted with the wavelet-based descriptor. +
Connected operators are morphological filters which have the property of keeping objects contours when simplifying images. They bring to the light objects situated in the image. To do it, an implementation of the Tarjan's Union-find algorithm is used for an easy manipulation of image components. A binary partition tree is built, in order to simplify the objects attributes computation and the filtering of image. First of all, we will introduce morphological filters and connected operators, then we will propose an overview of different kinds of methods used in the literature in order to create a binary partition tree and we will explain the Tarjan's "union-find" algorithm for the image filtering. At last, we will apply this method in order to clean and delete stars in space's images. +