Master 2013 2014
Stages de la spécialité SAR
Minimisation d’automates de Büchi et Rabin avec un SAT-solver


Site :LRDE
Lieu :Laboratoire de Recherche et Développement de l'Épita (LRDE)
Encadrant : - Alexandre Duret-Lutz (LRDE/EPITA) <adl@lrde.epita.fr> - Souheib Baarir (LIP6/UPMC) <souheib.baarir@lip6.fr>
Dates :flexibles
Rémunération :800€ bruts par mois
Mots-clés : Parcours SAR autre qu’ATIAM, recherche

Description

La bibliothèque Spot (http://spot.lip6.fr/) fournit de nombreux algorithmes pour traduire des formules LTL en automates de Büchi, ainsi que pour simplifier ces formules et ces automates. Une technique ajoutée récement (dans la version 1.2 de Spot) permet de minimiser les automates de Büchi deterministes à l’aide un SAT-solver (dans notre cas, glucose : http://www.labri.fr/perso/lsimon/gl...).

Pour minimiser un automate de Büchi deterministe à n états (un problème NP-complet), on encode son équivalence avec un automate déterministe à x états sous la forme d’un problème SAT, qu’on fait résoudre par un SAT-solver. Si une solution est trouvée, c’est qu’il exist un automate équivalent avec x états ou moins.

Actuellement, une première version de l’approche est implémentée en sauvegardant le problème encodé dans un fichier temporaire (dont la taille peut occuper plusieurs gigaoctets) avant de lancer le SAT solver sur ce fichier. Une fois le problème résolu pour passer de n à n-1, le fichier temporaire est effacé, puis un nouveau fichier est créé pour le problème consistant à passer de n-1 états à n-2 états.

L’objectif du stage est d’améliorer les performances de cette approche puis de la généraliser. Il s’agit dans un premier temps :
- d’implémentater des optimisations "bêtement techniques" (p.ex. se débarasser du fichier temporaire pour communiquer avec le SAT solver).
- de tirer partie des fonctionalités offertes par les SAT solvers modernes : par exemple le "SAT-solving incrémental" permet de réutiliser des connaissances accumulées lors de la résolution d’un problème pour accélérer le calcul du problème suivant. Dans notre cas cela reviendrait à demander au SAT-solver "puisque tu sais réduire cet automate à n-1 états, sais-tu le réduire à n-2 états ?" sans devoir encoder un nouveau problème.
- de proposer optimisations de l’encodage du problème de façon à tirer partie de la structure de l’automate que l’on cherche à minimiser, afin de simplifier l’encodage du problème donné au SAT-solver. (Nous avons plein de suggestions.)

Dans un second temps, il faudra généraliser cette approche aux automates de Rabin pour lesquels on sait toujours construire des automates déterministe (ce n’est pas le cas pour Büchi).

Ce stage s’adresse à des candidats qui
- sont à l’aise en C++ et en développement sous Unix (la maîtrise d’emacs et git sont des plus)
- se soucient d’écrire du code propre et utile (Spot est une bibliothèque open-source utilisée dans d’autres projets)
- aiment optimiser
- ont envie de se familiariser avec le monde extraordinaire des SAT-solvers et celui des automates de Büchi ou Rabin.

Bibliographie

Sur l’utilisation d’un SAT-solver pour minimiser un automate déterministe : http://www.react.uni-saarland.de/pu... et http://www.react.uni-saarland.de/pe... (La méthode mise en œuvre dans Spot est un peu plus évoluée, mais s’inspire de celle-ci.)

Sur l’utilisation de la minimisation avec SAT dans Spot : http://spot.lip6.fr/userdoc/satmin.html