[Varies] Complementation of Buchi Automata
How can we complement Büchi automata? Analyze existing algorithms and design an implementation of such an algorithm in out automata library.
| Course type | Bachelor-Project, Bachelor Thesis, Master Laboratory or Master Team Project |
|---|---|
| Instructors | Matthias Heizmann |
| Credits | Depending on course type 6, 12 or 30 |
| Course Catalog |
Complementation of finite automata is easy: determinize and totalize the automaton first, switch accepting and non-accepting states afterwards. For Büchi automata this approach does not work. However in the last decades several algorithms for the complementation of Büchi automata have been proposed [1].
In this project we are going to analyze the Ramsey based complementation approach [2] and design an implementation in out automata library. Depending on the course type and your preferences we will continue with one or both of the following tasks.
- Design an algorithm for a difference operation of Büchi automata.
- Design an algorithm for a Ramsey based complementation of Nested Word Automata.