Publications

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

By Étienne Renault

2014-12-05

In

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

Traitement d’images multivariées avec l’arbre des formes

By Edwin Carlinet, Thierry Géraud

2014-11-17

In

Abstract

L’Arbre des Formes (ToS) est un arbre morphologique qui fournit une représentation hiérarchique de l’image auto-duale et invariante par changement de contraste. De ce fait, il est adapté à de nombreuses applications de traitement d’images. Néanmoins, on se heurte à des problèmes avec l’Arbre des Formes lorsqu’on doit traiter des images couleurs car sa définition tient uniquement en niveaux de gris. Les solutions les plus courantes sont alors d’effectuer un traitement composante par composante (marginal) ou d’imposer un ordre total. Ces solutions ne sont généralement pas satisfaisantes et font survenir des problèmes (des artefacts de couleur, des pertes de propriétés…) Dans cet article, nous insistons sur la nécessité d’une représentation à la fois auto-duale et invariante par changement de contraste et nous proposons une méthode qui construit un Arbre des Formes unique en fusionnant des formes issues des composantes marginales tout en préservant les propriétés intrinsèques de l’arbre. Cette méthode s’affranchit de tout relation d’ordre totale en utilisant uniquement la relation d’inclusion entre les formes et en effectuant une fusion dans l’espace des formes. Finalement, nous montrerons la pertinence de notre méthode et de la structure en les illustrant sur de la simplification d’images et de la segmentation interactive.

Continue reading

Une généralisation du <i>bien-composé</i> à la dimension $n$

By Nicolas Boutry, Thierry Géraud, Laurent Najman

2014-11-17

In

Abstract

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$.

Continue reading

Tree-based morse regions: A topological approach to local feature detection

By Yongchao Xu, Thierry Géraud, Pascal Monasse, Laurent Najman

2014-10-03

In IEEE Transactions on Image Processing

Abstract

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 (e.g., 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.

Continue reading

Improving the model checking of stutter-invariant LTL properties

By Ala Eddine Ben Salem

2014-09-25

In

Abstract

Software systems have become ubiquitous in our everyday life. They replace humans for critical tasks that involve high costs and even human lives. The serious consequences caused by the failure of such systems make crucial the use of rigorous methods for system validation. One of the widely-used formal verification methods is the automata-theoretic approach to model checking. It takes as input a model of the system and a property, and answers if the model satisfies or not the property. To achieve this goal, it translates the negation of the property in an automaton and checks whether the product of the model and this automaton is empty. Although it is automatic, this approach suffers from the combinatorial explosion of the resulting product. To tackle this problem, especially when checking stutter-invariant LTL properties, we firstly improve the two-pass verification algorithm of Testing automata (TA), then we propose a transformation of TA into a normal form (STA) that only requires a single-pass verification algorithm. We also propose a new type of automata: the TGTA. These automata also enable a check in a single-pass and without adding artificial states : it combines the benefits of TA and generalized Büchi automata (TGBA). TGTA improve the explicit and symbolic model checking approaches. In particular, by combining TGTA with the saturation technique, the performances of the symbolic approach has been improved by an order of magnitude compared to TGBA. Used in hybrid approaches TGTA prove complementary to TGBA. All the contributions of this work have been implemented in SPOT and LTS-ITS, respectively, an explicit and a symbolic open source model-checking libraries.

Continue reading

Practical genericity: Writing image processing algorithms both reusable and efficient

By Roland Levillain, Thierry Géraud, Laurent Najman, Edwin Carlinet

2014-09-10

In Progress in pattern recognition, image analysis, computer vision, and applications – proceedings of the 19th iberoamerican congress on pattern recognition (CIARP)

Abstract

An important topic for the image processing and pattern recognition community is the construction of open source and efficient libraries. An increasing number of software frameworks are said to be generic: they allow users to write reusable algorithms compatible with many input image types. However, this design choice is often made at the expense of performance. We present an approach to preserve efficiency in a generic image processing framework, by leveraging data types features. Variants of generic algorithms taking advantage of image types properties can be defined, offering an adjustable trade-off between genericity and efficiency. Our experiments show that these generic optimizations can match dedicated code in terms of execution times, and even sometimes perform better than routines optimized by hand. Digital Topology software should reflect the generality of the underlying mathematics: mapping the latter to the former requires genericity. By designing generic solutions, one can effectively reuse digital topology data structures and algorithms. We propose an image processing framework focused on the Generic Programming paradigm in which an algorithm on the paper can be turned into a single code, written once and usable with various input types. This approach enables users to design and implement new methods at a lower cost, try cross-domain experiments and help generalize results.

Continue reading

Search

Tags