Model checking and transitive-closure logic

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 μ-calculus for symbolic evaluation. Evaluation of μ-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 efficient 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 efficient dynamic evaluation is possible.