Connected filters on generalized shape-spaces
In Pattern Recognition Letters
Abstract
Classical hierarchical image representations and connected filters work on sets of connected components (CC). These approaches can be defective to describe the relations between disjoint objects or partitions on images. In practice, objects can be made of several connected components in images (due to occlusions for example), therefore it can be interesting to be able to take into account the relationship between these components to be able to detect the whole object. In Mathematical Morphology, second-generation connectivity (SGC) and tree-based shape-space study this relation between the connected components of an image. However, they have limitations. For this reason, we propose in this paper an extension of the usual shape-space paradigm into what we call a Generalized Shape-Space (GSS). This new paradigm allows to analyze any graph of connected components hierarchically and to filter them thanks to connected operators.
Combining parallel emptiness checks with partial order reductions
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.
Generic emptiness check for fun and profit
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.
Towards more efficient parallel SAT solving
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.
Braids of partitions for the hierarchical representation and segmentation of multimodal images
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.
One more step towards well-composedness of cell complexes over $n$-D pictures
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.
Estimation du niveau de bruit par arbre des formes et statistiques non paramétriques
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.
Filtres connexes multivariés par fusion d’arbres de composantes
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.