A Tableau for CTL

摘要

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