It is proved that CTL
+ is exponentially more succinct than CTL. More p recisely, it is shown that every CTL formula (and every modal μ-calculus
formula) equivalent to the CTL
+ formula E(F
p
0 ∧ · · · ∧ Fp
n—1) is of length at least (
⌈n/2⌉
n
), which is
$
\Omega (2^n /\sqrt n )$
\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
μ-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 (μ-calculus) formula there exists an equivalent alternating
tree automaton of linear size. The core of this proof is an involved cut-and-paste argument for alternating tree automata.