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