Towards a CTL* Tableau

Abstract

We present a sound, complete and relatively straightforward
tableau method for deciding
valid formulas in the propositional version of
the bundled (or suffix and fusion closed) computation tree logic BCTL*.
This proves that BCTL* is decidable.
It is also moderately useful to have
a tableau available for
a reasonably expressive branching time temporal logic.
However,
the main interest in this
should be that it leads us closer to being able
to devise a tableau-based technique
for theorem-proving in the
important full computational tree logic
CTL*.

Full Paper

Postscript version with full proof appendices September 2005

Status

Accepted to appear in proceedings of FSTTCS 2005.

Bibtex

@inproceedings{Reynolds:ctltab,
       author="M. Reynolds",
       title="Towards a CTL* Tableau",
    editors="R. Ramanujam and S. Sen",
booktitle="Foundations of Software Technology and Theoretical Computer Science (FSTTCS' 05)",
        publisher="Springer LNCS",
       year=2005,
       pages="? -- ?"
}