Back to Search
Start Over
Co-ing Büchi Made Tight and Useful
- 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