Complementation of Büchi automata: A survey and implementation

Sammanfattning: This thesis is a survey of the field of languages over infinite sequences. There is active research going on in this field, during the last year several new results where published. We investigate the language containment problem for infinite sequences, with focus on complementation of Büchi automata. Our main focus is on the approach with alternating automata by Kupferman&Vardi. The language containment problem has been proved to be in EXPSPACE. We identify some cases when we can avoid the exponential blow-up by taking advantage of properties of the input automaton. Some of the algorithms we explain are also implemented in a Sicstus Prolog library.