A clausal resolution method for extended computation tree logic ECTL

Journal of Applied Logic - Tập 4 - Trang 141-167 - 2006
Alexander Bolotov1, Artie Basukoski1
1Harrow School of Computer Science, University of Westminster, HA1 3TP, UK

Tài liệu tham khảo

Bernholtz, 1994, An automata-theoretic approach to branching-time model checking, vol. 818, 142 A. Bolotov, Clausal resolution for branching-time temporal logic, PhD thesis, Department of Computing and Mathematics, The Manchester Metropolitan University, 2000 Bolotov, 2003, Clausal resolution for extended computation tree logic ECTL Bolotov, 2004, A clausal resolution for branching-time logic ECTL+, 140 Bolotov, 2000, Resolution for branching time temporal logics: applying the temporal resolution rule, 163 Bolotov, 1999, A clausal resolution method for CTL branching time temporal logic, J. Experimental Theoret. Artificial Intelligence, 11, 77, 10.1080/095281399146625 Bolotov, 2002, On the relationship between ‘w’-automata and temporal logic normal form, J. Logic Comput., 12, 561, 10.1093/logcom/12.4.561 Bradfield, 2001, Modal logics and mu-calculi, 293 Clarke, 1981, Design and synthesis of synchronisation skeletons using branching time temporal logic, vol. 131, 52 Emerson, 1990, Temporal and modal logic, 996 Emerson, 1996, Automated reasoning about reactive systems, vol. 1043, 41 Emerson, 1986, “Sometimes” and “Not never” revisited: On branching versus linear time temporal logic, J. ACM, 33, 151, 10.1145/4904.4999 E.A. Emerson, A.P. Sistla, Deciding full branching time logic, in: Proceedings of the Sixteenth Annual ACM Symposium on Theory of Computing (STOC 1984), 1984, pp. 14–24 M. Fisher, A resolution method for temporal logic, in: Proc. of the XII International Joint Conference on Artificial Intelligence (IJCAI), 1991, pp. 99–104 Wolper, 1995, On the relation of programs and computations to models of temporal logic, 131