A tableau for CTL

Abstract

We present a sound, complete and relatively straightforward tableau method for deciding valid formulas in the propositional version of computation tree logic CTL*. This is the first such tableau. CTL*is an exceptionally important temporal logic with applications from hardware design to agent reasoning but there is no easy automated reasoning approach to CTL*. The tableau here is a traditional tree-shaped or top-down style tableau and affords the possibility of reasonably quick decisions on the satisfiability of sufficiently short formulas and construction of models for them. Handling looping is subtle. © 2009 Springer-Verlag Berlin Heidelberg.