[Lrde Annonce] Soutenance de thèse de Florian Renkin

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