A Tableau for Bundled CTL
Mark A Reynolds · Journal of Logic and Computation · 2006
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*.