**Abstract:**
We introduce a new Ehrenfeucht-Fraisse game for proving lower
bounds on the size of first-order formulas. Up until now such games have
only been used to prove bounds on the operator depth of formulas, not their
size. We use this game to prove that the CTL^{+} formula,

which says
that there is a path along which predicates p_{1} through p_{n} occur in some
order, requires size n! to express in CTL. Our lower bound is optimal. It
follows that the succinctness of CTL^{+} with respect to CTL is exactly
Theta(n). Wilke had shown that the succinctness was at least exponential
[Wi99].

We also use our games to prove an optimal Omega(n) lower bound on the
number of boolean variables needed for a weak reachability logic (*RL ^{w}*) to
polynomially embed the language LTL. The number of booleans needed for
full reachability logic

Recent Publications of Neil Immerman