You are here: Home Student Projects and … Finished [Varies] Complementation of Buchi …

[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.

 

Literature

[1] Ming-Hsien Tsai, Seth Fogarty, Moshe Y. Vardi, Yih-Kuen Tsay: State of Büchi Complementation. CIAA 2010:261-271

[2] A. Prasad Sistla, Moshe Y. Vardi, Pierre Wolper: The Complementation Problem for Büchi Automata with Appplications to Temporal Logic. Theor. Comput. Sci. (TCS) 49:217-237 (1987)