Difference between revisions of "Jobs/M2 ADL 2015 General Acceptance Condition"
From LRDE
| (3 intermediate revisions by 3 users not shown) | |||
| Line 22: | Line 22: | ||
conditions. |
conditions. |
||
|Prerequisites=Automata Theory |
|Prerequisites=Automata Theory |
||
| − | |Objectives=The goal of this internship is to survey |
+ | |Objectives=The goal of this internship is to survey, implement, |
| + | and extend existing algorithms that simplify omega-automata (with |
||
| − | differ from one acceptance condition to the other, and develop |
||
| + | different acceptance conditions), and convert between various |
||
| − | algorithms that will work with the generalized acceptance condition. |
||
| + | acceptance conditions. |
||
| − | The first algorithms we would like to have are: |
||
| − | * emptiness check (is the language of the automaton empty?) |
||
| − | * conversion to Büchi acceptance |
||
|Benefit for the candidate=This internship targets students who would like to do some theory, |
|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. |
and might be interested into continuing on a Ph.D thesis. |
||
|References=* HOAF: format for omega-automata with general acceptance. http://adl.github.io/hoaf/ |
|References=* HOAF: format for omega-automata with general acceptance. http://adl.github.io/hoaf/ |
||
| − | * Spot: C++ library in which we would like to implement the developed algorithms |
+ | * Spot: C++ library in which we would like to implement the developed algorithms. https://spot.lrde.epita.fr/ |
* Christof Löding's diploma thesis about conversion between different acceptance types. http://www.automata.rwth-aachen.de/~loeding/diploma_loeding.pdf |
* Christof Löding's diploma thesis about conversion between different acceptance types. http://www.automata.rwth-aachen.de/~loeding/diploma_loeding.pdf |
||
|Contact=<adl at lrde . epita . fr> |
|Contact=<adl at lrde . epita . fr> |
||
|Compensation=1000 € gross/month |
|Compensation=1000 € gross/month |
||
| + | |Future work opportunities=PhD |
||
|Type=Master Internship |
|Type=Master Internship |
||
|Language=en |
|Language=en |
||
| + | |Published=No |
||
}} |
}} |
||
Latest revision as of 17:27, 30 November 2016
| Algorithms for automata over infinite words using a general acceptance condition | |
|---|---|
| Reference id |
M2 ADL 2015 General Acceptance Condition |
| Dates |
5-6 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 "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. |
| Prerequisites |
Automata Theory |
| Objectives |
The goal of this internship is to survey, implement, and extend existing algorithms that simplify omega-automata (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 |