Property

Abstract

From LRDE

Showing 20 pages using this property.
.
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.  +