Skip navigation
Skip navigation

One-pass tableaux for computation tree logic

Abate, Pietro; Gore, Rajeev; Widmann, Florian


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)...[Show more]

CollectionsANU Research Publications
Date published: 2007
Type: Conference paper
Source: Proceedings of 14th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2007)


File Description SizeFormat Image
01_Abate_One-pass_tableaux_for_2007.pdf156.68 kBAdobe PDF    Request a copy
02_Abate_One-pass_tableaux_for_2007.pdf147.86 kBAdobe PDF    Request a copy
03_Abate_One-pass_tableaux_for_2007.pdf26.16 kBAdobe PDF    Request a copy
04_Abate_One-pass_tableaux_for_2007.pdf120.14 kBAdobe PDF    Request a copy
05_Abate_One-pass_tableaux_for_2007.pdf67.4 kBAdobe PDF    Request a copy
06_Abate_One-pass_tableaux_for_2007.pdf376.23 kBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator