A tableau-based decision procedure for CTL* |
| |
Authors: | Mark Reynolds |
| |
Affiliation: | (1) Dept. Logic, University of L?dz, Kopcinskiego 16/18, 90-232 L?dz, Poland |
| |
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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|