Bibliographic Details
| Title: |
A tableau-based decision procedure for CTL*. |
| Authors: |
Reynolds, Mark1 mark@csse.uwa.edu.au |
| Source: |
Formal Aspects of Computing. Nov2011, Vol. 23 Issue 6, p739-779. 41p. |
| Subjects: |
Computer software termination, Computing platforms, Subroutines (Computer programs), Reasoning, Ring networks |
| Abstract: |
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. [ABSTRACT FROM AUTHOR] |
|
Copyright of Formal Aspects of Computing is the property of Association for Computing Machinery and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) |
| Database: |
Engineering Source |
