The Blow-Up in Translating LTL to Deterministic Automata
========================================================

The translation of LTL formulas to nondeterministic automata involves
an exponential blow-up, and so does the translation of
nondeterministic automata to deterministic ones. This yields a
$2^{2^{O(n)}}$ upper bound for the translation of LTL to deterministic
automata. A lower bound for the translation was studied in
[KV05], which describes a $2^{2^{\Omega(\sqrt{n})}}$ lower
bound, leaving the problem of the exact blow-up open. In this paper we
solve this problem and tighten the lower bound to $2^{2^{\Omega(n)}}$.