Publications

Mechanizing the minimization of deterministic generalized Büchi automata

By Souheib Baarir, Alexandre Duret-Lutz

2014-03-21

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

Abstract

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.

Continue reading

LTL translation improvements in Spot 1.0

By Alexandre Duret-Lutz

2014-03-06

In International Journal on Critical Computer-Based Systems

Abstract

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.

Continue reading

Tree-based shape spaces: Definition and applications in image processing and computer vision

By Yongchao Xu

2013-12-12

In

Abstract

The classical framework of connected filters relies on the removal of some connected components of a graph. To apply those filters, it is often useful to transform an image into a component tree, and to prune the tree to simplify the original image. Those trees have some remarkable properties for computer vision. A first illustration of their usefulness is the proposition of a local feature detector, truly invariant to change of contrast. which allows us to obtain the state-of-the-art results in image registration and in multi-view 3D reconstruction. Going further in the use of those trees, we propose to expand the classical framework of connected filters. For this, we introduce the notion of tree-based shape spaces: instead of filtering the connected components of the graph corresponding to the image, we propose to filter the connected components of the graph given by the component tree of the image. This general framework, which we call shape-based morphology can be used for object detection and segmentation, hierarchical segmentation, and image filtering. Many applications and illustrations show the usefulness of the proposed framework.

Continue reading

Planting, growing and pruning trees: Connected filters applied to document image analysis

By Guillaume Lazzara, Thierry Géraud, Roland Levillain

2013-12-10

In Proceedings of the 11th IAPR international workshop on document analysis systems (DAS)

Abstract

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.

Continue reading

Text detection in street level image

By Jonathan Fabrizio, Beatriz Marcotegui, Matthieu Cord

2013-11-05

In Pattern Analysis and Applications

Abstract

Text detection system for natural images is a very challenging task in Computer Vision. Image acquisition introduces distortion in terms of perspective, blurring, illumination, and characters which may have very different shape, size, and color. We introduce in this article a full text detection scheme. Our architecture is based on a new process to combine a hypothesis generation step to get potential boxes of text and a hypothesis validation step to filter false detections. The hypothesis generation process relies on a new efficient segmentation method based on a morphological operator. Regions are then filtered and classified using shape descriptors based on Fourier, Pseudo Zernike moments and an original polar descriptor, which is invariant to rotation. Classification process relies on three SVM classifiers combined in a late fusion scheme. Detected characters are finally grouped to generate our text box hypotheses. Validation step is based on a global SVM classification of the box content using dedicated descriptors adapted from the HOG approach. Results on the well-known ICDAR database are reported showing that our method is competitive. Evaluation protocol and metrics are deeply discussed and results on a very challenging street-level database are also proposed.

Continue reading

Three SCC-based emptiness checks for generalized Büchi automata

By Étienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud

2013-10-09

In Proceedings of the 19th international conference on logic for programming, artificial intelligence, and reasoning (LPAR’13)

Abstract

The automata-theoretic approach for the verification of linear time properties involves checking the emptiness of a Büchi automaton. However generalized Büchi automata, with multiple acceptance sets, are preferred when verifying under weak fairness hypotheses. Existing emptiness checks for which the complexity is independent of the number of acceptance sets are all based on the enumeration of Strongly Connected Components (SCCs). In this paper, we review the state of the art SCC enumeration algorithms to study how they can be turned into emptiness checks. This leads us to define two new emptiness check algorithms (one of them based on the Union Find data structure), introduce new optimizations, and show that one of these can be of benefit to a classic SCCs enumeration algorithm. We have implemented all these variants to compare their relative performances and the overhead induced by the emptiness check compared to the corresponding SCCs enumeration algorithm. Our experiments shows that these three algorithms are comparable.

Continue reading

LTL model checking with Neco

By Łukasz Fronc, Alexandre Duret-Lutz

2013-06-15

In Proceedings of the 11th international symposium on automated technology for verification and analysis (ATVA’13)

Abstract

We introduce neco-spot, an LTL model checker for Petri net models. It builds upon Neco, a compiler turning Petri nets into native shared libraries that allows fast on-the-fly exploration of the state-space, and upon Spot, a C++ library of model-checking algorithms. We show the architecture of Neco and explain how it was combined with Spot to build an LTL model checker.

Continue reading

Manipulating LTL formulas using Spot 1.0

By Alexandre Duret-Lutz

2013-06-15

In Proceedings of the 11th international symposium on automated technology for verification and analysis (ATVA’13)

Abstract

We present a collection of command-line tools designed to generate, filter, convert, simplify, lists of Linear-time Temporal Logic formulas. These tools were introduced in the release 1.0 of Spot, and we believe they should be of interest to anybody who has to manipulate LTL formulas. We focus on two tools in particular: ltlfilt, to filter and transform formulas, and ltlcross to cross-check LTL-to-Büchi-Automata translators.

Continue reading

Unsupervised methods for speaker diarization: An integrated and iterative approach

By S. Shum, Najim Dehak, Réda Dehak, J. Glass

2013-06-07

In IEEE Transactions on Audio, Speech, and Language Processing

Abstract

In speaker diarization, standard approaches typically perform speaker clustering on some initial segmentation before refining the segment boundaries in a re-segmentation step to obtain a final diarization hypothesis. In this paper, we integrate an improved clustering method with an existing re-segmentation algorithm and, in iterative fashion, optimize both speaker cluster assignments and segmentation boundaries jointly. For clustering, we extend our previous research using factor analysis for speaker modeling. In continuing to take advantage of the effectiveness of factor analysis as a front-end for extracting speaker-specific features (i.e., i-vectors), we develop a probabilistic approach to speaker clustering by applying a Bayesian Gaussian Mixture Model (GMM) to principal component analysis (PCA)-processed i-vectors. We then utilize information at different temporal resolutions to arrive at an iterative optimization scheme that, in alternating between clustering and re-segmentation steps, demonstrates the ability to improve both speaker cluster assignments and segmentation boundaries in an unsupervised manner. Our proposed methods attain results that are comparable to those of a state-of-the-art benchmark set on the multi-speaker CallHome telephone corpus. We further compare our system with a Bayesian nonparametric approach to diarization and attempt to reconcile their differences in both methodology and performance.

Continue reading

Salient level lines selection using the Mumford-Shah functional

By Yongchao Xu, Thierry Géraud, Laurent Najman

2013-05-27

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

Abstract

Many methods relying on the morphological notion of shapes, (i.e., connected components of level sets) have been proved to be very useful for pattern analysis and recognition. Selecting meaningful level lines (boundaries of level sets) yields to simplify images while preserving salient structures. Many image simplification and/or segmentation methods are driven by the optimization of an energy functional, for instance the Mumford-Shah functional. In this article, we propose an efficient shape-based morphological filtering that very quickly compute to a locally (subordinated to the tree of shapes) optimal solution of the piecewise-constant Mumford-Shah functional. Experimental results demonstrate the efficiency, usefulness, and robustness of our method, when applied to image simplification, pre-segmentation, and detection of affine regions with viewpoint changes.

Continue reading

Search

Tags