Mark Reynolds

Tableau for CTL*

We present a sound, complete and relatively straightforward tableau method for deciding valid formulas in the propositional version of full computation tree logic CTL*.