This paper investigates the speckle spot detection task in ultrasound images. Speckle spots are described by structural criteria: dimensions, shape, and topology. We propose to represent the image using a morphological inclusion tree, from which speckle spots are detected using their structural appearance. This makes the method independent of contrast, and hence robusts to intensity correction. The detection was applied to speckle reduction and speckle tracking, and experiments showed that this approach performs well compared to state-of-the-art methods.

We present a type system for automata and rational expressions, expressive enough to encompass weighted automata and transducers in a single coherent formalism. The system allows to express useful properties about the applicability of operations including binary heterogeneous functions over automata. We apply the type system to the design of the platform, a library dedicated to the computation with finite weighted automata, in which genericity and high efficiency are obtained at the lowest level through the use of template metaprogramming, by letting the template system play the role of a static type system for automata. Between such a low-level layer and the interactive high-level interface, the type system plays the crucial role of a mediator and allows for a cleanly-structured use of dynamic compilation.

Le cadre classique des filtres connexes consiste à enlever d’un graphe certaines de ses composantes connexes. Pour appliquer ces filtres, il est souvent utile de transformer une image en un arbre de composantes, et on élague cet arbre pour simplifier l’image de départ. Les arbres ainsi formés ont des propriétés remarquables pour la vision par ordinateur. Une première illustration de leur intérêt est la définition d’un détecteur de zones d’intérêt, vraiment invariant aux changements de contraste, qui nous permet d’obtenir des résultats à l’état de l’art en recalage d’images et en reconstruction 3D à base d’images. Poursuivant dans l’utilisation de ces arbres, nous proposons d’élargir le cadre des filtres connexes. Pour cela, nous introduisons la notion d’espaces des formes basés sur des arbres : au lieu de filtrer des composantes connexes du graphe correspondant à l’image, nous proposons de filtrer des composantes connexes du graphe donné par l’arbre des composantes de l’image. Ce cadre général, que nous appelons morphologie basée sur les formes, peut être utilisé pour la détection et la segmentation d’objets, l’obtention de segmentations hiérarchiques, et le filtrage d’images. De nombreuses applications et illustrations montrent l’intérêt de ce cadre.

Deterministic Büchi automata (DBA) are useful to (probabilistic) model checking and synthesis. We survey techniques used to obtain and minimize DBAs for different classes of properties. We extend these techniques to support DBA that have generalized and transition-based acceptance (DTGBA) as they can be even smaller. Our minimization technique—a reduction to a SAT problem—synthesizes a DTGBA equivalent to the input DTGBA for any given number of states and number of acceptance sets (assuming such automaton exists). We present benchmarks using a framework that implements all these techniques.

In this paper, we explored the use of Gaussian Mixture Model (GMM) weights adaptation for speaker verifica- tion. We compared two different subspace weight adap- tation approaches: Subspace Multinomial Model (SMM) and Non-Negative factor Analysis (NFA). Both techniques achieved similar results and seemed to outperform the retraining maximum likelihood (ML) weight adaptation. However, the training process for the NFA approach is substantially faster than the SMM technique. The i-vector fusion between each weight adaptation approach and the classical i-vector yielded slight improvements on the tele- phone part of the NIST 2010 Speaker Recognition Eval- uation dataset.

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.

In a previous work, we showed that a kind of $\omega$-automata known as <i>Transition-based Generalized Testing Automata</i> (TGTA) can outperform the Büchi automata traditionally used for <i>explicit</i> model checking when verifying stutter-invariant properties. In this work, we investigate the use of these generalized testing automata to improve <i>symbolic</i> model checking of stutter-invariant LTL properties. We propose an efficient symbolic encoding of stuttering transitions in the product between a model and a TGTA. Saturation techniques available for decision diagrams then benefit from the presence of stuttering self-loops on all states of TGTA. Experimentation of this approach confirms that it outperforms the symbolic approach based on (transition-based) Generalized Büchi Automata.

Mathematical morphology, when used in the field of document image analysis and processing, is often limited to some classical yet basic tools. The domain however features a lesser-known class of powerful operators, called connected filters. These operators present an important property: they do not shift nor create contours. Most connected filters are linked to a tree-based representation of an image’s contents, where nodes represent connected components while edges express an inclusion relation. By computing attributes for each node of the tree from the corresponding connected component, then selecting nodes according to an attribute-based criterion, one can either filter or recognize objects in an image. This strategy is very intuitive, efficient, easy to implement, and actually well-suited to processing images of magazines. Examples of applications include image simplification, smart binarization, and object identification.

Spot is a library of model-checking algorithms started in 2003. This paper focuses on its module for translating linear-time temporal logic (LTL) formulas into Büchi automata: one of the steps required in the automata-theoretic approach to LTL model-checking. We detail the different algorithms involved in this translation: the core translation itself, which performs many simplifications thanks to its use of binary decision diagrams; the pre-processing of the LTL formulas with rewriting rules chosen to help their translation; and various post-processing algorithms whose use depends on the intent of the translation: do we favor deterministic automata, or small automata? Using different benchmarks, we show how Spot competes with other LTL translators, and how it has improved over the years.