La distance de la barrière minimum est définie comme le plus petit intervalle de l’ensemble des niveaux de gris le long d’un chemin entre deux points dans une image. Pour cela, on considère que l’image est un graphe à valeurs sur les sommets. Cependant, cette définition ne correspond pas à l’interprétation d’une image comme étant une carte d’élévation, c’est-à-dire, un paysage continu d’une manière ou d’une autre. En se plaçant dans le cadre des fonctions multivoques, nous présentons une nouvelle définition pour cette distance. Cette définition, compatible avec l’interprétation paysagère, est dénuée de problèmes topologiques bien qu’en restant dans un monde discret. Nous montrons que la distance proposée est reliée à la structure morphologique d’arbre des formes, qui permet de surcroît un calcul rapide et exact de cette distance. Cela se démarque de sa définition classique, pour laquelle le seul calcul rapide n’est qu’approximatif.

Exploiting multi-core architectures is a way to tackle the CPU time consumption when solving SAT- isfiability (SAT) problems. Portfolio is one of the main techniques that implements this principle. It consists in making several solvers competing, on the same problem, and the winner will be the first that answers. In this work, we improved this technique by using a learning schema, namely the Exploration- Exploitation using Exponential weight (EXP3), that allows smart resource allocations. Our contribution is adapted to situations where we have to solve a bench of SAT instances issued from one or several sequence of problems. Our experiments show that our approach achieves good results.

We present a tool that transforms nondeterministic $\omega$-automata to semi-deterministic $\omega$-automata. The tool Seminator accepts transition-based generalized Büchi automata (TGBA) as an input and produces automata with two kinds of semi-determinism. The implemented procedure performs degeneralization and semi-determinization simultaneously and employs several other optimizations. We experimentally evaluate Seminator in the context of LTL to semi-deterministic automata translation.

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.

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.

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.

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.

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.

We present new parallel explicit emptiness checks for LTL model checking. Unlike existing parallel emptiness checks, these are based on a Strongly Connected Component (SCC) enumeration, support generalized Büchi acceptance, and require no synchronization points nor recomputing 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 checked. Besides these basic algorithms, we present one architectural variant isolating threads that write to the union-find, and one extension that decomposes the automaton based on the strength of its SCCs to use more optimized emptiness checks. The results from an extensive experimentation of our algorithms and their variations show encouraging performances, especially when the decomposition technique is used.