Publications

A comparison of many max-tree computation algorithms

Edwin Carlinet · Thierry Géraud

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.

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

Thierry Géraud · Edwin Carlinet · Sébastien Crozet · Laurent Najman

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.

Discrete set-valued continuity and interpolation

Laurent Najman · Thierry Géraud

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.

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

Yongchao Xu · Thierry Géraud · Laurent Najman

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.

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

Renault · Alexandre Duret-Lutz · Fabrice Kordon · Denis Poitrenaud

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.

Practical application of probabilistic model checking to communication protocols

Marie Duflot · Marta Kwiatkowska · Gethin Norman · Dave Parker · Sylvain Peyronnet · Claudine Picaronny · Jeremy Sproston

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

Didier Verna

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.

TiCL: The prototype (Star TeX: The next generation, season 2)

Didier Verna

At TUG 2012, we presented some ideas about using one of the oldest programming languages (Lisp), in order to modernize one of the oldest typesetting systems (TeX). This talk was mostly focused on justifying the technical fitness of Lisp for this task. This time, we would like to take the opposite view and demonstrate a prototype, from the user’s perspective. This involves showing what a TiCL document could look like, the implications in terms of typesetting vs. programmatic features, and also in terms of extensibility (relate this to class / style authoring).

MITLL 2012 speaker recognition evaluation system description

Jonas Borgstrom · William Campbell · Najim Dehak · Réda Dehak · Daniel Garcia-Romero · Kara Greenfieldand Alan McCree · Doug Reynold · Fred Richardsony · Elliot Singery · Douglas Sturim · Pedro A. Torres-Carrasquillo

Morphological filtering in shape spaces: Applications using tree-based image representations

Yongchao Xu · Thierry Géraud · Laurent Najman

Connected operators are filtering tools that act by merging elementary regions of an image. A popular strategy is based on tree-based image representations: for example, one can compute a shape-based 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 build from the image. Such a processing is a generalization of the existing tree-based connected operators. Indeed, the framework includes classical existing connected operators by attributes. It also allows us to propose a class of novel connected operators from the leveling family, based on shape attributes. Finally, we also propose a novel class of self-dual connected operators that we call morphological shapings.