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 medium-sized formulas and construction of small models for them.
A quick subroutine is given for determining when loops are allowed back up in the tree 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.
There is a draft technical report placed online January 2009 (see above).
There is a short conference version appearing at FM2009.
The final journal version has been submitted to a journal in early 2010.
There is now an online (preliminary) implementation here.
@article{Rey:startab,
Author = {M. Reynolds},
Issue = {?},
Journal = {Journal of Formal Aspects of Computing},
Pages = {?--?},
Title = {A Tableau for {CTL*}: extended version},
Volume = ?,
Year = {submitted 2010}
}
@techreport{Reynolds:startablong,
author="M. Reynolds",
title="A Tableau for CTL*",
institution="The university of Western Australia",
url="http://www.csse.uwa.edu.au/~mark/research/Online/startab.html",
year=2009,
}