One-pass Tableaux for Computation Tree Logic (CTL)

Paper accepted to LPAR 07 : http://www.lpar.net/2007/

Abstract:
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 (twb.rsise.anu.edu.au) without these extensive optimisations. Its one-pass nature also makes it amenable to parallel proof-search on multiple processors.

http://twb.rsise.anu.edu.au/one_pass_tableaux_computation_tree_logic