We propose an automatic system to classify images of galaxies with varying resolution. Morphologically typing galaxies is a difficult task in particular for distant galaxies convolved by a point-spread function and suffering from a poor signal-to-noise ratio. In the context of the first phase of the project EFIGI (extraction of the idealized shapes of galaxies in imagery), we present the three steps of our software: cleaning, dimensionality reduction and supervised learning. We present preliminary results derived from a subset of 774 galaxies from the Principal Galaxies Catalog and compare them to human classifications made by astronomers. We use g-band images from the Sloan Digital Sky Survey. Finally, we discuss future improvements which we intend to implement before releasing our tool to the community.

Dans cette thèse nous étudions la minimisation d’énergies markoviennes rencontrées dans les domaines du traitement des images et de la vision par ordinateur. Nous proposons des algorithmes de minimisation exacte pour différents types d’énergies. Ces algorithmes ont l’intérêt de fournir un minimum global quand bien même l’énergie n’est pas convexe. Enfin, nous mettons en évidence quelques liens entre les champs de Markov binaires et la morphologie mathématique. La version finale de ce manuscrit suit les recommandations des rapporteurs.

This paper sheds new light on minimization of the total variation under the $L^1$-norm as data fidelity term ($L^1+TV$) and its link with mathematical morphology. It is well known that morphological filters enjoy the property of being invariant with respect to any change of contrast. First, we show that minimization of $L^1+TV$ yields a self-dual and contrast invariant filter. Then, we further constrain the minimization process by only optimizing the grey levels of level sets of the image while keeping their boundaries fixed. This new constraint is maintained thanks to the Fast Level Set Transform which yields a complete representation of the image as a tree. We show that this filter can be expressed as a Markov Random Field on this tree. Finally, we present some results which demonstrate that these new filters can be particularly useful as a preprocessing stage before segmentation.

In this paper, we present fast algorithms for area opening and closing on grayscale images. Salembier’s max-tree based algorithm is one of the well known methods to perform area opening. It makes use of a special representation where each node in the tree stands for a flat region and the tree itself is oriented towards the maxima of the grayscale image. Pruning the tree with respect to some attribute, e.g., the area, boils down to attribute opening. Following the same approach, we propose an algorithm for area opening (closing) without building the max-tree (min-tree). Our algorithm exhibit considerable performance compared to the state-of-the art in this domain.

This paper describes a probabilistic method of inferring the position of a point with respect to a reference point knowing their relative spatial position to a third point. We address this problem in the case of incomplete information where only the angular spatial relationships are known. The use of probabilistic representations allows us to model prior knowledge. We derive exact formulae expressing the conditional probability of the position given the two known angles, in typical cases: uniform or Gaussian random prior distributions within rectangular or circular regions. This result is illustrated with respect to two different simulations: The first is devoted to the localization of a mobile phone using only angular relationships, the second, to geopositioning within a city. This last example uses angular relationships and some additional knowledge about the position.

APMC is a model checker dedicated to the quantitative verification of fully probabilistic systems against LTL formulas. Using a Monte-Carlo method in order to efficiently approximate the verification of probabilistic specifications, it could be used naturally in a distributed framework. We present here the tool and his distribution scheme, together with extensive performance evaluation, showing the scalability of the method, even on clusters containing 500+ heterogeneous workstations.

Model checking is an algorithmic method allowing to automatically verify if a system which is represented as a Kripke model satisfies a given specification. Specifications are usually expressed by formulas of temporal logic. The first objective of this paper is to give an overview of methods able to verify probabilistic systems. Models of such systems are labelled discrete time Markov chains and specifications are expressed in extensions of temporal logic by probabilistic operators. The second objective is to focus on complexity of these methods and to answer the question: can probabilistic verification be efficiently approximated? In general, the answer is negative. However, in many applications, the specification formulas can be expressed in some positive fragment of linear time temporal logic. In this paper, we show how some simple randomized approximation algorithms can improve the efficiency of the verification of such probabilistic specifications.

This paper presents some features of the Vaucanson platform. We describe some original algorithms on weighted automata and transducers (computation of the quotient, conversion of a regular expression into a weighted automaton, and composition). We explain how complex declarations due to the generic programming are masked from the user and finally we present a proposal for an XML format that allows implicit descriptions for simple types of automata.