Master 2014 2015
Stages de la spécialité SAR
Minimization of Büchi automata using SAT-solving


Site :Minimization of Büchi automata using SAT-solving
Lieu :Laboratoire de Recherche & Développement de l'EPITA (LRDE) 14 -16 rue Voltaire 94276 Le Kremlin-Bicêtre Cedex
Encadrant : Alexandre Duret-Lutz
Dates :01/03/2015 au 31/08/2015
Rémunération :1000 Euros brut/mois
Mots-clés : Master SAR, autre qu’ATIAM

Description

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. This internship targets students who :
- have some experience in C++ programming and Unix development (experience with git would be a welcome bonus)
- like to write clean and useful code (Spot is an open-source library used by other projects)
- like to optimize
- would like do get familiar with the amazing world of SAT-solvers and Büchi automata. Presently, our first implementation saves the SAT problem as a huge file before calling the SAT-solver, and it does this for each iteration. The goal of this internship is to improve this situation in multiple ways :
- implement purely technical optimizations (like direct communication with the SAT solver, bypassing any temporary files)
- take advantage of feature offered by modern SAT solvers (for instance an "incremental SAT-solver" can be given new constraints after it has found a solution, without needing to restart from scratch)
- implement optimization to the encoding of the SAT-problem, based on structural properties of the automaton (we have some ideas) In a second, step, we would like to generalize the existing technique to non-deterministic automata, or to different types of acceptance conditions (i.e., not Büchi).

Bibliographie

- On the usage of a SAT-solver for minimization : https://www.lrde.epita.fr/ adl/dl/a...

- For the present usage of SAT-based minimization in Spot : http://spot.lip6.fr/userdoc/satmin.html