Co-ing Büchi Made Tight and Useful

We solve the longstanding open problems of the blowup involved in the translations (when possible) of a nondeterministic Buchi word automaton (NBW) to a nondeterministic co-Buchi word automaton (NCW) and to a deterministic co-Buchi word automaton (DCW). For the NBW to NCW translation, the currently known upper bound is 2^{O(n log n)} and the lower bound is 1.5n. We improve the upper bound to n2ⁿ and describe a matching lower bound of 2^Omega(n). For the NBW to DCW translation, the currently known upper bound is 2^{O(m log n)}. We improve it to 2^O(n), which is asymptotically tight. Both of our upper-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 LTL to deterministic Buchi word automata.