CTL+ is exponentially more succinct than CTL
Thomas Wilke
It is proved that CTL+ is exponentially more succinct than
CTL. More precisely, it is shown that every CTL formula
(and every modal mu-calculus formula) equivalent to the CTL+
formula E(F p0 and F p1 and ... and F p(n-1)) is of length at
least n choose n/2, which is Omega(2^n/sqrt(n)). This matches
almost the upper bound provided by Emerson and Halpern, which
says that for every CTL+ formula of length n there exists an
equivalent CTL formula of length at most 2^{n log n}.
It follows that the exponential blow-up as incurred in known
conversions of nondeterministic Büchi word automata into
alternation-free $\mu$-calculus formulas is unavoidable. This
answers a question posed by Kupferman and Vardi.
The proof of the above lower bound exploits the fact that for
every CTL (mu-calculus) formula there exists an equivalent
alternating tree automaton of linear size. The core of the
proof is an involved cut-and-paste argument for alternating
tree automata.