Université de Rennes 1 There and back again : formal methods and model learning for real-time systems : acting upon reality and learning from its reactions Histoire d’un aller et retour : méthodes formelles et apprentissage de modèles pour les systèmes en temps réel Automates temporisésThéorie des jeuxApprentissage actifMéthodes formellesEstimation d’état Timed automataGame TheoryActive learningFormal methodsState estimation Automates temporisés Théorie des jeux Apprentissage automatique Méthodes formelles (informatique) 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. 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. Electronic Thesis or DissertationText en application/pdf1 : 2061 Kohttps://ged.univ-rennes1.fr/nuxeo/site/esupversions/a7252355-1ed1-41c0-b782-e16db1f393c7 Henry Léo 1995-11-28 FR 260094021 leo.henry.lin@gmail.com 2021REN1S071 http://www.theses.fr/2021REN1S071 2021-12-03 Informatique Universite de Rennes 1thesis.degree.grantor_1 02778715X Doctorat non ouiMarkeyNicolasintervenant_1073426482JéronThierryintervenant_2095612777LimeDidierintervenant_308563025XBassetNicolasintervenant_6191360848LonguetDelphineintervenant_712073270XTripakisStavrosintervenant_8AndréÉtienneintervenant_4151927081VaandragerFrits W.intervenant_5 MATHSTICecoleDoctorale_1 204770424 IRISA partenaireRecherche_1 026386909 ddc:004 MarkeyNicolasJéronThierryLimeDidierAndréÉtienneVaandragerFrits W.BassetNicolasLonguetDelphineTripakisStavrosUniversite de Rennes 1Sciences et technologie, medecine, pharmacie, odontologie, droit, economie, gestion, philosophieMATHSTICÉcole doctorale Mathématiques et sciences et technologies de l'information et de la communication (Rennes) IRISA ASCII PDF 2110046