Back to Search Start Over

Co-ing Büchi Made Tight and Useful

Authors :
Udi Boker
Orna Kupferman
Source :
LICS
Publication Year :
2009
Publisher :
IEEE, 2009.

Abstract

We solve the longstanding open problems of the blow-up involved in the translations (when possible) of a nondeterministic B\"uchi word automaton (NBW) to a nondeterministic co-B\"uchi word automaton (NCW)and to a deterministic co-B\"uchi 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^n$ and describe a matching lower bound of$2^{\Omega(n)}$. For the NBW to DCW translation, the currently known upper bound is $2^{O(n \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 B\"uchi word automata.

Details

Database :
OpenAIRE
Journal :
2009 24th Annual IEEE Symposium on Logic In Computer Science
Accession number :
edsair.doi...........5803e20ce9d6a2c5a0b70b84944cd161