Ecole Doctorale
Mathématiques et Informatique de Marseille
Spécialité
Informatique
Etablissement
Aix-Marseille Université
Mots Clés
Automates temporisés,Synthèse,Robustesse,Jeux pondéré,
Keywords
Timed automata,Synthesis,Robustness,Weighted games,
Titre de thèse
Synthèse symbolique de contrôleurs pour systèmes temporisés: robustesse et optimalité
Symbolic controller synthesis for timed systems: robustness and optimality
Date
Mardi 3 Décembre 2019 à 14:00
Adresse
Aix Marseille Université,
Site St Charles,
3 place Victor Hugo,
13003 Marseille Amphithéâtre Sciences Naturelles
Jury
Directeur de these |
M. Pierre-Alain REYNIER |
Aix Marseille Université |
CoDirecteur de these |
M. Benjamin MONMEGE |
Aix Marseille Université |
Examinateur |
Mme Patricia BOUYER-DECITRE |
ENS Paris-Saclay |
Examinateur |
Mme Nathalie BERTRAND |
INRIA Rennes Bretagne-Atlantique |
Examinateur |
Mme Laure PETRUCCI |
Université Paris 13 |
Rapporteur |
M. Igor WALUKIEWICZ |
Université de Bordeaux |
Rapporteur |
M. Joël OUAKNINE |
Max Planck Institute for Software Systems |
Résumé de la thèse
Le domaine de la synthèse réactive a pour objectif d'obtenir
un système correct par construction à partir d'une spécification logique.
Une approche classique consiste à se ramener à un jeu à somme nulle,
où deux joueurs interagissent tour-à-tour dans
un système de transitions, et demande si le joueur "contrôleur" peut garantir
que son objectif sera rempli, et ce indépendamment des décisions du joueur "environnement".
Nous étudions des spécifications temps-réel, modélisées par un automate temporisé
équipé d'un objectif d'accessibilité ou de Büchi, et présentons
des méthodes symboliques pour synthétiser des stratégies du contrôleur.
Nos contributions concernent deux problématiques distinctes :
on peut souhaiter que le contrôleur obtienne une stratégie robuste aux perturbations,
ou bien le faire jouer de manière optimale, dans un contexte de jeux pondérés.
Thesis resume
The field of reactive synthesis studies ways to obtain,
starting from a specification, a system that is correct
by construction.
A classical approach models this setting as a
zero-sum game played by two players on a transition system,
and asks whether player controller can
ensure an objective against any competing player environment.
We focus on real-time specifications,
modelled as timed automata with reachability or Büchi acceptance conditions,
and present symbolic ways to synthesise strategies for the controller.
We consider two problems, either restricting controller to robust strategies
or aiming for optimal strategies in a weighted game setting.