Jobs/M2 ADL 2015 General Acceptance Condition
From LRDE
Algorithms for automata over infinite words using a general acceptance condition  

Reference id 
M2 ADL 2015 General Acceptance Condition 
Dates 
56 months in 2015 
Research field 
Automata Theory 
Related project  
Advisor  
General presentation of the field 
The formal method community uses several types of automata over infinite words (called "omegaautomata"): 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 omegaautomata 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. 
Prerequisites 
Automata Theory 
Objectives 
The goal of this internship is to survey, implement, and extend existing algorithms that simplify omegaautomata (with different acceptance conditions), and convert between various acceptance conditions. 
Benefit for the candidate 
This internship targets students who would like to do some theory, and might be interested into continuing on a Ph.D thesis. 
References 

Place  LRDE: How to get to us 
Compensation 
1000 € gross/month 
Future work opportunities 
PhD 
Contact 