## 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: |