Jobs/M2 2015 ADL SAT-based Minimization
From LRDE
Minimization of Büchi automata using SAT-solving | |
---|---|
Reference id |
M2 2015 ADL SAT-based Minimization |
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 allows us to minimize deterministic Büchi automata using a SAT-solver; the implementation is actually not restricted to Büchi and can work with deterministic omega-automata with any acceptance conditions. To minimize a n-state deterministic omega-automaton (an NP-complete problem) we encode its equivalence with a (n-1)-state deterministic omega-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 |
This internship targets students who:
|
Objectives |
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:
In a second step, we would like to generalize the existing technique to non-deterministic automata (first as input, and then as output as well). |
Benefit for the candidate | |
References |
|
Place | LRDE: How to get to us |
Compensation |
1000 € gross/month |
Future work opportunities |
This internship can easily be prolonged as a PhD thesis. |
Contact |