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.