In the automata theoretic approach to model checking, checking a state-space S against a linear-time property φ can be done in (|S|×2(|φ|)) time. When model checking under n strong fairness hypotheses expressed as a Generalized Büchi automaton, this complexity becomes (|S|× 2(|φ|+n)).Here we describe an algorithm to check the emptiness of Streett automata, which allows model checking under n strong fairness hypotheses in (|S|× 2(|φ|)×n). We focus on transition-based Streett automata, because it allows us to express strong fairness hypotheses by injecting Streett acceptance conditions into the state-space without any blowup.
We present an XML format that allows to describe a large class of finite weighted automata and transducers. Our design choices stem from our policy of making the implementation as simple as possible. This format has been tested for the communication between the modules of our automata manipulation platform Vaucanson, but this document is less an experiment report than a position paper intended to open the discussion among the community of automata software writers.
Nous présentons deux algorithmes d'emptiness check pour les automates de Büchi dont les états sont des ensembles qui peuvent s'inclure les uns les autres. Le premier est équivalent à un emptiness check traditionnel, mais utilise des tests d'inclusion pour diriger la construction à la volée de l'automate. Le second est beaucoup plus rapide, mais peut retourner de faux négatifs. Nous illustrons et évaluons l'amélioration avec une réduction basée sur les symétries.
We introduce two emptiness checks for Büchi automata whose states represent sets that may include each other. The first is equivalent to a traditional emptiness check but uses inclusion tests to direct the on-the-fly construction of the automaton. The second is impressively faster but may return false negatives. We illustrate and benchmark the improvement on a symmetry-based reduction.
A possible attack on the state explosion of the automata-theoretic approach to model-checking is to build an automaton B whose states represent sets of states of the original automaton A to check for emptiness. This paper introduces two emptiness checks for Büchi automata whose states represent sets that may include each other. The first check on B is equivalent to a traditional emptiness check on A but uses inclusion tests to direct and further reduce the on-the-fly construction of B. The second check is impressively faster but may return false negatives. We illustrate and benchmark both using a symmetry-based reduction.
Emptiness check is a key operation in the automata-theoretic approach to LTL verification. However, it is usually done on Büchi automata with a single u acceptance condition. We review existing on-the-fly emptiness-check algorithms for generalized Büchi automata (i.e., with multiple acceptance conditions) and u show how they compete favorably with emptiness-checks for degeneralized automata, especially in presence of weak fairness assumptions. We also introduce a new emptiness-check algorithm, some heuristics to improve existing checks, and propose algorithms to compute accepting runs in the case of multiple acceptance conditions.
Spot is a C++ library offering model checking bricks that can be combined and interfaced with third party tools to build a model checker. It relies on Transition-based Generalized Büchi Automata (TGBA) and does not need to degeneralize these automata to check their emptiness. We motivate the choice of TGBA by illustrating a very simple (yet efficient) translation of LTL into TGBA. We then show how it supports on-the-fly computations, and how it can be extended or integrated in other tools.
Object-oriented and generic programming are both supported in C++. OOP provides high expressiveness whereas GP leads to more efficient programs by avoiding dynamic typing. This paper presents SCOOP, a new paradigm which enables both classical OO design and high performance in C++ by mixing OOP and GP. We show how classical and advanced OO features such as virtual methods, multiple inheritance, argument covariance, virtual types and multimethods can be implemented in a fully statically typed model, hence without run-time overhead.
In this paper we propose a novel approach for color image segmentation. Our approach is based on segmentation of subsets of bands using mathematical morphology followed by the fusion of the resulting segmentation "channels". For color images the band subsets are chosen as RG, RB and GB pairs, whose 2D histograms are processed as projections of a 3D histogram. The segmentations in 2D color spaces are obtained using the watershed algorithm. These 2D segmentations are then combined to obtain a final result using a region split-and-merge process. The CIE L*a*b* color space is used to measure the color distance. Our approach results in improved performance and can be generalized for multiband segmentation of images such as multi-spectral satellite images.
Several libraries dedicated to mathematical morphology exist. But they lack genericity, that is to say, the ability for operators to accept input of different natures-2D binary images, graphs enclosing floating values, etc. We describe solutions which are integrated in Olena, a library providing morphological operators. We demonstrate with some examples that translating mathematical formulas and algorithms into source code is made easy and safe with Olena. Moreover, experimental results show that no extra costs at run-time are induced.
High-order matrix or vector expressions tend to be penalized by the use of huge temporary variables. Expression templates is a C++ technique which can be used to avoid these temporaries, in a way that is transparent to the user. We present an Ada adaptation of this technique which-while not transparent-addresses the same efficiency issue as the original. We make intensive use of the signature idiom to combine packages together, and discuss its importance in generic programming. Finally, we express some concerns about generic programming in Ada.
This paper presents the evolution of algorithms implementation in image processing libraries and discusses the limits of these implementations in terms of reusability. In particular, we show that in C++, an algorithm can have a general implementation; said differently, an implementation can be generic, i.e., independent of both the input aggregate type and the type of the data contained in the input aggregate. A total reusability of algorithms can therefore be obtained; moreover, a generic implementation is more natural and does not introduce a meaningful additional cost in execution time as compared to an implementation dedicated to a particular input type.
Generic programming is a paradigm whose wide adoption by the C++ community is quite recent. In this scheme most classes and procedures are parameterized, leading to the construction of general and efficient software components. In this paper, we show how some design patterns from Gamma et al. can be adapted to this paradigm. Although these patterns rely highly on dynamic binding, we show that, by intensive use of parametric polymorphism, the method calls in these patterns can be resolved at compile-time. In intensive computations, the generic patterns bring a significant speed-up compared to their classical peers.
Algorithm libraries dedicated to image processing and pattern recognition are not reusable; to run an algorithm on particular data, one usually has either to rewrite the algorithm or to manually "copy, paste, and modify". This is due to the lack of genericity of the programming paradigm used to implement the libraries. In this paper, we present a recent paradigm that allows algorithms to be written once and for all and to accept input of various types. Moreover, this total reusability can be obtained with a very comprehensive writing and without significant cost at execution, compared to a dedicated algorithm. This new paradigm is called "generic programming" and is fully supported by the C++ language. We show how this paradigm can be applied to image processing and pattern recognition routines. The perspective of our work is the creation of a generic library.
Great efforts have gone into building scientific libraries dedicated to particular application domains and a main issue is to manage the large number of data types involved in a given domain. An ideal algorithm mplementation should be general: it should be written once and process data in an abstract way. Moreover, it should be efficient. For several years, some libraries have been using generic programming to address this problem. In this report, we present two major improvements of this paradigm.In generic libraries, a concept is the description of a set of requirements on a type that parameterizes an algorithm implementation (the notion of concept replaces the classical object-oriented notion of abstract class). A problem is that, until now, concepts are only defined in the documentation. We managed to make them explicit in the program by representing a concept by a type; moreover, (multiple) concept inheritance is fully supported. The procedure signature thus evolves from void foo(AbstractA&) for classic object-orientation, and from template<class A> void foo(A&) for classic generic programming, towards template<class A> void foo(ConceptA<A>&). This results in a better support of procedure overloading, which is of prime importance for libraries where each algorithm implementation can have numerous variations.
Another problem is that the generic programming paradigm suffers from a lack of appropriate design patterns. We observed that classical patterns of Gamma et al. can be translated into this paradigm while handling operation polymorphism by parametric polymorphism. In these patterns, method calls can be solved statically, because the inferior type of each object in generic programming is known at compile-time. We thus preserve their modularity and reusability properties but we avoid the performance penalty due to their dynamic behavior, which is a critical issue in numerical computing. This results in better design capabilities for object-oriented generic libraries.
Dans le cadre de l'écriture en C++ d'une bibliothèque de traitements d'images et d'un atelier de programmation par composants d'une chaîne de traitements, nous nous sommes fixés deux objectifs principaux : rendre les traitements génériques vis-à-vis du type de ses entrées sans entraîner de surcoût significatif à l'exécution, et pouvoir exécuter un traitement lorsqu'il a eté introduit ultérieurement à la compilation de l'atelier.Le premier objectif est atteint a l'aide de programmation générique et de la traduction en polymorphisme statique de certains idiomes (design patterns) définis pour le polymorphisme dynamique. La problématique du second objectif est double. Tout d'abord, nous devions réaliser la mise en correspondance d'un traitement dont les entrées-sorties sont des types abstraits et de la routine générique, chargée du traitement, dont les paramètres sont des types concrets ; ensuite, nous devions pouvoir compiler et lier de nouveaux traitements a la volée, lors de l'exécution de l'atelier. Pour atteindre ce double objectif, nous utilisons de la programmation générative et nous pratiquons l'instanciation paresseuse (lazy) de code générique.
Les solutions que nous apportons permettent la gestion de composants réutilisables de calcul scientifique, ce qui, à notre connaissance, est original.