One-pass Tableaux for Computation Tree Logic (CTL)

Paper accepted to LPAR 07 :

We extend Schwendimann's single-pass decision procedure for propositional linear temporal logic (PLTL) to give a single-pass tableau decision procedure for computational tree logic (CTL). The extension is non-trivial because the soundness proof requires a careful analysis of the interactions between the branching inherent in CTL-models, which is missing in PLTL-models, with 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 and our procedure requires 2EXPTIME. But a similar phenomenon occurs in expressive description logics where the highly optimised and implemented 2EXPTIME procedures for EXPTIME-complete logics remain practical even for large formulae. Our procedure has been implemented in the Tableau Work Bench ( without these extensive optimisations. Its one-pass nature also makes it amenable to parallel proof-search on multiple processors.