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

Spot

Advisor

Alexandre Duret-Lutz

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

adl@lrde.epita.fr