Combining explicit and symbolic approaches for better on-the-fly LTL model checking
In
Abstract
We present two new hybrid techniques that replace the synchronized product used in the automata-theoretic approach for LTL model checking. The proposed products are explicit graphs of aggregates (symbolic sets of states) that can be interpreted as Büchi automata. These hybrid approaches allow 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. The Symbolic Observation Product assumes a globally stuttering property (e.g., LTL-X) to aggregate states. The Self-Loop Aggregation Product does not require the property to be globally stuttering (i.e., it can tackle full LTL), but dynamically detects and exploits a form of stuttering where possible. Our experiments show that these two variants, while incomparable with each other, can outperform other existing approaches.
Generalized Büchi automata versus testing automata for model checking
In Proceedings of the second international workshop on scalable and usable model checking for petri net and other models of concurrency (SUMO’11)
Abstract
Geldenhuys and Hansen have shown that a kind of $\omega$-automaton known as testing automata can outperform the Buchi automata traditionally used in the automata-theoretic approach to model checking (geldenhuys.06.spin?). This work completes their experiments by including a comparison with generalized Buchi automata; by using larger state spaces derived from Petri nets; and by distinguishing violated formulæ (for which testing automata fare better) from verified formulæ (where testing automata are hindered by their two-pass emptiness check).
On-the-fly emptiness check of transition-based Streett automata
In Proceedings of the 7th international symposium on automated technology for verification and analysis (ATVA’09)
Abstract
In the automata theoretic approach to model checking, checking a state-space $S$ against a linear-time property $\varphi$ can be done in $\mathrm{O}(|S|\times 2^{\mathrm{O}(|\varphi|)})$ time. When model checking under $n$ strong fairness hypotheses expressed as a Generalized Büchi automaton, this complexity becomes $\mathrm{O}(|S|\times 2^{\mathrm{O}(|\varphi|+n)})$.Here we describe an algorithm to check the emptiness of Streett automata, which allows model checking under $n$ strong fairness hypotheses in $\mathrm{O}(|S|\times 2^{\mathrm{O}(|\varphi|)}\times 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.
An XML format proposal for the description of weighted automata, transducers, and regular expressions
In Post-proceedings of the seventh international workshop on finite-state methods and natural language processing (FSMNLP’08)
Abstract
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.
A static C++ object-oriented programming (SCOOP) paradigmc mixing benefits of traditional OOP and generic programming
In Proceedings of the workshop on multiple paradigm with object-oriented languages (MPOOL)
Abstract
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.
Multi-band segmentation using morphological clustering and fusion: Application to color image segmentation
In Proceedings of the IEEE international conference on image processing (ICIP)
Abstract
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 multi-band segmentation of images such as multi-spectral satellite images information.
Generic implementation of morphological image operators
In Mathematical morphology, proceedings of the 6th international symposium (ISMM)
Abstract
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.
Expression templates in Ada 95
In Proceedings of the 6th international conference on reliable software technologies (ada-europe)
Abstract
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.
Applying generic programming to image processing
In Proceedings of the IASTED international conference on applied informatics (AI)—symposium on advances in computer applications
Abstract
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.