Publications

Seminator: A tool for semi-determinization of omega-automata

Abstract

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.

Continue reading

La pseudo-distance du dahu

Abstract

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.

Continue reading

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