Büchi Complementation Made Tight

Abstract : The precise complexity of complementing \buchi\ automata is an intriguing and long standing problem. While optimal complementation techniques for finite automata are simple -- it suffices to determinize them using a simple subset construction and to dualize the acceptance condition of the resulting automaton -- \buchi\ complementation is more involved. Indeed, the construction of an EXPTIME complementation procedure took a quarter of a century from the introduction of \buchi\ automata in the early $60$s, and stepwise narrowing the gap between the upper and lower bound to a simple exponent (of $(6e)^n$ for \buchi\ automata with $n$ states) took four decades. % While the distance between the known upper ($O\big((0.96\,n)^n\big)$) and lower ($\Omega\big((0.76\,n)^n\big)$) bound on the required number of states has meanwhile been significantly reduced, an exponential factor remains between them. Also, the upper bound on the size of the complement automaton is not linear in the bound of its state space. These gaps are unsatisfactory from a theoretical point of view, but also because \buchi\ complementation is a useful tool in formal verification, in particular for the language containment problem. % This paper proposes a \buchi\ complementation algorithm whose complexity meets, modulo a quadratic ($O(n^2)$) factor, the known lower bound for \buchi\ complementation. It thus improves over previous constructions by an exponential factor and concludes the quest for optimal \buchi\ complementation algorithms.
Type de document :
Communication dans un congrès
Susanne Albers and Jean-Yves Marion. 26th International Symposium on Theoretical Aspects of Computer Science - STACS 2009, Feb 2009, Freiburg, Germany. IBFI Schloss Dagstuhl, pp.661-672, 2009, Proceedings of the 26th Annual Symposium on the Theoretical Aspects of Computer Science
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00360108
Contributeur : Publications Loria <>
Soumis le : mardi 10 février 2009 - 12:00:27
Dernière modification le : lundi 15 janvier 2018 - 11:47:14
Document(s) archivé(s) le : mardi 8 juin 2010 - 22:10:28

Fichiers

Schewe_new.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00360108, version 1
  • ARXIV : 0902.2152

Collections

Citation

Sven Schewe. Büchi Complementation Made Tight. Susanne Albers and Jean-Yves Marion. 26th International Symposium on Theoretical Aspects of Computer Science - STACS 2009, Feb 2009, Freiburg, Germany. IBFI Schloss Dagstuhl, pp.661-672, 2009, Proceedings of the 26th Annual Symposium on the Theoretical Aspects of Computer Science. 〈inria-00360108〉

Partager

Métriques

Consultations de la notice

101

Téléchargements de fichiers

198