PhD Defense Florian Renkin

From LRDE

Revision as of 12:47, 28 October 2022 by Alexandre Duret-Lutz (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)


Logo of Sorbonne University.png EDITE Logo.png Epita-logo-2.png Lrde.png


SOUTENANCE de THÈSE
Florian RENKIN
Vendredi 7 octobre 2022
à 9h30
EPITA, 14-16 Rue Voltaire, 94270 Le Kremlin-Bicêtre
Amphi 401
Plan d’accès :



Transformations d’ω-automates pour la synthèse de contrôleurs réactifs


Résumé :

Le travail de cette thèse s'inscrit dans le cadre de la création de manière automatique de systèmes corrects à partir de spécifications, ce que l'on appelle “synthèse”. Ce besoin de création automatique vient d'une part de la complexité de plus en plus importante des systèmes que l'on crée mais aussi de la difficulté de vérifier si un système est correct. Pour que la synthèse soit utilisable en pratique, y compris dans l'industrie, il faut être capable de produire des solutions pour des problèmes plus ou moins complexes en un temps raisonnable. De plus, on peut chercher à optimiser les systèmes produits afin qu'ils soient les plus simples possibles. Pour décrire les contraintes que le système doit respecter, nous utiliserons des formules de logique linéaire temporelle (LTL) qui ajoutent aux opérateurs Booléens traditionnels une notion de temps discret afin d'exprimer des contraintes telles que “il existera un instant où la variable sera vraie”. Dans notre cas, il s'agira de produire un contrôleur réactif, c'est-à-dire associant à une suite d'assignations de variables Booléennes d'entrées une suite d'assignations de variables Booléennes de sorties.

L'approche de la synthèse LTL que nous allons décrire consiste à :

Traduire la spécification LTL en un jeu de parité où un joueur contrôle l'environnement alors que le second représente les actions que peut faire le contrôleur. Rechercher dans ce jeu s'il existe une stratégie gagnante pour le second joueur. Cette stratégie indique les actions que doit faire le contrôleur pour respecter les spécifications et il reste alors à l'encoder sous la forme voulue (circuit, programme, …). Une partie de la première étape est une procédure dite de paritisation consistant à obtenir à partir d'un automate quelconque un automate de parité. Une contribution majeure de cette thèse consiste en l'amélioration de cette procédure. Dans cette optique, nous proposons et comparons divers algorithmes de paritisation. La première méthode est une combinaison d'algorithmes existants auxquels ont été associées des heuristiques mais aussi de nouveaux algorithmes. La seconde est l'adaptation d'une méthode introduite en 2021 par Casares et al. assurant une forme d'optimalité sur la taille de l'automate de parité obtenu. Dans les deux cas, ces algorithmes ont à la fois pour objectif de réduire le temps nécessaire pour une telle transformation mais aussi de limiter la taille de l'automate créé.

Une autre contribution consiste à proposer des techniques de simplification du contrôleur. En particulier, nous tirerons parti des libertés offertes par la spécification. Par exemple, si l'on souhaite un système allumant une ampoule lorsqu'une présence est détectée, alors ce qu'il faut faire lorsque personne n'est détecté n'a pas d'importance. Pour obtenir un système simple, on peut décider de toujours allumer l'ampoule et le système n'a alors plus besoin d'un capteur. Deux types de simplifications seront décrites. La première est inspirée d'un outil existant (MeMin) et utilise un SAT-solver pour obtenir une solution minimale. La complexité de la recherche d'optimalité (NP-complet) nous incite également à nous tourner vers une seconde méthode basée sur les BDD visant à fournir un système réduit plus rapidement mais sans garantie d'optimalité.

Ces deux contributions majeures ont été intégrées à l'outil ltlsynt distribué avec la bibliothèque Spot et ont été accompagnées de plusieurs améliorations que nous évaluons : une décomposition du problème permettant de créer des contrôleurs pour des sous-parties de la spécification mais aussi une méthode permettant de s'affranchir de la construction d'un jeu pour une certaine classe de formules. Ces travaux ont fait l'objet de publications dans les conférences ATVA'20 (première méthode de paritisation), TACAS'22 (seconde méthode de paritisation), FORTE'22 (simplification de contrôleur), CAV'22 (présentation des évolutions de Spot) ainsi que d'une présentation de ltlsynt lors de la conférence SYNT'21.

L'outil ltlsynt a par ailleurs participé aux éditions 2020, 2021 et 2022 de la SYNTCOMP.


Mots-clés : synthèse réactive, LTL, ω-automates, machines de Mealy


Manuscrit et présentation


Composition du Jury :

Rapporteurs :

  • Olivier Carton, Pr., Université Paris Cité, IRIF
  • Nicolas Markey, Pr., Université de Rennes, IRISA


Examinateurs :

  • Hanna Klaudel, Pr., Université d'Évry, IBISC
  • Laure Petrucci, Pr., Université Sorbonne Paris Nord, LIPN
  • Nathalie Sznajder, MdC, Sorbonne Université, LIP6


Encadrants :

  • Alexandre Duret-Lutz, Pr., EPITA, LRE
  • Adrien Pommellet, MdC, EPITA, LRE