Publications

A color tree of shapes with illustrations on filtering, simplification, and segmentation

By Edwin Carlinet, Thierry Géraud

2015-04-07

In Mathematical morphology and its application to signal and image processing – proceedings of the 12th international symposium on mathematical morphology (ISMM)

Abstract

The Tree of Shapes is a morphological tree that provides a high-level, hierarchical, self-dual, and contrast invariant representation of images, suitable for many image processing tasks. When dealing with color images, one cannot use the Tree of Shapes because its definition is ill-formed on multivariate data. Common workarounds such as marginal processing, or imposing a total order on data are not satisfactory and yield many problems (color artifacts, loss of invariances, etc.) In this paper, we highlight the need for a self-dual and contrast invariant representation of color images and we provide a method that builds a single Tree of Shapes by merging the shapes computed marginally, while guarantying the most important properties of the ToS. This method does not try to impose an arbitrary total ordering on values but uses only the inclusion relationship between shapes. Eventually, we show the relevance of our method and our structure through some illustrations on filtering, image simplification, and interactive segmentation.

Continue reading

Efficient computation of attributes and saliency maps on tree-based image representations

By Yongchao Xu, Edwin Carlinet, Thierry Géraud, Laurent Najman

2015-04-07

In Mathematical morphology and its application to signal and image processing – proceedings of the 12th international symposium on mathematical morphology (ISMM)

Abstract

Tree-based image representations are popular tools for many applications in mathematical morphology and image processing. Classically, one computes an attribute on each node of a tree and decides whether to preserve or remove some nodes upon the attribute function. This attribute function plays a key role for the good performance of tree-based applications. In this paper, we propose several algorithms to compute efficiently some attribute information. The first one is incremental computation of information on region, contour, and context. Then we show how to compute efficiently extremal information along the contour (e.g., minimal gradient’s magnitude along the contour). Lastly, we depict computation of extinction-based saliency map using tree-based image representations. The computation complexity and the memory cost of these algorithms are analyzed. To the best of our knowledge, except information on region, none of the other algorithms is presented explicitly in any state-of-the-art paper.

Continue reading

How to make $n$D functions digitally well-composed in a self-dual way

By Nicolas Boutry, Thierry Géraud, Laurent Najman

2015-04-07

In Mathematical morphology and its application to signal and image processing – proceedings of the 12th international symposium on mathematical morphology (ISMM)

Abstract

Latecki et al. introduced the notion of 2D and 3D well-composed images, i.e., a class of images free from the “connectivities paradox” of digital topology. Unfortunately natural and synthetic images are not a priori well-composed. In this paper we extend the notion of “digital well-composedness” to $n$D sets, integer-valued functions (gray-level images), and interval-valued maps. We also prove that the digital well-composedness implies the equivalence of connectivities of the level set components in $n$D. Contrasting with a previous result stating that it is not possible to obtain a discrete $n$D self-dual digitally well-composed function with a local interpolation, we then propose and prove a self-dual discrete (non-local) interpolation method whose result is always a digitally well-composed function. This method is based on a sub-part of a quasi-linear algorithm that computes the morphological tree of shapes.

Continue reading

Self-duality and digital topology: Links between the morphological tree of shapes and well-composed gray-level images

By Thierry Géraud, Edwin Carlinet, Sébastien Crozet

2015-04-07

In Mathematical morphology and its application to signal and image processing – proceedings of the 12th international symposium on mathematical morphology (ISMM)

Abstract

In digital topology, the use of a pair of connectivities is required to avoid topological paradoxes. In mathematical morphology, self-dual operators and methods also rely on such a pair of connectivities. There are several major issues: self-duality is impure, the image graph structure depends on the image values, it impacts the way small objects and texture are processed, and so on. A sub-class of images defined on the cubical grid, well-composed images, has been proposed, where all connectivities are equivalent, thus avoiding many topological problems. In this paper we unveil the link existing between the notion of well-composed images and the morphological tree of shapes. We prove that a well-composed image has a well-defined tree of shapes. We also prove that the only self-dual well-composed interpolation of a 2D image is obtained by the median operator. What follows from our results is that we can have a purely self-dual representation of images, and consequently, purely self-dual operators.

Continue reading

A self-adaptive likelihood function for tracking with particle filter

By Séverine Dubuisson, Myriam Robert-Seidowsky, Jonathan Fabrizio

2015-03-01

In Proceedings of the 10th international conference on computer vision theory and applications (VISAPP)

Abstract

The particle filter is known to be efficient for visual tracking. However, its parameters are empirically fixed, depending on the target application, the video sequences and the context. In this paper, we introduce a new algorithm which automatically adjusts “on-line" two majors of them: the correction and the propagation parameters. Our purpose is to determine, for each frame of a video, the optimal value of the correction parameter and to adjust the propagation one to improve the tracking performance. On one hand, our experimental results show that the common settings of particle filter are sub-optimal. On another hand, we prove that our approach achieves a lower tracking error without needing tuning these parameters. Our adaptive method allows to track objects in complex conditions (illumination changes, cluttered background, etc.) without adding any computational cost compared to the common usage with fixed parameters.

Continue reading

Single-pass testing automata for LTL model checking

By Ala Eddine Ben Salem

2015-03-01

In Proceedings of the 9th international conference on language and automata theory and applications (LATA’15)

Abstract

Testing Automaton (TA) is a new kind of $\omega$-automaton introduced by Hansen et al. as an alternative to the standard Büchi Automata (BA) for the verification of stutter-invariant LTL properties. Geldenhuys and Hansen shown later how to use TA in the automata-theoretic approach to LTL model checking. They propose a TA-based approach using a verification algorithm that requires two searches (two passes) and compare its performance against the BA approach. This paper improves their work by proposing a transformation of TA into a normal form (STA) that only requires a single one-pass verification algorithm. The resulting automaton is called Single-pass Testing Automaton (STA). We have implemented the STA approach in Spot model checking library. We are thus able to compare it with the “traditional” BA and TA approaches. These experiments show that STA compete well on our examples.

Continue reading

TextTrail: A robust text tracking algorithm in wild environments

By Myriam Robert-Seidowsky, Jonathan Fabrizio, Séverine Dubuisson

2015-03-01

In Proceedings of the 10th international conference on computer vision theory and applications (VISAPP)

Abstract

In this paper, we propose TextTrail, a robust new algorithm dedicated to text tracking in uncontrolled environments (strong motion of camera and objects, partial occlusions, blur, etc.). It is based on a particle filter framework whose correction step has been improved. First, we compare some likelihood functions and introduce a new one that integrates tangent distance. We show that the likelihood function has a strong influence on the text tracking performances. Secondly, we compare our tracker with another and finally present an example of application. TextTrail has been tested on real video sequences and has proven its efficiency. In particular, it can track texts in complex situations starting from only one detection step without needing another one to reinitialize the tracking model.

Continue reading

Parallel explicit model checking for generalized Büchi automata

By Étienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud

2015-01-13

In Proceedings of the 19th international conference on tools and algorithms for the construction and analysis of systems (TACAS’15)

Abstract

We present new parallel emptiness checks for LTL model checking. Unlike existing parallel emptiness checks, these are based on an SCC enumeration, support generalized Buchi acceptance, and require no synchronization points nor repair procedures. A salient feature of our algorithms is the use of a global union-find data structure in which multiple threads share structural information about the automaton being checked. Our prototype implementation has encouraging performances: the new emptiness checks have better speedup than existing algorithms in half of our experiments.

Continue reading

Context-oriented image processing

By Didier Verna, François Ripault

2015-01-01

In Context-oriented programming workshop

Abstract

Genericity aims at providing a very high level of abstraction in order, for instance, to separate the general shape of an algorithm from specific implementation details. Reaching a high level of genericity through regular object-oriented techniques has two major drawbacks, however: code cluttering (e.g. class / method proliferation) and performance degradation (e.g. dynamic dispatch). In this paper, we explore a potential use for the Context-Oriented programming paradigm in order to maintain a high level of genericity in an experimental image processing library, without sacrificing either the performance or the original object-oriented design of the application.

Continue reading

Contribution aux tests de vacuité pour le model checking explicite

Abstract

The automata-theoretic approach to linear time model-checking is a standard technique for formal verification of concurrent systems. The system and the property to check are modeled with omega-automata that recognizes infinite words. Operations overs these automata (synchronized product and emptiness checks) allows to determine whether the system satisfies the property or not. In this thesis we focus on a particular type of omega-automata that enable a concise representation of weak fairness properties: transitions-based generalized Büchi automata (TGBA). First we outline existing verification algorithms, and we propose new efficient algorithms for strong automata. In a second step, the analysis of the strongly connected components of the property automaton led us to develop a decomposition of this automata. This decomposition focuses on multi-strength property automata and allows a natural parallelization for already existing model-checkers. Finally, we proposed, for the first time, new parallel emptiness checks for generalized Büchi automata. Moreover, all these emptiness checks are lock-free, unlike those of the state-of-the-art. All these techniques have been implemented and then evaluated on a large benchmark.

Continue reading