Jobs/ENGI ADL 2015 Spot Traduction de formules de logique temporelle en automates
From LRDE
Traduction de formules de logique temporelle en automates | |
---|---|
Reference id |
ENGI ADL 2015 Spot Traduction de formules de logique temporelle en automates |
Dates |
5-6 months in 2015 |
Research field |
Automata Theory |
Related project | |
Advisor | |
General presentation of the field |
The Spot library (http://spot.lip6.fr/) contains many algorithms for translating LTL formulas into Büchi automata, and to simplify these formulas and automata. A recently added technique (in Spot version 1.2) allows us to minimize deterministic Büchi automata using a SAT-solver. To minimize a n-state deterministic Büchi automaton (an NP-complete problem) we encode its equivalence with a (n-1)-state deterministic Büchi automaton as a SAT problem, and let a SAT solver do the work of finding a solution. If such a solution is found, we try again, looking for a (n-2) state automaton, etc. |
Prerequisites |
Savoir programmer en C++. Avoir apprécié le cours de théorie des langage rationnels (niveau spé). |
Objectives |
La bibliothèque Spot fournit des algorithmes pour fabriquer un model checker, c'est-à-dire un outil qui sert à prouver que tous les comportements possible d'un système vérifient une propriété donnée. On y trouve entre autres des algorithmes pour traduire des formules de logique temporelle (qui expriment les propriétés) en automates (pour automatiser la preuve). L'une de ces logiques s'appelle PSL (Property Specification Language) et est déjà supportée, mais de façon sous optimale. L'objectif du stage est de réimplementer la traduction de PSL en automates proprement. Cela passe par l'introduction d'un nouveau type d'automate, similaire aux automates non-déterministes du cours de THLR, mais avec des transitions finales au lieu d'avoir des états finaux. Comme il existe déjà une traduction, et que Spot est déjà équippé avec tout ce qu'il faut pour comparer des traductions entre elles, il sera facile de rapidement débugger la nouvelle approche. |
Benefit for the candidate |
Rédevelopper une théorie des automates pour un nouveau type d'automates, découvrir les logiques temporelles et leurs applications. |
References | |
Place | LRDE: How to get to us |
Compensation |
500€ brut/mois |
Future work opportunities | |
Contact |