Title: co-ing Buchi made tight
 
Abstract:
The translation, when possible, of a nondeterministic Buchi word
automaton to a nondeterministic co-Buchi word automaton
is a longstanding open problem. The best known lower bound for
the state blow-up is linear, while the upper bound is 2^(n log n).
By pointing to some key observations on nondeterminism and
co-Buchi recognizable languages, we resolve the problem, showing
an asymptotically tight bound of 2^n.
 
In addition, we resolve a related open problem, of translating, when
possible, a nondeterministic Buchi word automaton to a deterministic
co-Buchi word automaton, also showing an asymptotically tight bound
of 2^n.
 
Both of our tight-bound constructions are based on a simple subset
construction, do not involve intermediate automata with richer
acceptance conditions, and can be implemented symbolically. We point
to numerous applications of the new constructions. In particular,
they imply a simple subset-construction based translation, when
possible, of linear-temporal-logic formulas to deterministic
Buchi word automata.

Joint work with Orna Kupferman.