Master 2014 2015
Stages de la spécialité SAR
Algorithms for automata over infinite words using a general acceptance condition

Site :Algorithms for automata over infinite words using a general acceptance condition
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


The formal method community uses several types of automata over infinite words (called "omega-automata") : Büchi automata, Streett automata, Rabin automata... These automata differ by their acceptance condition, i.e., the condition under which an infinite run of the automaton is accepted. For each of these different acceptance conditions there exist specialized algorithms, for instance to decide if an automaton is accepting, or to change an acceptance condition into another, or to determinize an automaton... We have recently defined file format for exchanging omega-automata between tools. This format can represent all the above types of automata thanks to a very general way to to represent the acceptance condition. In fact the acceptance condition specification is so general that it allows us to represent combination of existing conditions. The goal of this internship is to survey existing algorithms that differ from one acceptance condition to the other, and develop algorithms that will work with the generalized acceptance condition. The first algorithms we would like to have are :
- emptiness check (is the language of the automaton empty ?)
- conversion to Büchi acceptance. This internship targets students who would like to do some theory, and might be interested into continuing on a Ph.D thesis.


- HOAF : format for omega-automata with general acceptance.

- Spot : C++ library in which we would like to implement the developed algorithms at some point. (Currently the support is limited to some variant of Büchi acceptance, and some bits of Streett and Rabin).

- Christof Löding’s diploma thesis about conversion between different acceptance types.