Co-ing Büchi Made Tight and Useful
Udi Boker, Orna Kupferman · 2009
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 2O(nlogn)and the lower bound is 1.5n. We improve the upper bound to n2nand describe a matching lower bound of 2Omega(n). For the NBW to DCW translation, the currently known upper bound is 2O(mlogn). We improve it to 2O(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.