Publications

Extending testing automata to all LTL

By Ala Eddine Ben Salem

2015-05-19

In Proceedings of the 35th IFIP international conference on formal techniques for distributed objects, components and systems (FORTE’15)

Abstract

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.

Continue reading

How to make $n$D images well-composed without interpolation

By Nicolas Boutry, Thierry Géraud, Laurent Najman

2015-05-14

In Proceedings of the IEEE international conference on image processing (ICIP)

Abstract

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.

Continue reading

The Hanoi Omega-Automata format

By Tomáš Babiak, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Křetínský, David Müller, David Parker, Jan Strejček

2015-04-27

In Proceedings of the 27th international conference on computer aided verification (CAV’15)

Abstract

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.

Continue reading

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

Search

Tags