Publications

Parallel satisfiability solver based on hybrid partitioning method

Abstract

This paper presents a hybrid partitioning method used to improve the performance of solving a Satisfiability (SAT) problems. The principle of our approach consist firstly to apply a static partitioning to decompose the search tree in finite set of disjoint sub-trees, than assign each sub-tree to one computing core. However it is not easy to choose the relevant branching variables to partition the search tree. We propose in this context to partition the search tree according to the variables that occur more frequently then others. The advantage of this method is that it gives a good disjoint sub- trees. However, the drawback is the imbalance load between all computing cores of the system. To overcome this drawback, we propose as novelty to extend the static partitioning by combining with a new dynamic partitioning that assure a good load balancing between cores. Each time a new waiting core is detected, the dynamic partitioning selects automatically using an estimation function the computing core which has the most work to do in order to partition dynamically its sub-tree in two parts. It keeps one part and gives the second part to the waiting core. Preliminary result show that a good speedup is achieved using our hybrid method.

Continue reading

Introducing the Dahu pseudo-distance

Abstract

The minimum barrier (MB) distance is defined as the minimal interval of gray-level values in an image along a path between two points, where the image is considered as a vertex-valued graph. Yet this definition does not fit with the interpretation of an image as an elevation map, i.e. a somehow continuous landscape. In this paper, based on the discrete set-valued continuity setting, we present a new discrete definition for this distance, which is compatible with this interpretation, while being free from digital topology issues. Amazingly, we show that the proposed distance is related to the morphological tree of shapes, which in addition allows for a fast and exact computation of this distance. That contrasts with the classical definition of the MB distance, where its fast computation is only an approximation.

Continue reading

Morphological analysis of brownian motion for physical measurements

Abstract

Brownian motion is a well-known, apparently chaotic mo- tion affecting microscopic objects in fluid media. The mathematical and physical basis of Brownian motion have been well studied but not often exploited. In this article we propose a particle tracking methodology based on mathematical morphology, suitable for Brownian motion analysis, which can provide difficult physical measurements such as the local temperature and viscosity. We illustrate our methodology on simulation and real data, showing that interesting phenomena and good precision can be achieved.

Continue reading

Morphological hierarchical image decomposition based on Laplacian 0-crossings

Abstract

A method of text detection in natural images, to be turn into an effective embedded software on a mobile device, shall be both efficient and lightweight. We observed that a simple method based on the morphological Laplace operator can do the trick: we can construct in quasi-linear time a hierarchical image decomposition / simplification based on its 0-crossings, and search for some text in the resulting tree. Yet, for this decomposition to be sound, we need “0-crossings” to be Jordan curves, and to that aim, we rely on some discrete topology tools. Eventually, the hierarchical representation is the morphological tree of shapes of the Laplacian sign. Moreover, we provide an algorithm with linear time complexity to compute this representation. We expect that the proposed hierarchical representation can be useful in some applications other than text detection.

Continue reading

Periodic area-of-motion characterization for bio-medical applications

Abstract

Many bio-medical applications involve the analysis of sequences for motion characterization. In this article, we consider 2D+t sequences where a particular motion (e.g. a blood flow) is associated with a specific area of the 2D image (e.g. an artery) but multiple motions may exist simultaneously in the same sequences (e.g. there may be several blood vessels present, each with their specific flow). The characterization of this type of motion typically involves first finding the areas where motion is present, followed by an analysis of these motions: speed, regularity, frequency, etc. In this article, we propose a methodology called “area-of-motion characterization” suitable for simultaneously detecting and characterizing areas where motion is present in a sequence. We can then classify this motion into consistent areas using unsupervised learning and produce directly usable metrics for various ap- plications. We illustrate this methodology for the analysis of cilia motion on ex-vivo human samples, and we apply and validate the same methodology for blood flow analysis in fish embryo.

Continue reading

Programmatic manipulation of Common Lisp type specifiers

Abstract

In this article we contrast the use of the s-expression with the BDD (Binary Decision Diagram) as a data structure for programmatically manipulating Common Lisp type specifiers. The s-expression is the de facto standard surface syntax and also programmatic representation of the type specifier, but the BDD data structure offers advantages: most notably, type equivalence checks using s-expressions can be computationally intensive, whereas the type equivalence check using BDDs is a check for object identity. As an implementation and performance experiment, we define the notion of maximal disjoint type decomposition, and discuss implementations of algorithms to compute it: a brute force iteration, and as a tree reduction. The experimental implementations represent type specifiers by both aforementioned data structures, and we compare the performance observed in each approach.

Continue reading

Analysis of algorithms calculating the maximal disjoint decomposition of a set

Abstract

In this article we demonstrate 4 algorithms for calculating the maximal disjoint decomposition of a given set of types. We discuss some advantages and disadvantages of each, and compare their performance. We extended currently known work to describe an efficient algorithm for manipulating binary decision diagrams representing types in a programming language which supports subtyping viewed as subsets.

Continue reading

Contributions to LTL and $\omega$-automata for model checking

Abstract

Continue reading

The MIT Lincoln Laboratory 2016 speaker recognition system

Abstract

This document presents the system submission for the group composed of MIT Lincoln Laboratory, Johns Hopkins University (JHU), Laboratoire de Recherche et de Développement de l’EPITA (LRDE) and Universidad Autónoma de Madrid (ATVS). The primary submission is a combination of four systems focused on i-vector systems. Two secondary submissions are also included

Continue reading

A study of well-composedness in $n$-d

Abstract

Digitization of the real world using real sensors has many drawbacks; in particular, we loose “well-composedness” in the sense that two digitized objects can be connected or not depending on the connectivity we choose in the digital image, leading then to ambiguities. Furthermore, digitized images are arrays of numerical values, and then do not own any topology by nature, contrary to our usual modeling of the real world in mathematics and in physics. Loosing all these properties makes difficult the development of algorithms which are “topologically correct” in image processing: e.g., the computation of the tree of shapes needs the representation of a given image to be continuous and well-composed; in the contrary case, we can obtain abnormalities in the final result. Some well-composed continuous representations already exist, but they are not in the same time $n$-dimensional and self-dual. In fact, $n$-dimensionality is crucial since usual signals are more and more 3-dimensional (like 2D videos) or 4-dimensional (like 4D Computerized Tomography-scans), and self-duality is necessary when a same image can contain different objects with different contrasts. We developed then a new way to make images well-composed by interpolation in a self-dual way and in $n$-D; followed with a span-based immersion, this interpolation becomes a self-dual continuous well-composed representation of the initial $n$-D signal. This representation benefits from many strong topological properties: it verifies the intermediate value theorem, the boundaries of any threshold set of the representation are disjoint union of discrete surfaces, and so on.

Continue reading