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, <i>well-composed</i> 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.

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.

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.

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.

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.

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.

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.

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.

This paper introduces a topological approach to local invariant feature detection motivated by Morse theory. We use the critical points of the graph of the intensity image, revealing directly the topology information as initial “interest” points. Critical points are selected from what we call a tree-based shape-space. Specifically, they are selected from both the connected components of the upper level sets of the image (the Max-tree) and those of the lower level sets (the Min-tree). They correspond to specific nodes on those two trees: (1) to the leaves (extrema) and (2) to the nodes having bifurcation (saddle points). We then associate to each critical point the largest region that contains it and is topologically equivalent in its tree. We call such largest regions the Tree-Based Morse Regions (TBMR). TBMR can be seen as a variant of MSER, which are contrasted regions. Contrarily to MSER, TBMR relies only on topological information and thus fully inherit the invariance properties of the space of shapes (<i>e.g.</i>, invariance to affine contrast changes and covariance to continuous transformations). In particular, TBMR extracts the regions independently of the contrast, which makes it truly contrast invariant. Furthermore, it is quasi parameter-free. TBMR extraction is fast, having the same complexity as MSER. Experimentally, TBMR achieves a repeatability on par with state-of-the-art methods, but obtains a significantly higher number of features. Both the accuracy and the robustness of TBMR are demonstrated by applications to image registration and 3D reconstruction.

La notion de bien-composé a été introduite par Latecki en 1995 pour les ensembles et les images 2D et pour les ensembles 3D en 1997. Les images binaires bien-composées disposent d’importantes propriétés topologiques. De plus, de nombreux algorithmes peuvent tirer avantage de ces propriétés topologiques. Jusqu’à maintenant, la notion de bien-composé n’a pas été étudiée en dimension $n$, avec $n > 3$. Dans le travail présenté ici, nous démontrons le théorème fondamental de l’équivalence des connexités pour un ensemble bien-composé, puis nous généralisons la caractérisation des ensembles et des images bien-composés à la dimension $n$.