Publications

Combining parallel emptiness checks with partial order reductions

By Denis Poitrenaud, Étienne Renault

2019-08-02

In Proceedings of the 21st international conference on formal engineering methods (ICFEM’19)

Abstract

In explicit state model checking ofconcurrent systems, multicore emptiness checks and partial order reductions (POR) are two major techniques to handle large state spaces. The first one tries to take advantage of multi-core architectures while the second one may decrease exponentially the size of the state space to explore. For checking LTL properties, Bloemen and van de Pol [2] shown that the best performance is currently obtained using their multi-core SCC-based emptiness check. However, combining the latest SCC-based algorithm with POR is not trivial since a condition on cycles, the proviso, must be enforced on an algorithm which processes collaboratively cycles. In this paper, we suggest a pessimistic approach to tackle this problem for liveness properties. For safety ones, we propose an algorithm which takes benefit from the information computed by the SCC-based algorithm. We also present new parallel provisos for both safety and liveness prop- erties that relies on other multi-core emptiness checks. We observe that all presented algorithms maintain good reductions and scalability.

Continue reading

Generic emptiness check for fun and profit

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

2019-07-29

In Proceedings of the 17th international symposium on automated technology for verification and analysis (ATVA’19)

Abstract

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.

Continue reading

Towards more efficient parallel SAT solving

By Ludovic Le Frioux

2019-07-03

In

Abstract

Boolean SATisfiability has been used successfully in many applicative contexts. This is due to the capability of modern SAT solvers to solve complex problems involving millions of variables. Most SAT solvers have long been sequential and based on the CDCL algorithm. The emergence of many-core machines opens new possibilities in this domain. There are numerous parallel SAT solvers that differ by their strategies, programming languages, etc. Hence, comparing the efficiency of the theoretical approaches in a fair way is a challenging task. Moreover, the introduction of a new approach needs a deep understanding of the existing solvers’ implementations. We present Painless: a framework to build parallel SAT solvers for many-core environments. Thanks to its genericness and modularity, it provides the implementation of basics for parallel SAT solving. It also enables users to easily create their parallel solvers based on new strategies. Painless allowed to build and test existing strategies by using different chunk of solutions present in the literature. We were able to easily mimic the behaviour of three state-of-the-art solvers by factorising many parts of their implementations. The efficiency of Painless was highlighted as these implementations are at least efficient as the original ones. Moreover, one of our solvers won the SAT Competition’18. Going further, Painless enabled to conduct fair experiments in the context of divide-and-conquer solvers, and allowed us to highlight original compositions of strategies performing better than already known ones. Also, we were able to create and test new original strategies exploiting the modular structure of SAT instances.

Continue reading

Braids of partitions for the hierarchical representation and segmentation of multimodal images

By Guillaume Tochon, Mauro Dalla Mura, Miguel Angel Veganzones, Thierry Géraud, Jocelyn Chanussot

2019-07-01

In Pattern Recognition

Abstract

Hierarchical data representations are powerful tools to analyze images and have found numerous applications in image processing. When it comes to multimodal images however, the fusion of multiple hierarchies remains an open question. Recently, the concept of braids of partitions has been proposed as a theoretical tool and possible solution to this issue. In this paper, we demonstrate the relevance of the braid structure for the hierarchical representation of multimodal images. We first propose a fully operable procedure to build a braid of partitions from two hierarchical representations. We then derive a framework for multimodal image segmentation, relying on an energetic minimization scheme conducted on the braid structure. The proposed approach is investigated on different multimodal images scenarios, and the obtained results confirm its ability to efficiently handle the multimodal information to produce more accurate segmentation outputs.

Continue reading

One more step towards well-composedness of cell complexes over $n$-D pictures

By Nicolas Boutry, Rocio Gonzalez-Diaz, Maria-Jose Jimenez

2019-06-18

In Proceedings of the 21st international conference on discrete geometry for computer imagery (DGCI)

Abstract

An $n$-D pure regular cell complex $K$ is weakly well-composed (wWC) if, for each vertex $v$ of $K$, the set of $n$-cells incident to $v$ is face-connected. In previous work we proved that if an $n$-D picture $I$ is digitally well composed (DWC) then the cubical complex $Q(I)$ associated to $I$ is wWC. If $I$ is not DWC, we proposed a combinatorial algorithm to locally repair $Q(I)$ obtaining an $n$-D pure simplicial complex $P_S(I)$ homotopy equivalent to $Q(I)$ which is always wWC. In this paper we give a combinatorial procedure to compute a simplicial complex $P_S(\bar{I})$ which decomposes the complement space of $|P_S(I)|$ and prove that $P_S(\bar{I})$ is also wWC. This paper means one more step on the way to our ultimate goal: to prove that the $n$-D repaired complex is continuously well-composed (CWC), that is, the boundary of its continuous analog is an $(n-1)$-manifold.

Continue reading

Estimation du niveau de bruit par arbre des formes et statistiques non paramétriques

By Baptiste Esteban, Guillaume Tochon, Thierry Géraud

2019-06-14

In Proceedings of the 27st symposium on signal and image processing (GRETSI)

Abstract

La connaissance du niveau de bruit dans une image est précieuse pour de nombreuses applications en traitement d’images. L’estimation de la fonction de niveau de bruit requiert l’identification des zones homogènes sur lesquelles les paramètres du bruit peuvent être calculés. Sutour et al. en 2015 ont proposé une méthode d’estimation de la fonction de niveau de bruit se basant sur la recherche de zones homogènes de forme carrée, donc inadaptées au contenu local de l’image. Nous généralisons cette méthode à la recherche de zones homogènes de forme quelconque en nous basant sur la représentation par arbre des formes de l’image étudiée, permettant ainsi une estimation plus robuste de la fonction de niveau de bruit.

Continue reading

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

By Edwin Carlinet, Thierry Géraud

2019-06-14

In Proceedings of the 27st symposium on signal and image processing (GRETSI)

Abstract

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.

Continue reading

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

By Baptiste Esteban, Guillaume Tochon, Thierry Géraud

2019-06-07

In Proceedings of the 18th international conference on computer analysis of images and patterns (CAIP)

Abstract

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.

Continue reading

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

By 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

2019-04-11

In IEEE Transactions on Medical Imaging

Abstract

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.

Continue reading

Standardized assessment of automatic segmentation of white matter hyperintensities: Results of the WMH segmentation challenge

By H. J. Kuijf, J. M. Biesbroek, J. de Bresser, R. Heinen, S. Andermatt, M. Bento, M. Berseth, M. Belyaev, M. J. Cardoso, A. Casamitjana, D. L. Collins, M. Dadar, A. Georgiou, M. Ghafoorian, D. Jin, A. Khademi, J. Knight, H. Li, X. Lladó, M. Luna, Q. Mahmood, R. McKinley, A. Mehrtash, S. Ourselin, B. Park, H. Park, S. H. Park, S. Pezold, Élodie Puybareau, L. Rittner, C. H. Sudre, S. Valverde, V. Vilaplana, R. Wiest, Yongchao Xu, Z. Xu, G. Zeng, J. Zhang, G. Zheng, C. Chen, W. van der Flier, F. Barkhof, M. A. Viergever, G. J. Biessels

2019-04-10

In IEEE Transactions on Medical Imaging

Abstract

Quantification of cerebral white matter hyperintensities (WMH) of presumed vascular origin is of key importance in many neurological research studies. Currently, measurements are often still obtained from manual segmentations on brain MR images, which is a laborious procedure. Automatic WMH segmentation methods exist, but a standardized comparison of the performance of such methods is lacking. We organized a scientific challenge, in which developers could evaluate their method on a standardized multi-center/-scanner image dataset, giving an objective comparison: the WMH Segmentation Challenge (https://wmh.isi.uu.nl/). Sixty T1+FLAIR images from three MR scanners were released with manual WMH segmentations for training. A test set of 110 images from five MR scanners was used for evaluation. Segmentation methods had to be containerized and submitted to the challenge organizers. Five evaluation metrics were used to rank the methods: (1) Dice similarity coefficient, (2) modified Hausdorff distance (95th percentile), (3) absolute log-transformed volume difference, (4) sensitivity for detecting individual lesions, and (5) F1-score for individual lesions. Additionally, methods were ranked on their inter-scanner robustness. Twenty participants submitted their method for evaluation. This paper provides a detailed analysis of the results. In brief, there is a cluster of four methods that rank significantly better than the other methods, with one clear winner. The inter-scanner robustness ranking shows that not all methods generalize to unseen scanners. The challenge remains open for future submissions and provides a public platform for method evaluation.

Continue reading

Search

Tags