Publications

Learning endmember dynamics in multitemporal hyperspectral data using a state-space model formulation

By Lucas Drumetz, Mauro Dalla Mura, Guillaume Tochon, Ronan Fablet

2020-01-24

In Proceedings of the 45th IEEE international conference on acoustics, speech, and signal processing (ICASSP)

Abstract

Hyperspectral image unmixing is an inverse problem aiming at recovering the spectral signatures of pure materials of interest (called endmembers) and estimating their proportions (called abundances) in every pixel of the image. However, in spite of a tremendous applicative potential and the avent of new satellite sensors with high temporal resolution, multitemporal hyperspectral unmixing is still a relatively underexplored research avenue in the community, compared to standard image unmixing. In this paper, we propose a new framework for multitemporal unmixing and endmember extraction based on a state-space model, and present a proof of concept on simulated data to show how this representation can be used to inform multitemporal unmixing with external prior knowledge, or on the contrary to learn the dynamics of the quantities involved from data using neural network architectures adapted to the identification of dynamical systems.

Continue reading

Performance comparison of several folding strategies

By Jim Newton

2020-01-14

In Trends in functional programming

Abstract

In this article we examine the computation order and consequent performance of three different conceptual implementations of the fold function. We explore a set of performance based experiments on different implementations of this function. In particular, we contrast the fold-left implementation with two other implements we refer to as pair-wise-fold and tree-like-fold. We explore two application areas: ratio arithmetic and Binary Decisions Diagram construction. We demonstrate several cases where the performance of certain algorithms is very different depending on the approach taken. In particular iterative computations where the object size accumulates are good candidates for the tree-like-fold.

Continue reading

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

By Didier Verna

2019-11-06

In TUGboat

Abstract

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.

Continue reading

Connected filters on generalized shape-spaces

By Lê Duy Huỳnh, Nicolas Boutry, Thierry Géraud

2019-09-20

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.

Continue reading

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