Histoire d'un aller et retour : méthodes formelles et apprentissage de modèles pour les systèmes en temps réel

(english version below)

La soutenance de thèse de Léo Henry, équipe SUMO, se déroulera le 3 décembre 2021, à 15 heures, en salle Petri-Turing, à Inria Rennes.

Histoire d'un aller et retour : méthodes formelles et apprentissage de modèles pour les systèmes en temps réel

Cette thèse traite des méthodes formelles pour les automates temporisés, de leurs actions sur la réalité, et des informations que l'on peut apprendre grâce à ces observations.
Elle propose différentes contributions dans trois domaines distincts : la théorie des jeux et la génération de tests, vue comme un moyen de contrôler un système à l'aide de méthodes formelles; l'estimation d'état, qui déduit les configurations possibles d'un système à partir d'observations au moyen d'une construction formelle; l'apprentissage actif de modèles, qui propose de construire un modèle d'un système en lui demandant des observations, en les orientant selon les besoins de la tâche.
Aussi diverses qu'elles puissent paraître, ces contributions sont liées par le formalisme sous-jacent, les abstractions utilisées et les préoccupations qui caractérisent les interactions entre les modèles formels et la réalité. De plus, elles bénéficient les unes des autres dans la pratique, formant un cercle vertueux:
la capacité d'apprendre de la réalité permet de meilleurs modèles, qui à leur tour permettent un contrôle plus fin des systèmes, ce qui favorise les processus d'apprentissage.
Nous relions ces différentes contributions entre elles sur la base de ces motifs, et nous plaidons pour un rapprochement entre les méthodes et les communautés d'apprentissage de modèles et de méthodes formelles.

-----------

There and back again : formal methods and model learning for real-time systems

This thesis deals with formal methods for timed automata, their actions upon reality, and the informations that can be learned from it.
It proposes different contributions in three separate domains: game theory and formal test generation, seen as a way to control a system using formal methods; state estimation, that deduce the possible configurations of a system from observations by the mean of a formal construction; active model learning, that propose to construct a formal model of a system by requesting observations out of it, directing them as needed for the task.
As diverse as they may seem, these contributions are linked by the underlying formalism, abstractions and preoccupations that characterizes interactions between formal models and reality.
Furthermore, they benefit from one another in practice, forming a virtuous loop: the capacity to learn from reality allows for better models, that in turn permit a finer control of the real systems, which helps the learning processes.
We link these different contributions together based on these grounds, and advocate for a greater rapprochement between learning and formal methods and communities.