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]
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.