Publications

Generic emptiness check for fun and profit

Christel Baier · František Blahoudek · Alexandre Duret-Lutz · Joachim Klein · David Müller · Jan Strejček

We present a new algorithm for checking the emptiness of $\omega$-automata with an Emerson-Lei acceptance condition (i.e., a positive Boolean formula over sets of states or transitions that must be visited infinitely or finitely often). The algorithm can also solve the model checking problem of probabilistic positiveness of MDP under a property given as a deterministic Emerson-Lei automaton. Although both these problems are known to be NP-complete and our algorithm is exponential in general, it runs in polynomial time for simpler acceptance conditions like generalized Rabin, Streett, or parity. In fact, the algorithm provides a unifying view on emptiness checks for these simpler automata classes. We have implemented the algorithm in Spot and PRISM and our experiments show improved performance over previous solutions.

Weakly well-composed cell complexes over $n$D pictures

Nicolas Boutry · Rocio Gonzalez-Diaz · Maria-Jose Jimenez

In previous work we proposed a combinatorial algorithm to “locally repair” the cubical complex $Q(I)$ that is canonically associated with a given 3D picture I. The algorithm constructs a 3D polyhedral complex $P(I)$ which is homotopy equivalent to $Q(I)$ and whose boundary surface is a 2D manifold. A polyhedral complex satisfying these properties is called <i>well-composed</i>. In the present paper we extend these results to higher dimensions. We prove that for a given $n$-dimensional picture the obtained cell complex is well-composed in a weaker sense but is still homotopy equivalent to the initial cubical complex.

Intervertebral disc segmentation using mathematical morphology—A CNN-free approach

Edwin Carlinet · Thierry Géraud

In the context of the challenge of “automatic InterVertebral Disc (IVD) localization and segmentation from 3D multi-modality MR images” that took place at MICCAI 2018, we have proposed a segmentation method based on simple image processing operators. Most of these operators come from the mathematical morphology framework. Driven by some prior knowledge on IVDs (basic information about their shape and the distance between them), and on their contrast in the different modalities, we were able to segment correctly almost every IVD. The most interesting feature of our method is to rely on the morphological structure called the Three of Shapes, which is another way to represent the image contents. This structure arranges all the connected components of an image obtained by thresholding into a tree, where each node represents a particular region. Such structure is actually powerful and versatile for pattern recognition tasks in medical imaging.

Advanced ports toolkit: Near-perfect packing-list generation

Marc Espie

Estimating the noise level function with the tree of shapes and non-parametric statistics

Baptiste Esteban · Guillaume Tochon · Thierry Géraud

The knowledge of the noise level within an image is a valuableinformation for many image processing applications. Estimating the noise level function (NLF) requires the identification of homogeneous regions, upon which the noise parameters are computed. Sutour et al. have proposed a method to estimate this NLF based on the search for homogeneous regions of square shape. We generalize this method to the search for homogeneous regions with arbitrary shape thanks to the tree of shapes representation of the image under study, thus allowing a more robust and precise estimation of the noise level function.

Quickref: Common Lisp reference documentation as a stress test for Texinfo

Didier Verna

Quickref is a global documentation project for the Common Lisp ecosystem. It creates reference manuals automatically by introspecting libraries and generating corresponding documentation in Texinfo format. The Texinfo files may subsequently be converted into PDF or HTML. Quickref is non-intrusive: software developers do not have anything to do to get their libraries documented by the system.Quickref may be used to create a local website documenting your current, partial, working environment, but it is also able to document the whole Common Lisp ecosystem at once. The result is a website containing almost two thousand reference manuals. Quickref provides a Docker image for an easy recreation of this website, but a public version is also available and actively maintained.Quickref constitutes an enormous and successful stress test for Texinfo. In this paper, we give an overview of the design and architecture of the system, describe the challenges and difficulties in generating valid Texinfo code automatically, and put some emphasis on the currently remaining problems and deficiencies.

Benchmark on automatic 6-month-old infant brain segmentation algorithms: The iSeg-2017 challenge

Li Wang · Dong Nie · Guannan Li · Élodie Puybareau · Jose Dolz · Qian Zhang · Fan Wang · Jing Xia · Zhengwang Wu · Jiawei Chen · Kim-Han Thung · Toan Duc Bui · Jitae Shin · Guodong Zeng · Guoyan Zheng · Vladimir S. Fonov · Andrew Doyle · Yongchao Xu · Pim Moeskops · Josien P. W. Pluim · Christian Desrosiers · Ismail Ben Ayed · Gerard Sanroma · Oualid M. Benkarim · Adrià Casamitjana · Verónica Vilaplana · Weili Lin · Gang Li · Dinggang Shen

Image segmentation; Magnetic resonance imaging; Manuals; Pediatrics; Biomedical imaging; Testing; White matter

Accurate segmentation of infant brain magnetic resonance (MR) images into white matter (WM), gray matter (GM), and cerebrospinal fluid (CSF) is an indispensable foundation for early studying of brain growth patterns and morphological changes in neurodevelopmental disorders. Nevertheless, in the isointense phase (approximately 6-9 months of age), due to inherent myelination and maturation process, WM and GM exhibit similar levels of intensity in both T1-weighted (T1w) and T2-weighted (T2w) MR images, making tissue segmentation very challenging. Despite many efforts were devoted to brain segmentation, only few studies have focused on the segmentation of 6-month infant brain images. With the idea of boosting methodological development in the community, iSeg-2017 challenge (http://iseg2017.web.unc.edu) provides a set of 6-month infant subjects with manual labels for training and testing the participating methods. Among the 21 automatic segmentation methods participating in iSeg-2017, we review the 8 top-ranked teams, in terms of Dice ratio, modified Hausdorff distance and average surface distance, and introduce their pipelines, implementations, as well as source codes. We further discuss limitations and possible future directions. We hope the dataset in iSeg-2017 and this review article could provide insights into methodological development for the community.

Document detection in videos captured by smartphones using a saliency-based method

Minh Ôn Vũ Ngọc · Jonathan Fabrizio · Thierry Géraud

Smartphones are now widely used to digitizepaper documents. Document detection is the first importantstep of the digitization process. Whereas many methods extractlines from contours as candidates for the document boundary, we present in this paper a region-based approach. A key feature of our method is that it relies on visual saliency, using a recent distance existing in mathematical morphology. We show that the performance of our method is competitive with state-of-the-art methods on the ICDAR Smartdoc 2015 Competition dataset.

Filtres connexes multivariés par fusion d’arbres de composantes

Edwin Carlinet · Thierry Géraud

Les arbres de composantes fournissent une représentation d’images de haut niveau, hiérarchisée et invariante par contraste, adaptée à de nombreuses tâches de traitement d’image. Pourtant, ils sont mal définis sur des données multivariées, telle que celles des images couleur, des images multimodalités, des images multibande, etc. Les solutions courantes, telles que le traitement marginal, ou l’imposition d’un ordre total sur les données, ne sont pas satisfaisantes et génèrent de nombreux problèmes, tels que des artefacts visuels, la perte d’invariances, etc. Dans cet article, inspiré par la manière dont l’arbre des formes multivariés (MToS) a été défini, nous proposons une définition pour un Min-Tree ou un Max-Tree multivarié. Nous n’imposons pas un ordre total arbitraire aux valeurs; nous utilisons uniquement la relation d’inclusion entre les composantes. En conséquence, nous introduisons une nouvelle classe d’ouvertures et de fermetures connectées multivariées.