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: | 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. |
Pages: | 10 |
Talk: | Jul 09 16:20 (Session 51D) |
Paper: |