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{sup}*. This proves that BCTL{sup}* 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{sup}*.
展开▼
