Transformations d’ω-automates pour la synthèse de systèmes réactifs
Florian Renkin · 2022
La synthèse vise à produire un système correct à partir de spécifications. Une approche pour résoudre ce problème consiste à traduire la spécification en un jeu de parité dont la stratégie gagnante encode le système. Dans cette thèse nous allons montrer deux méthodes permettant de produire des automates de parité. La première s'appuie sur l'amélioration et la combinaison de procédures nouvelles ou existantes. La seconde est un algorithme de Casares et al. apportant une garantie d'optimalité du résultat. Dans un deuxième temps, nous montrerons comment nous réduisons le système obtenu. Deux types de réductions seront abordées. La première permet d'obtenir un résultat optimal mais pas la seconde qui privilégie le temps de traitement. La troisième partie décrira des optimisations qui peuvent être utilisées pour certaines classes de spécifications.