Bonjour,

J'ai le plaisir de vous inviter à la soutenance (en français) de ma thèse intitulée : "Transformations d’ω-automates pour la synthèse de contrôleurs réactifs".
Vous êtes également cordialement invité au pot qui suivra.

Version web : https://www.lrde.epita.fr/~frenkin/thesis.php

Date
Vendredi 7 octobre, 9h30

Lieu
Amphi 401, 14-16 rue Voltaire, Le Kremlin-Bicêtre 94270

Jury
Rapporteurs

• Olivier Carton, Université Paris Cité
• Nicolas Markey, Université de Rennes

Examinateurs

• Hanna Klaudel, Université d'Évry
• Laure Petrucci, Université Sorbonne Paris Nord
• Nathalie Sznajder : Sorbonne Université

Encadrants

• Alexandre Duret-Lutz, EPITA
• Adrien Pommellet, EPITA

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 à : (1) 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. (2) Rechercher dans ce jeu s’il existe une stratégie gagnante pour le second joueur.
(3) 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’19 (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.

A bientôt,
Florian Renkin