Abstract
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”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”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.
Continue reading
