A Simple and Optimal Complementation Algorithm for Büchi Automata

Authors: Joel Allred and Ulrich Ultes-Nitsche

Paper Information

Title:A Simple and Optimal Complementation Algorithm for Büchi Automata
Authors:Joel Allred and Ulrich Ultes-Nitsche
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:Büchi Automaton, Complementation, Optimal Upper Bound, Benchmarking

ABSTRACT. Complementation of Büchi automata is well known for being complex, as Büchi automata in general are nondeterministic. In the worst case, a state-space growth of $O((0.76n)^n)$ cannot be avoided. Experimental results suggest that complementation algorithms perform better on average when they are structurally simple.

In this paper, we present a simple algorithm for complementing Büchi automata, operating directly on subsets of states, structured into state-set tuples (similar to slices), and producing a deterministic automaton. The second step in the construction is then a complementation procedure that resembles the straightforward complementation algorithm for deterministic Büchi automata, the latter algorithm actually being a special case of our construction. Finally, we prove our construction to be optimal, i.e.\ having an upper bound in $O((0.76n)^n)$, and furthermore calculate the $0.76$ factor in a novel exact way.

Talk:Jul 09 16:20 (Session 51D)