Latecki et al. have introduced the notion of well-composed images, i.e., a class of images free from the connectivities paradox of discrete topology. Unfortunately natural and synthetic images are not a priori well-composed, usually leading to topological issues. Making any $n$D image well-composed is interesting because, afterwards, the classical connectivities of components are equivalent, the component boundaries satisfy the Jordan separation theorem, and so on. In this paper, we propose an algorithm able to make $n$D images well-composed without any interpolation. We illustrate on text detection the benefits of having strong topological properties.

L’arbre des formes est un arbre morphologique à la fois auto-dual et invariant par changement de contraste. Il fournit une représentation haut-niveau de l’image, intéressante pour de nombreuses tâches de traitement d’images. Malgré son potentiel et sa simplicité, il reste largement sous-utilisé en reconnaissance des formes et vision par ordinateur. Dans cet article, nous présentons une méthode de segmentation interactive qui s’effectue simplement en manipulant cet arbre. Pour cela, nous nous appuierons sur une représentation récemment définie : l’Arbre des Formes Couleur . La méthode de segmentation interactive que nous proposons ne requiert aucun apprentissage statistique ; néanmoins elle obtient des résultats qui rivalisent avec ceux de l’état de l’art. Bien que préliminaires, les résultats obtenus mettent en avant le potentiel et l’intérêt des méthodes travaillant dans l’espace des formes.

In explicit model checking, systems are typically described in an implicit and compact way. Some valid information about the system can be easily derived directly from this description, for example that some atomic propositions cannot be valid at the same time. The paper shows several ways to apply this information to improve the Büchi automaton built from an LTL specification. As a result, we get smaller automata with shorter edge labels that are easier to understand and, more importantly, for which the explicit model checking process performs better.

In the context of text detection evaluation, it is essential to use protocols that are capable of describing both the quality and the quantity aspects of detection results. In this paper we propose a novel visual representation and evaluation tool that captures the whole nature of a detector by using histograms. First, two histograms (coverage and accuracy) are generated to visualize the different characteristics of a detector. Secondly, we compare these two histograms to a so called optimal one to compute representative and comparable scores. To do so, we introduce the usage of the Earth Mover’s Distance as a reliable evaluation tool to estimate recall and precision scores. Results obtained on the ICDAR 2013 dataset show that this method intuitively characterizes the accuracy of a text detector and gives at a glance various useful characteristics of the analyzed algorithm.

We propose several automata-based constructions that check whether a specification is stutter-invariant. These constructions assume that a specification and its negation can be translated into Büchi automata, but aside from that, they are independent of the specification formalism. These transformations were inspired by a construction due to Holzmann and Kupferman, but that we broke down into two operations that can have different realizations, and that can be combined in different ways. As it turns out, implementing only one of these operations is needed to obtain a functional stutter-invariant check. Finally we have implemented these techniques in a tool so that users can easily check whether an LTL or PSL formula is stutter-invariant.

We propose a flexible exchange format for $\omega$-automata, as typically used in formal verification, and implement support for it in a range of established tools. Our aim is to simplify the interaction of tools, helping the research community to build upon other people’s work. A key feature of the format is the use of very generic acceptance conditions, specified by Boolean combinations of acceptance primitives, rather than being limited to common cases such as Büchi, Streett, or Rabin. Such flexibility in the choice of acceptance conditions can be exploited in applications, for example in probabilistic model checking, and furthermore encourages the development of acceptance-agnostic tools for automata manipulations. The format allows acceptance conditions that are either state-based or transition-based, and also supports alternating automata.

An alternative to the traditional Büchi Automata (BA), called Testing Automata (TA) was proposed by Hansen et al. to improve the automata theoretic approach to LTL model checking. In previous work, we proposed an improvement of this alternative approach called TGTA (Generalized Testing Automata). TGTA mixes features from both TA and TGBA (Generalized Büchi Automata), without the disadvantage of TA, which is the second pass of the emptiness check algorithm. We have shown that TGTA outperform TA, BA and TGBA for explicit and symbolic LTL model checking. However, TA and TGTA are less expressive than Büchi Automata since they are able to represent only stutter-invariant LTL properties (LTL). In this paper, we show how to extend Generalized Testing Automata (TGTA) to represent any LTL property. This allows to extend the model checking approach based on this new form of testing automata to check other kinds of properties and also other kinds of models (such as Timed models). Implementation and experimentation of this extended TGTA approach show that it is statistically more efficient than the Büchi Automata approaches (BA and TGBA), for the explicit model checking of LTL properties.

In automata-theoretic model checking, there are mainly two approaches: <i>explicit</i> and <i>symbolic</i>. In the explicit approach, the state-space is constructed explicitly and lazily during exploration (i.e., on-the-fly). The symbolic approach tries to overcome the state-space explosion obstacle by symbolically encoding the state-space in a concise way using decision diagrams. However, this symbolic construction is not performed on-the-fly as in the explicit approach. In order to take advantage of the best of both worlds, <i>hybrid approaches</i> are proposed as combinations of explicit and symbolic approaches. A hybrid approach is usually based on an on-the-fly construction of an explicit graph of symbolic nodes, where each symbolic node encodes a subset of states by means of binary decision diagrams. An alternative to the standard Büchi automata, called Testing automata have never been used before for hybrid model checking. In addition, in previous work, we have shown that <i>Generalized Testing Automata</i> (TGTA) can outperform the Büchi automata for explicit and symbolic model checking of stutter-invariant LTL properties. In this work, we investigate the use of these TGTA to improve hybrid model checking. We show how traditional hybrid approaches based on Generalized Büchi Automata (TGBA) can be adapted to obtain TGTA-based hybrid approaches. Then, each original approach is experimentally compared against its TGTA variant. The results show that these new variants are statistically more efficient.

Latecki <i>et al.</i> introduced the notion of 2D and 3D well-composed images, <i>i.e.</i>, a class of images free from the “connectivities paradox” of digital topology. Unfortunately natural and synthetic images are not <i>a priori</i> 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.

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.