Publications

Implementation concepts in Vaucanson 2

Abstract

Vaucanson is an open source C++ platform dedicated to the computation with finite weighted automata. It is generic: it allows to write algorithms that apply on a wide set of mathematical objects. Initiated ten years ago, several shortcomings were discovered along the years, especially problems related to code complexity and obfuscation as well as performance issues. This paper presents the concepts underlying Vaucanson 2, a complete rewrite of the platform that addresses these issues.

Continue reading

Compositional approach to suspension and other improvements to LTL translation

Abstract

Recently, there was defined a fragment of LTL (containing fairness properties among other interesting formulae) whose validity over a given infinite word depends only on an arbitrary suffix of the word. Building upon an existing translation from LTL to Büchi automata, we introduce a compositional approach where subformulae of this fragment are translated separately from the rest of an input formula and the produced automata are composed in a way that the subformulae are checked only in relevant accepting strongly connected components of the final automaton. Further, we suggest improvements over some procedures commonly applied to generalized Büchi automata, namely over generalized acceptance simplification and over degeneralization. Finally we show how existing simulation-based reductions can be implemented in a signature-based framework in a way that improves the determinism of the automaton.

Continue reading

Efficient multiscale Sauvola’s binarization

Abstract

This work is focused on the most commonly used binarization method: Sauvola’s. It performs relatively well on classical documents. However, three main defects remain: the window parameter of Sauvola’s formula do not fit automatically to the content; it is not robust to low contrasts; it is non-invariant with respect to contrast inversion. Thus, on documents such as magazines, the content may not be retrieved correctly which is crucial for indexing purpose. In this paper, we describe how to implement an efficient multiscale implementation of Sauvola’s algorithm in order to guarantee good binarization for both small and large objects inside a single document without adjusting the window size to the content. We also describe on how to implement it in an efficient way, step by step. Pixel-based accuracy and OCR evaluations are performed on more than 120 documents. This implementation remains notably fast compared to the original algorithm. For fixed parameters, text recognition rates and binarization quality are equal or better than other methods on small and medium text and is significantly improved on large text. Thanks to the way it is implemented, it is also more robust on textured text and on image binarization. This implementation extends the robustness of Sauvola’s algorithm by making the results almost insensible to the window size whatever the object sizes. Its properties make it usable in full document analysis toolchains.

Continue reading

A comparison of many max-tree computation algorithms

Abstract

With the development of connected filters in the last decade, many algorithms have been proposed to compute the max-tree. Max-tree allows computation of the most advanced connected operators in a simple way. However, no exhaustive comparison of these algorithms has been proposed so far and the choice of an algorithm over another depends on many parameters. Since the need for fast algorithms is obvious for production code, we present an in depth comparison of five algorithms and some variations of them in a unique framework. Finally, a decision tree will be proposed to help the user choose the most appropriate algorithm according to their requirements.

Continue reading

A quasi-linear algorithm to compute the tree of shapes of $n$-D images

Abstract

To compute the morphological self-dual representation of images, namely the tree of shapes, the state-of-the-art algorithms do not have a satisfactory time complexity. Furthermore the proposed algorithms are only effective for 2D images and they are far from being simple to implement. That is really penalizing since a self-dual represen- tation of images is a structure that gives rise to many powerful operators and applications, and that could be very useful for 3D images. In this paper we propose a simple-to-write algorithm to compute the tree of shapes; it works for nD images and has a quasi-linear complexity when data quantization is low, typically 12 bits or less. To get that result, this paper introduces a novel representation of images that has some amazing properties of continuity, while remaining discrete.

Continue reading

Discrete set-valued continuity and interpolation

Abstract

The main question of this paper is to retrieve some continuity properties on (discrete) T0-Alexandroff spaces. One possible application, which will guide us, is the construction of the so-called “tree of shapes” (intuitively, the tree of level lines). This tree, which should allow to process maxima and minima in the same way, faces quite a number of theoretical difficulties that we propose to solve using set-valued analysis in a purely discrete setting. We also propose a way to interpret any function defined on a grid as a “continuous” function thanks to an interpolation scheme. The continuity properties are essential to obtain a quasi-linear algorithm for computing the tree of shapes in any dimension, which is exposed in a companion paper.

Continue reading

Two applications of shape-based morphology: Blood vessels segmentation and a generalization of constrained connectivity

Abstract

Connected filtering is a popular strategy that relies on tree-based image representations: for example, one can compute an attribute on each node of the tree and keep only the nodes for which the attribute is sufficiently strong. This operation can be seen as a thresholding of the tree, seen as a graph whose nodes are weighted by the attribute. Rather than being satisfied with a mere thresholding, we propose to expand on this idea, and to apply connected filters on this latest graph. Consequently, the filtering is done not in the space of the image, but on the space of shapes built from the image. Such a processing, that we called shape-based morphology, is a generalization of the existing tree-based connected operators. In this paper, two different applications are studied: in the first one, we apply our framework to blood vessels segmentation in retinal images. In the second one, we propose an extension of constrained connectivity. In both cases, quantitative evaluations demonstrate that shape-based filtering, a mere filtering step that we compare to more evolved processings, achieves state-of-the-art results.

Continue reading

Strength-based decomposition of the property Büchi automaton for faster model checking

Abstract

The automata-theoretic approach for model checking of linear-time temporal properties involves the emptiness check of a large Büchi automaton. Specialized emptiness-check algorithms have been proposed for the cases where the property is represented by a weak or terminal automaton. When the property automaton does not fall into these categories, a general emptiness check is required. This paper focuses on this class of properties. We refine previous approaches by classifying strongly-connected components rather than automata, and suggest a decomposition of the property automaton into three smaller automata capturing the terminal, weak, and the remaining strong behaviors of the property. The three corresponding emptiness checks can be performed independently, using the most appropriate algorithm. Such a decomposition approach can be used with any automata-based model checker. We illustrate the interest of this new approach using explicit and symbolic LTL model checkers.

Continue reading

Practical application of probabilistic model checking to communication protocols

Abstract

Continue reading

The incredible tale of the author who didn’t want to do the publisher’s job

Abstract

In this article, I relate on a recent experience of mine: writing a book chapter for a publisher who doesn’t have a clue about typesetting. I confess my futile attempt at using TeX for writing the chapter in question. I describe the hell that descended upon me for daring to do that. I however admit that the hell in question would have been even greater, hadn’t I done so. This article is both a nervous breakdown and a laughter, and I am seeking for the reader’s comfort.

Continue reading