Complementing deterministic Büchi automata in polynomial time (Q1116702)

The main result of the paper is a construction which to each deterministic edge recurring Büchi automaton A with n states yields a nondeterministic edge recurring Büchi automaton with 2n states accepting the complement of the language accepted by A. For nondeterministic A the construction yields in general a superclass of the complement. The basic idea of the construction is quite simple and transparent, however some local optimizations are included. The author also presents polynomial time algorithms for - deciding emptiness of the complement for deterministic Büchi automata, - deciding whether the main construction applied to a nondeterministic automaton yields exactly the complement. A state-splitting algorithm converting state recurring automaton into an equivalent edge recurring automaton is also given.