A Tableau for Bundled CTL~*

摘要

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~*.