Annonce

annonce@lrde.epita.fr

564 discussions

by Roland Levillain

The Olena Team is proud to announce the release of Olena 2.0. Olena is a platform dedicated to image processing and pattern recognition. Its core component is a generic and efficient C++ library called Milena. Milena provides a framework to implement simple, fast, safe, reusable and extensible image processing tool chains. The library provides many ready-to-use image data structures (regular 1D, 2D, 3D images, graph-based images, etc.) and algorithms. Milena's algorithms are built upon classical entities from the image processing field (images, points/sites, domains, neighborhoods, etc.). This design allows image processing developers and practitioners to easily understand, modify, develop and extend new algorithms while retaining the core traits of Milena: genericity and efficiency. On top of Milena, the Olena platform also features optional modules such as Swilena, a component exposing Milena to other languages thanks to the Simplified Wrapper and Interface Generator (SWIG); and the SCRIBO module for Document Image Analysis (see below). The Olena platform is Free Software. It is distributed under the conditions of the GNU General Public License (GPL) version 2. See the file COPYING shipped with the Olena distribution. Release notes are available at: http://olena.lrde.epita.fr/Olena200 You can download packages of the Olena 2.0 distribution here: http://www.lrde.epita.fr/dload/olena/2.0/olena-2.0.tar.gz (38 MB) http://www.lrde.epita.fr/dload/olena/2.0/olena-2.0.tar.bz2 (32 MB) The SHA1 digests of theses packages are: d3a829fa56bff4edbca58af0c9a39c9569820c60 olena-2.0.tar.gz 0abae2a9bc751a8fb33acacd2dbe70635d5dd00b olena-2.0.tar.bz2 Here is a list of major changes since Olena 1.0: * The biggest addition to Olena available in this new version is the SCRIBO module for Document Image Analysis (DIA). This module has been developed in the context of the SCRIBO project (see http://www.scribo.ws). The SCRIBO module provides software building blocks to create DIA tool chains, including routines for preprocessing steps (such as binarization, show-through removal, deskew and denoising), text lines identification, non-text objects retrieval (tables, pictures, separators, etc.), line reconstruction (rebuilding separators and tables), Optical Character Recognition (OCR) integration and document reconstruction (converting a document to XML, PDF and/or HTML outputs). Dedicated data structures are also provided to handle intermediate results. Some Graphical User Interface (GUI) programs based on the Qt toolkit are also proposed. * Several compilation issues have been addressed. * New algorithms (especially in mathematical morphology), canvases (or algorithmic patterns) and efficient algorithm variants have been added to Milena, as well as some new data types (see NEWS for more details). * More conversion routines, especially regarding color values. * Support for I/O routines (both built-in and depending on third-party packages) has been improved. * Various bug fixes and improvements. The file NEWS, included in the archive, contains a more complete list of user-visible changes. Please report any problem by mail to <olena-bugs(a)lrde.epita.fr>. -- Roland Levillain - LRDE/EPITA - A3SI/ESIEE/LIGM/UMLV-Paris Est EPITA Research and Development Laboratory (LRDE) 14-16, rue Voltaire - FR-94276 Le Kremlin-Bicêtre Cedex - France Phone: +33 1 53 14 59 45 - Fax: +33 1 53 14 59 22 - www.lrde.epita.fr

13 years, 6 months

Publication: VECoS'11: LTL Translation Improvements in Spot

by Alexandre Duret-Lutz

We are happy to announce that the following paper has been accepted for publication at the 5th International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS'11) that will take place in Tunis, Tunisia, on September 15-16, 2011. LTL Translation Improvements in Spot A. Duret-Lutz Laboratoire de Recherche et Développement de l'Epita (LRDE) http://publis.lrde.epita.fr/201109-VECOS Spot is a library of model-checking algorithms. This paper focuses on the module translating LTL formulæ into automata. We discuss improvements that have been implemented in the last four years, we show how Spot's translation competes on various benchmarks, and we give some insight into its implementation. -- Alexandre Duret-Lutz

13 years, 8 months

Extensible Languages (book chapter)

by Didier Verna

Hello, I'm happy to announce that I will be writing a chapter for an upcoming book on Domain Specific Languages. The chapter description is given below: Extensible languages -- blurring the distinction between DSLs and GPLs Domain-specific language (DSL) design and implementation is inherently a transversal activity. It usually requires from the application developers knowledge and expertise in both the application domain and in language design and implementation, two completely orthogonal areas of expertise. The difficulty is that either one needs to find people with such dual competence, which is rare, or one needs to add manpower to the project by means of different teams which in turn need to coordinate their efforts and communicate together, something not easy to do either. >From the programming language perspective, one additional complication is that being an expert developer in one specific programming language does not make you an expert in language design and implementation -- only in using one of them. DSLs, however, are most of the time completely different from the language in which the embedding application is written. A general-purpose programming language (GPL), suitable to write a large application, is generally not suited to domain-specific modeling, precisely because it is too general. Using a GPL for domain-specific modeling would require too much expertise from the end-users and wouldn't be expressive enough for the very specific domain the application is supposed to focus on. As a consequence, it is often taken for granted that your application's DSL has to be completely different from your application's GPL. But what if this assumption was wrong in the first place ? The need for designing a DSL as a completely new language often comes from the lack of extensibility of your GPL of choice. By imposing a rigid syntax, a set of predefined operators and data structures on you, the traditional GPL approach gives you no choice but to implement your application's DSL as a different language, with its own lexical and syntactic parser, semantic analyzer and possibly its own brand new interpreter or even compiler. A much less widely accepted view, however, is that some GPLs are extensible, or customizable enough to let you implement a DSL merely as either a subset or an extension of your original language. The result is that your final application, as a whole, is now written in a completely unified language. While the end-user does not have access to the whole backstage infrastructure and hence does not really see a difference with the traditional approach, the gain for the developer is substantial. Since the DSL is now just another entry point for the same original GPL, there is essentially only one application written in only one language to maintain. Moreover, no specific language infrastructure (parser, interpreter, compiler etc.) is required for the DSL anymore, since it is simply expressed in terms of the original GPL. The already existing GPL infrastructure is all that is needed. -- Resistance is futile. You will be jazzimilated. Scientific site: http://www.lrde.epita.fr/~didier Music (Jazz) site: http://www.didierverna.com EPITA/LRDE, 14-16 rue Voltaire, 94276 Le Kremlin-Bicêtre, France Tel. +33 (0)1 44 08 01 85 Fax. +33 (0)1 53 14 59 22

13 years, 8 months

L'air de rien 21

by Daniela Becker

Bonjour, nous avons le plaisir de vous présenter le n°21 du bulletin du LRDE. C'est un numéro spécial consacré au séminaire des élèves CSI organisé le 4 juillet 2011 avec les résumés de toutes les présentations. Les étudiants des promos 2012 et 2013 y présenteront leur travail. Vous trouverez également les dernières publications et sorties de logiciels du LRDE dans ce numéro. Et une autre date à retenir : le 6 juillet aura lieu le séminaire LRDE. Vous pouvez télécharger le bulletin en couleur à la page suivante : http://publis.lrde.epita.fr/201107-l-air-de-rien-21 -- Daniela Becker Responsable administrative du LRDE

13 years, 9 months

[Séminaire des étudiants CSI] lundi 4 juillet 2011 - Amphi Masters

by Daniela Becker

Bonjour, nous avons le plaisir de vous inviter au séminaire des étudiants du LRDE. Il aura lieu le lundi 4 juillet 2011 à 9h30 - 17h15 en Amphi Masters (KB). ----------------------------------------------------------------------- Au programme: *CLIMB, SCRIBO, TIGER, SPOT, SPEAKER ID et VAUCANSON* http://publis.lrde.epita.fr/Seminar-2011-07-04 CLIMB * 09h30 : Arbres de composantes et opérateurs de chaînage -- Christopher Chedeau * 10h00 : Ecriture d'algorithmes de traitement d'images génériques -- Simon Guillot * 10h30 : Implémentation de voisinages pondérés -- Laurent Senta SCRIBO * 11h15 : Analyse de la mise en page d'un document dans SCRIBO -- Julien Marquegnies * 11h45 : Extraction du texte en inverse video dans SCRIBO -- Coddy Levi * 12h15 : Désambiguïsation de la superposition de lignes -- Sylvain Lobry TIGER * 14h00 : Optimisations dans le compilateur Tiger -- Félix Abecassis SPOT * 14h30 : Amélioration de la dégénéralisation dans Spot -- Pierre Parutto * 15h00 : Réductions basées sur la bisimulation appliquées aux TGBA -- Thomas Badie SPEAKER ID * 15h45 : Speaker ID - Détection de voix -- Victor Lenoir VAUCANSON * 16h15 : Avancées vers Vaucanson 1.4 et 2.0 -- Guillaume Fiette * 16h45 : Implémentation du semi-anneau rationnel -- David Moreira ----------------------------------------------------------------------- Les Résumés des exposés : ************************** CLIMB 09h30 : Arbres de composantes et opérateurs de chaînage -- Christopher Chedeau 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. 10h00 : Ecriture d'algorithmes de traitement d'images génériques -- Simon Guillot Climb est une bibliothèque générique de traitement d'images en Lisp. L'étude de l'implémentation d'un algorithme de segmentation par ligne de partage des eaux permet de faire état des possibilités offertes par un langage dynamique tel que Lisp allié à une modélisation générique des images. Cette étude de cas permet d'aborder les concepts de base de la manipulation d'images au sein de Climb tels que les sites, les ensembles de sites et les accumulateurs. L'utilisation de l'ensemble de ces notions reposent sur l'aspect dynamique et fonctionnel de Lisp. 10h30 : Implémentation de voisinages pondérés -- Laurent Senta Climb est une bibliothèque de traitement d’images générique développée en Lisp. Les voisinages sont representés sous la forme d’ensemble de sites (site-set) pour permettre des manipulations génériques sur de multiples types d’images. En parallèle de ces concepts, une étude des voisinages pondérés est effectuée, expliquant différents moyens d’étendre le concept d’une écriture unique des algorithmes pour les exécuter sur différents types de paramètres. Trois implémentations sont proposées, décrites et comparées au niveau de leur généricité et de leur expressivité. SCRIBO 11h15 : Analyse de la mise en page d'un document dans SCRIBO -- Julien Marquegnies L’extraction des différentes structures d’un document numérisé se base sur la mise en place d’une chaîne de traitement 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 paragraphes, constitue 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. 11h45 : Extraction du texte en inverse video dans SCRIBO -- Coddy Levi L'extraction du texte d'images de document intervient dans le processus plus général de compréhension de documents que propose le projet SCRIBO. Le texte peut être présent dans deux formes : foncé sur fond clair ou clair sur fond foncé, appelé Inverse Video. Cette présentation explique les problématiques liées à l’extraction du texte en inverse video dans SCRIBO en utilisant la chaîne de traitement déjà existante, les problèmes ainsi introduits et les pistes explorées pour l’amélioration des résultats. 12h15 : Désambiguïsation de la superposition de lignes -- Sylvain Lobry Lorsque l'on essaye d'extraire du texte en inverse vidéo (couleur claire sur fond fonce), nous verrons lors de la présentation de Coddy Levi que de nombreux problèmes surgissent. Le plus courant d'entre eux est la superpositions entre ce texte en inverse vidéo, et celui en couleur foncée sur clair. Nous montrerons donc lors de cette présentation comment faire un choix entre ces lignes en superposition, en considérant différents critères et en les pondérant. TIGER 14h00 : Optimisations dans le compilateur Tiger -- Félix Abecassis Le compilateur Tiger est un projet éducatif jouant un rôle central dans le cursus de la troisième année de l’EPITA. Ce projet est l’occasion d’enseigner aux étudiants des bonnes pratiques de développement logiciel comme les design patterns ainsi que l’importance des tests et de la documentation. L’ère de l’informatique séquentielle étant terminée, la programmation parallèle, autrefois reléguée aux universités et aux laboratoires de recherche est maintenant devenue incontournable dans tout cursus d’informatique, pour cette raison nous aimerions introduire du parallèlisme dans le projet. Dans ce rapport nous étudions les possibilités de parallélisation dans le compilateur Tiger en utilisant la bibliothèque Intel Threading Building Blocks (TBB). Nous avons également diagnostiqué et corrigé plusieurs soucis de performance dans l’algorithme d’allocation de registres. SPOT 14h30 : Amélioration de la dégénéralisation dans Spot -- Pierre Parutto 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 capacité de transformer un TGBA en TBA (appelé dégénéralisation) 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. 15h00 : Réductions basées sur la bisimulation appliquées aux TGBA -- Thomas Badie Spot est une bibliothèque C++ de model checking utilisant l’approche par automates. Pour représenter les propriétés à vérifier, nous utilisons des formules LTL qui sont traduites en automates. Dans Spot, ces automates sont des Automates de Büchi généralisés basés sur les transitions (TGBA). Un enjeu pour tout model checker, est d’être rapide. Une manière de faire est de rendre les automates aussi petit que possible. La littérature scientifique propose de nombreux algorithmes pour arriver à notre but. La bisimulation et la simulation réduisent des automates qui reconnaissent des mots infinis. Ce rapport montre comment adapter ces algorithmes pour des TGBA ainsi que le gain apporté par l’implémentation de la bisimulation, ce qui souligne l’importance d’implémenter la simulation pour réduire les TGBA. SPEAKER ID 15h45 : Speaker ID - Détection de voix -- Victor Lenoir La détection de voix a de nombreuses applications. C'est par exemple une étape obligatoire avant de faire de la reconnaissance du locuteur. Ce rapport présente deux différents types d'algorithmes pour la détection de voix (VAD) : un utilisant des seuils et le second utilisant des mélanges de gaussiennes (GMM). Les algoritmes proposés utilisent des caractéristiques calculées sur des petits intervalles de temps comme par exemple l'énergie, la monotonie spectrale ou les Mel-Frequency Cepstral Coefficients (MFCC). Les différents algorithmes de détection de voix sont comparés dans différentes conditions de bruit afin de mettre en évidence leur robustesse aux bruits. VAUCANSON 16h15 : Avancées vers Vaucanson 1.4 et 2.0 -- Guillaume Fiette 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 à 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/nZ, ainsi que le travail en cours sur Vaucanson 2.0. 16h45 : Implémentation du semi-anneau rationnel -- David Moreira Vaucanson est une plateforme de manipulation d’automates finis et de transducteurs dont l’interface s’est montrée trop complexe. Pendant les deux dernières années, des travaux ont étés entrepris afin d’introduire le concept de kind d’un automate dans la bibliothèque. Aujourd’hui, une partie de la nouvelle interface a été implémentée et le travail sur le cœur a laissé Vaucanson 1.4 dans un état instable. Ce rapport montrera dans un premier temps le travail effectué pour Vaucanson 1.4, puis sur les travaux entrepris afin de rendre stable Vaucanson 2.0. -- Daniela Becker

13 years, 9 months

CDR 9 "File-Local Variables" finalized

by Didier Verna

Hello, I'm pleased to announce that my proposal for Common Lisp "File-Local Variables" has been accepted, finalized and published at the Common Document Repository. It can now be referred to as CDR #9. The abstract is given below: The Common Lisp standard defines two special variables, *PACKAGE* and *READTABLE*, that are treated in a special way: the functions LOAD and COMPILE-FILE establish a new dynamic binding for each of them, so that any modification to their value at load or compile time becomes local to the file being processed. It is this particular treatment of these variables that allows for IN-PACKAGE or IN-READTABLE (from the NAMED-READTABLES library) to essentially have a ``file-local'' effect. The motivation for the present document is the claim that this behavior could be useful for other, user-defined variables, although there is currently no way to do so in standard Common Lisp. -- Resistance is futile. You will be jazzimilated. Scientific site: http://www.lrde.epita.fr/~didier Music (Jazz) site: http://www.didierverna.com EPITA/LRDE, 14-16 rue Voltaire, 94276 Le Kremlin-Bicêtre, France Tel. +33 (0)1 44 08 01 85 Fax. +33 (0)1 53 14 59 22

13 years, 9 months

Publication: ATVA'11: Self-Loop Aggregation Product — A New Hybrid Approach to On-the-Fly LTL Model Checking

by Alexandre Duret-Lutz

We are happy to announce that the following paper has been accepted for publication at the 9th international symposium on Automated Technology for Verification and Analysis (ATVA'11) that will take place in Taipei, Taiwan, on October 11-14, 2011. Self-Loop Aggregation Product — A New Hybrid Approach to On-the-Fly LTL Model Checking A. Duret-Lutz (1) K. Klai (2) D. Poitrenaud (3) Y. Thierry-Mieg. (3) (1) Laboratoire de Recherche et Développement de l'Epita (LRDE) (2) Laboratoire d'Informatique de Paris-Nord (LIPN) (3) Laboratoire d'Informatique de Paris 6 (LIP6) http://publis.lrde.epita.fr/201110-ATVA We present the Self-Loop Aggregation Product (SLAP), a new hybrid technique that replaces the synchronized product used in the automata-theoretic approach for LTL model checking. The proposed product is an explicit graph of aggregates (symbolic sets of states) that can be interpreted as a Büchi automata. The criterion used by SLAP to aggregate states from the Kripke structure is based on the analysis of self-loops that occur in the Büchi automaton expressing the property to verify. Our hybrid approach allows on the one hand to use classical emptiness-check algorithms and build the graph on-the-fly, and on the other hand, to have a compact encoding of the state space thanks to the symbolic representation of the aggregates. Our experiments show that this technique often outperforms other existing (hybrid or fully symbolic) approaches. -- Alexandre Duret-Lutz

13 years, 9 months

[Seminaire-LRDE] Séminaire Performance et Généricité du LRDE le Mercredi 6 juillet 2011

by Jonathan Fabrizio

Chers collègues, La prochaine session du séminaire Performance et Généricité du LRDE (Laboratoire de Recherche et Développement de l'EPITA) aura lieu le Mercredi 6 juillet 2011 (14h-15h). Au programme: * 14h: Un algorithme rapide pour le Compressive Sensing sur architectures parallèles -- Alexandre Borghi http://www.lri.fr Dans ce séminaire je présenterai un algorithme de résolution approchée pour le problème du Compressive Sensing basé sur la programmation convexe. Cet algorithme a la particularité d'avoir été pensé dès sa conception pour tirer partie des architectures matérielles modernes, ce qui permet une implémentation efficace et rapide sur ces celles-ci. Bien qu'une résolution approchée soit en pratique suffisante pour obtenir rapidement une solution de très bonne qualité, une variante exacte très rapide sera aussi présentée. Cette dernière n'est toutefois utilisable que sous certaines conditions. Trois types d'architectures parallèles sont ici envisagées : des processeurs multi-coeurs avec unités de calcul vectoriel, des processeurs graphiques (GPU) et le processeur Cell. -- Alexandre Borghi est diplômé de la promotion CSI 2007 de l'EPITA et effectue actuellement sa thèse au LRI de l'Université Paris-SUD XI. Il s'intéresse principalement à l'adaptation de l'algorithmique aux architectures parallèles. Pour plus de renseignements, consultez http://seminaire.lrde.epita.fr/. L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette information le plus largement possible. _______________________________________________ Seminaire mailing list Seminaire(a)lrde.epita.fr https://www.lrde.epita.fr/mailman/listinfo/seminaire

13 years, 9 months

[Seminaire-LRDE] Séminaire Performance et Généricité du LRDE le Mercredi 15 juin 2011

by Jonathan Fabrizio

Chers collègues, La prochaine session du séminaire Performance et Généricité du LRDE (Laboratoire de Recherche et Développement de l'EPITA) aura lieu le Mercredi 15 juin 2011 (14h-17h). Au programme: * 14h: Modèle basé-contexte pour l'annotation automatique du multimédia -- Nicolas Ballas http://www.kalisteo.fr/en/index.htm http://caor.mines-paristech.fr/ Ces dernières années ont vu exploser le nombre de vidéos disponibles sur internet. Pour permettre leur exploitation, il est nécessaire de mettre en place des systèmes analysant automatiquement ces données multimédia. De tels systèmes permettent notamment d'indexer automatiquement des vidéos en fonction de leurs contenus. Durant cette présentation, je m'intéresserai aux récentes avancées effectuées dans ce domaine. Je présenterai des descripteurs vidéos, développés dans le cadre de ma thèse, qui capturent le mouvement et l'apparence d'une vidéo pour les résumer dans une courte signature. Ces signatures peuvent être utilisées a posteriori pour détecter différents évènements ou concepts dans les vidéos. -- Nicolas Ballas effectue sa thèse entre le laboratoire LVIC du CEA/List et le laboratoire CAOR de l'école des Mines de Paris. Il s'intéresse principalement au problème de perception automatique à travers l'étude d'algorithmes combinant vision par ordinateur et apprentissage automatique. * 15h30: Traitement d'images sur processeur graphique avec CUDA et C++ -- Matthieu Garrigues http://uei.ensta-paristech.fr Conçus à l'origine pour le rendu 2D et 3D, les processeurs graphiques (GPU) peuvent aujourd'hui être considérés comme des processeurs génériques massivement parallèles. Mais ce parallélisme impose des contraintes sur les algorithmes implantés et les types de données utilisés. D'autre part, le bus de communication entre le processeur central (CPU) et le GPU peut être un goulot d'étranglement. Ce séminaire débutera par un aperçu des avantages et inconvénients de la programmation GPU, puis je présenterai l'implantation d'un algorithme temps réel de suivi de points dans une vidéo. Je terminerai par l’introduction de deux petites boîtes à outils : Cuimg et Dige. Cuimg utilise C++ pour simplifier l'écriture d'algorithmes de traitement d'images avec CUDA, tandis que Dige, basée sur le framework Qt, permet le prototypage rapide d'interfaces graphiques. -- Matthieu Garrigues est diplômé de la promotion CSI 2009 de l'EPITA. Depuis, il s'intéresse au développement et l'implantation d'applications de vision par ordinateur sur des architectures parallèles. Il est actuellement ingénieur de recherche à l'unité d'électronique et d'informatique de l'ENSTA. Pour plus de renseignements, consultez http://seminaire.lrde.epita.fr/. L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette information le plus largement possible. _______________________________________________ Seminaire mailing list Seminaire(a)lrde.epita.fr https://www.lrde.epita.fr/mailman/listinfo/seminaire

13 years, 9 months

Publication: SUMo'11: Generalized Büchi Automata versus Testing Automata for Model Checking

by Alexandre Duret-Lutz

We are happy to announce that the following paper has been accepted for publication at the 2nd International Workshop on Scalable and Usable Model Checking for Petri Nets and other models of Concurrency (SUMo'11) that will take place in Newcastle, UK, on June 21, 2011. Generalized Büchi Automata versus Testing Automata for Model Checking A.-E. Ben Salem (1&2) A. Duret-Lutz (1) F. Kordon (2) (1) Laboratoire de Recherche et Développement de l'Epita (LRDE) (2) Laboratoire d'Informatique de Paris 6 (LIP6) http://publis.lrde.epita.fr/201106-SUMO Geldenhuys and Hansen have shown that a kind of omega-automaton known as testing automata can outperform the Büchi automata traditionally used in the automata-theoretic approach to model checking. This work completes their experiments by including a comparison with generalized Büchi automata; by using larger state spaces derived from Petri nets; and by distinguishing violated formulae (for which testing automata fare better) from verified formulae (where testing automata are hindered by their two-pass emptiness check). -- Alexandre Duret-Lutz

13 years, 10 months

← Newer
1
...
34
35
36
37
38
39
40
...
57
Older →

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

Annonce