2013/07/17 by Mark Reynolds
Computer Science · #cs.LO
paper · pdf · doi:10.4204/eptcs.119.7
published as EPTCS 119, 2013, pp. 50-63 · In Proceedings GandALF 2013, arXiv:1307.4162
arxiv created 2013/07/17 · arxiv updated 2013/07/18
There have been several recent suggestions for tableau systems for deciding satisfiability in the practically important branching time temporal logic known as CTL*. In this paper we present a streamlined and more traditional tableau approach built upon the author's earlier theoretical work. Soundness and completeness results are proved. A prototype implementation demonstrates the significantly improved performance of the new approach on a range of test formulas. We also see that it compares favourably to state of the art, game and automata based decision procedures.