×

A clausal resolution method for extended computation tree logic ECTL. (English) Zbl 1101.03017

Summary: A temporal clausal resolution method was originally developed for linear time temporal logic and further extended to the branching-time framework of Computation Tree Logic (CTL). In this paper, following our general idea to expand the applicability of this efficient method to more expressive formalisms useful in a variety of applications in computer science and AI requiring branching time logics, we define a clausal resolution technique for Extended Computation Tree Logic (ECTL). The branching-time temporal logic ECTL is strictly more expressive than CTL in allowing fairness operators. The key elements of the resolution method for ECTL, namely the clausal normal form, the concepts of step resolution and a temporal resolution, are introduced and justified with respect to this new framework. Although in developing these components we incorporate many of the techniques defined for CTL, we need novel mechanisms in order to capture fairness together with the limit closure property of the underlying tree models. We accompany our presentation of the relevant techniques by examples of the application of the temporal resolution method. Finally, we provide a correctness argument and consider future work discussing an extension of the method yet further, to the logic CTL\(^*\) asterisk operator, the most powerful logic of this class.

MSC:

03B35 Mechanization of proofs and logical operations
03B44 Temporal logic
03B70 Logic in computer science
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI

References:

[1] Bernholtz, O.; Vardi, M. Y.; Wolper, P., An automata-theoretic approach to branching-time model checking, (Computer Aided Verification, Proc. 6th Int. Workshop, Stanford, CA. Computer Aided Verification, Proc. 6th Int. Workshop, Stanford, CA, Lecture Notes in Computer Science, vol. 818 (1994), Springer: Springer Berlin), 142-155
[2] A. Bolotov, Clausal resolution for branching-time temporal logic, PhD thesis, Department of Computing and Mathematics, The Manchester Metropolitan University, 2000; A. Bolotov, Clausal resolution for branching-time temporal logic, PhD thesis, Department of Computing and Mathematics, The Manchester Metropolitan University, 2000 · Zbl 1054.68666
[3] Bolotov, A., Clausal resolution for extended computation tree logic ECTL, (Proceedings of the Time-2003/International Conference on Temporal Logic 2003, Cairns (2003), IEEE) · Zbl 1101.03017
[4] Bolotov, A.; Basukoski, A., A clausal resolution for branching-time logic \(ECTL^+\), (Proceedings of the Time-2004 (2004), IEEE), 140-147
[5] Bolotov, A.; Dixon, C., Resolution for branching time temporal logics: applying the temporal resolution rule, (Proceedings of the 7th International Conference on Temporal Representation Reasoning (TIME2000), Cape Breton, Nova Scotia, Canada (2000), IEEE Computer Society), 163-172
[6] Bolotov, A.; Fisher, M., A clausal resolution method for CTL branching time temporal logic, J. Experimental Theoret. Artificial Intelligence, 11, 77-93 (1999) · Zbl 1054.68666
[7] Bolotov, A.; Fisher, M.; Dixon, C., On the relationship between ‘w’-automata and temporal logic normal form, J. Logic Comput., 12, 561-581 (2002) · Zbl 1007.03014
[8] Bradfield, J.; Stirling, C., Modal logics and mu-calculi, (Bergstra, J.; Ponse, A.; Smolka, S., Handbook of Process Algebra (2001), Elsevier, North-Holland: Elsevier, North-Holland Amsterdam), 293-330 · Zbl 1002.03021
[9] Clarke, E. M.; Emerson, E. A., Design and synthesis of synchronisation skeletons using branching time temporal logic, (Logic of Programs, Proceedings of Workshop. Logic of Programs, Proceedings of Workshop, Lecture Notes in Computer Science, vol. 131 (1981), Springer: Springer Berlin), 52-71 · Zbl 0546.68014
[10] Emerson, E. A., Temporal and modal logic, (van Leeuwen, J., Handbook of Theoretical Computer Science, vol. B, Formal Models and Semantics (1990), Elsevier: Elsevier Amsterdam), 996-1072 · Zbl 0900.03030
[11] Emerson, E. A., Automated reasoning about reactive systems, (Logics for Concurrency: Structures Versus Automata, Proc. of International Workshop. Logics for Concurrency: Structures Versus Automata, Proc. of International Workshop, Lecture Notes in Computer Science, vol. 1043 (1996), Springer: Springer Berlin), 41-101 · Zbl 1543.68206
[12] Emerson, E. A.; Halpern, J. Y., “Sometimes” and “Not never” revisited: On branching versus linear time temporal logic, J. ACM, 33, 1, 151-178 (1986) · Zbl 0629.68020
[13] 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; 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 · Zbl 0593.03007
[14] M. Fisher, A resolution method for temporal logic, in: Proc. of the XII International Joint Conference on Artificial Intelligence (IJCAI), 1991, pp. 99-104; M. Fisher, A resolution method for temporal logic, in: Proc. of the XII International Joint Conference on Artificial Intelligence (IJCAI), 1991, pp. 99-104 · Zbl 0745.68091
[15] Wolper, P., On the relation of programs and computations to models of temporal logic, (Bolc, L.; Szałas, A., Time and Logic, a Computational Approach (1995), UCL Press Limited), 131-178, Chapter 3
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.