Jobs/M2 2015 ADL SAT-based Minimization

	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	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 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: have some experience in C++ programming and Unix development (experience with git and emacs 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.
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: implement purely technical optimizations (like direct communication with the SAT solver, bypassing any temporary files) take advantage of features 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 optimizations 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 (first as input, and then as output as well).
Benefit for the candidate
References	On the usage of a SAT-solver for minimization: https://www.lrde.epita.fr/~adl/dl/adl/baarir.15.lpar.pdf For the present usage of SAT-based minimization in Spots: https://spot.lrde.epita.fr/satmin.html
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	<adl at lrde . epita . fr> <adl at lrde . epita . fr>