University of Cambridge > > Computer Laboratory Automated Reasoning Group Lunches > One-pass Tableaux for Computation Tree Logic

One-pass Tableaux for Computation Tree Logic

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Thomas Tuerk.

Room changed

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 (} without these extensive optimisations. Its one-pass nature also makes it amenable to parallel proof-search on multiple processors.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity