A tableau-based decision procedure for CTL*

作者：Reynolds Mark^*

来源：Formal Aspects of Computing, 2011, 23(6): 739-779.

DOI：10.1007/s00165-011-0193-4

• CTL*
• Tableau
• Branching time
• Automated reasoning

We present a sound, complete and implementable tableau method for deciding satisfiability of 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 easily 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 medium-sized formulas and construction of small models for them. A straightforward subroutine is given for determining when looping allows successful branch termination, but much needed further development is left as future work. In particular, a more general repetition prevention mechanism is needed to speed up the task of tableau construction.

• 出版日期2011-11