CTL+ is exponentially more succinct than CTL

Abstract

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(Fp0 ∧…∧ Fpn-1) is of length at least(nn/2), which is Ω(2n/ √ 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 2n logn. 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. © Springer-Verlag Berlin Heidelberg 1999.