Publications

Assimilation de données variationnelle de séries temporelles d’images sentinel-2 avec un modèle dynamique auto-supervisé

Abstract

Au cours des dernières années, l’apprentissage profond a acquis une importance croissante dans de nombreux domaines scientifiques, notamment en ce qui concerne le traitement d’images, et en particulier pour le traitement des données issues de satellites. Le paradigme le plus courant en ce qui concerne l’apprentissage profond est l’apprentissage supervisé, qui requiert une grande quantité de données annotées représentant la vérité terrain pour la tâche d’intérêt. Or, obtenir des données correctement annotées pose souvent des difficultés financières ou techniques importantes. Pour cette raison, nous nous plaçons ici dans le cadre de l’apprentissage auto-supervisé. Nous proposons un modèle d’apprentissage profond inspiré de la théorie de l’opérateur de Koopman qui apprend, à partir de séries temporelles d’images multispectrales Sentinel-2, à modéliser les dynamiques de long terme de réflectance des pixels. Après son entraînement, notre modèle peut être utilisé dans divers problèmes inverses faisant intervenir la dynamique temporelle pour résoudre différentes tâches telles que l’interpolation ou le débruitage de données.

Continue reading

From Spot 2.0 to Spot 2.10: What’s new?

Abstract

Spot is a C++17 library for LTL and $\omega$-automata manipulation, with command-line utilities, and Python bindings. This paper summarizes its evolution over the past six years, since the release of Spot 2.0, which was the first version to support $\omega$-automata with arbitrary acceptance conditions, and the last version presented at a conference. Since then, Spot has been extended with several features such as acceptance transformations, alternating automata, games, LTL synthesis, and more. We also shed some lights on the data-structure used to store automata.

Continue reading

Survey on smart homes: Vulnerabilities, risks, and countermeasures

Abstract

Over the last few years, the explosive growth of Internet of Things (IoT) has revolutionized the way we live and interact with each other as well as with various types of systems and devices which form part of the Information Communication Technology (ICT) infrastructure. IoT is having a significant impact on various application domains including healthcare, smart home, transportation, energy, agriculture, manufacturing, and many others. We focus on the smart home environment which has attracted a lot of attention from both academia and industry recently. The smart home provides a lot of convenience to home users but it also opens up various risks that threaten both the security and privacy of the users. In contrast to previous works on smart home security and privacy, we present an overview of smart homes from both academic and industry perspectives. Next we discuss the security requirements, challenges and threats associated with smart homes. Finally, we discuss countermeasures that can be deployed to mitigate the identified threats.

Continue reading

The reactive synthesis competition (SYNTCOMP): 2018-2021

Abstract

Continue reading

Some equivalence relation between persistent homology and morphological dynamics

Abstract

In Mathematical Morphology (MM), connected filters based on dynamics are used to filter the extrema of an image. Similarly, persistence is a concept coming from Persistent Homology (PH) and Morse Theory (MT) that represents the stability of the extrema of a Morse function. Since these two concepts seem to be closely related, in this paper we examine their relationship, and we prove that they are equal on $n$-D Morse functions, $n\geq 1$. More exactly, pairing a minimum with a $1$-saddle by dynamics or pairing the same $1$-saddle with a minimum by persistence leads exactly to the same pairing, assuming that the critical values of the studied Morse function are unique. This result is a step further to show how much topological data analysis and mathematical morphology are related, paving the way for a more in-depth study of the relations between these two research fields.

Continue reading

A generic approach to quantitative verification

Abstract

Continue reading

Automatically guided selection of a set of underwater calibration images

Abstract

Continue reading

Données, transparence et démocratie

Abstract

Bienvenue dans l’âge des données. Nos actions sur Internet sont enregistrées au profit d’entreprises qui valorisent ces données et offrent des services en échange. Pouvons-nous faire de même ? Pouvons-nous utiliser les données de l’état pour améliorer notre démocratie ?Depuis 2016, les données publiques doivent être ouvertes àà tous. Les citoyens peuvent les analyser pour mesurer l’efficacité de l’action publique ou pour leur compte personnel. Les data journalistes les utilisent pour nous éclairer, les chercheurs pour comprendre. Ainsi la transparence permet de lutter contre la corruption et les intox, tout comme elle est source de progrès.Ce changement de paradigme, l’accès aux données de l’état, est surtout une opportunité pour participer. Noter un dysfonctionnement permet de suggérer une amélioration, un manque peut être une opportunité économique, même un jeu de données incomplet est une occasion pour tisser des liens entre l’administration, les associations et les citoyens.À travers cet essai, l’auteur nous propose un voyage optimiste dans le monde des données. Chemin faisant, les liens entre ces données et la transparence ouvrent la voie vers une démocratie plus ouverte, plus interactive et donc plus juste.

Continue reading

Effective reductions of Mealy machines

Abstract

We revisit the problem of reducing incompletely specified Mealy machines with reactive synthesis in mind. We propose two techniques: the former is inspired by the tool MeMin and solves the minimization problem, the latter is a novel approach derived from simulation-based reductions but may not guarantee a minimized machine. However, we argue that it offers a good enough compromise between the size of the resulting Mealy machine and performance. The proposed methods are benchmarked against MeMin on a large collection of test cases made of well-known instances as well as new ones.

Continue reading

LTL under reductions with weaker conditions than stutter invariance

Abstract

Verification of properties expressed as omega-regular languages such as LTL can benefit hugely from stutter insensitivity, using a diverse set of reduction strategies. However properties that are not stutter invariant, for instance due to the use of the neXt operator of LTL or to some form of counting in the logic, are not covered by these techniques in general. We propose in this paper to study a weaker property than stutter insensitivity. In a stutter insensitive language both adding and removing stutter to a word does not change its acceptance, any stuttering can be abstracted away; by decomposing this equivalence relation into two implications we obtain weaker conditions. We define a shortening insensitive language where any word that stutters less than a word in the language must also belong to the language. A lengthening insensitive language has the dual property. A semi-decision procedure is then introduced to reliably prove shortening insensitive properties or deny lengthening insensitive properties while working with a reduction of a system. A reduction has the property that it can only shorten runs. Lipton’s transaction reductions or Petri net agglomerations are examples of eligible structural reduction strategies. An implementation and experimental evidence is provided showing most non- random properties sensitive to stutter are actually shortening or lengthening in- sensitive. Performance of experiments on a large (random) benchmark from the model-checking competition indicate that despite being a semi-decision proce- dure, the approach can still improve state of the art verification tools. 1 Introduction Model checking is an automatic verification technique for proving the correctness of systems that have finite state abstractions. Properties can be expressed using the popular Linear-time Temporal Logic (LTL). To verify LTL properties, the automata-theoretic approach [25] builds a product between a Buchi automaton representing the negation of the LTL formula and the reachable state graph of the system (seen as a set of infinite runs). This approach has been used successfully to verify both hardware and software components, but it suffers from the so called “state explosion problem”: as the number of state variables in the system increases, the size of the system state space grows exponentially.

Continue reading