**Abstract:
**
We give a linear-time algorithm to translate any formula from computation
tree logic (CTL or CTL*) into an equivalent expression in a
variable-confined fragment of transitive-closure logic FO(TC).
Traditionally, CTL and CTL* have been used to express queries for model
checking and then translated into mu-calculus for symbolic evaluation.
Evaluation of mu-calculus formulas is, however, complete for time
polynomial in the (typically huge) number of states in the Kripke
structure. Thus, this is often not feasible, not parallelizable, and
incremental strategies are unlikely to exist. By contrast, evaluation of
any formula in FO(TC) requires only NSPACE[log n]. This means that the
space requirements are manageable, the entire computation is
parallelizable, and dynamic evaluation is possible.

Recent Publications of Neil Immerman