Abstract

We give the first single-pass (“on the fly”) tableau decision procedure for computational tree logic (CTL). Our method extends Schwendimann’s single-pass decision procedure for propositional linear temporal logic (PLTL) but the extension is non-trivial because of the interactions between the branching inherent in CTL -models, which is missing in PLTL -models, and the “or” branching inherent in tableau search. Our method extends to many other fix-point logics like propositional dynamic logic (PDL) and the logic of common knowledge (LCK).

The decision problem for CTL is known to be EXPTIME -complete, but our procedure requires 2EXPTIME in the worst case. A similar phenomenon occurs in extremely efficient practical single-pass tableau algorithms for very expressive description logics with EXPTIME -complete decision problems because the 2EXPTIME worst-case behaviour rarely arises. Our method is amenable to the numerous optimisation methods invented for these description logics and has been implemented in the Tableau Work Bench (twb.rsise.anu.edu.au} without these extensive optimisations. Its one-pass nature also makes it amenable to parallel proof-search on multiple processors.