On the relative succinctness of nondeterministic Büchi and co-Büchi word automata Academic Article uri icon


  • The practical importance of automata on infinite objects has motivated a re-examination of the complexity of automata-theoretic constructions. One such construction is the translation, when possible, of nondeterministic Büchi word automata (NBW) to nondeterministic co- Büchi word automata (NCW). Among other applications, it is used in the translation (when possible) of LTL to the alternation-free μ-calculus. The best known upper bound for the translation of NBW to NCW is exponential (given an NBW with n states, the best translation yields an equivalent NCW with 2 O (n log n) states). On the other hand, the best known lower bound is trivial (no NBW with n states whose equivalent NCW requires even n+ 1 states is known). In fact, only recently was it shown that there is an NBW whose equivalent NCW requires a different structure. In this paper we improve the lower bound by showing that …

publication date

  • November 22, 2008