PhD Thesis: Clausal Resolution for Branching-time Logics

Supervisor - Professor Michael Fisher.
Oral examination - June, 1st, 2000, passed without corrections.

Examiners:

Dov Gabbay (Augustus De Morgan Professor of Logic at King's College)

Tito Toro (Professor at the Manchester Metropolitan University)

Renate Shmidt (Lecturer at the University of Manchester)

Abstract

Getting my thesis

Related publications

Abstract

Temporal logic is considered as an essential tool in the areas of Artificial Intelligence and Computer Science when structures to be described invoke temporal aspects. If a temporal model is to represent the behavior of a complex dynamic system, for example, a complex multi-process system, the ability to refer to a range of possible execution paths is important. Here, the underlying model of time is a choice of possibilities branching into the future. Varieties of branching-time temporal logics are characterised by specific syntactic restrictions, which, in turn, lead to different levels of expressiveness. Within these constraints computation tree logics CTL and CTL*, often regarded, respectively, as pure and full branching-time logics, have shown to play a significant role in potential applications, most notably in the specification and verification of multi-agent systems. However, while much of the research into the temporal logic has centered around the model-checking technique, where the satisfiability of a formula in some linear or branching-time temporal logic is checked with respect to a model derived from a finite-state program, there is an obvious lack of research into efficient proof methods for branching-time logics. Further, in the case of CTL* where even its axiomatization is still an open problem, we do not have such methods at all. The clausal resolution technique presented in this thesis extends Fisher's clausal resolution method for linear-time temporal logic to the branching-time logic CTL and proposes a framework which forms a basis for defining clausal resolution for CTL*. The key elements of the resolution method, namely the normal form, the concept of step resolution and the temporal resolution rule, are introduced and justified with respect to CTL. The basic idea behind the normal form for CTL is to identify the core operators and generate implicative formulae relevant to either the first state in a model, or to all subsequent states in a model. Once the original CTL formula has been translated into its normal form, then all temporal statements within this formula are represented as sets of labelled clauses of the normal form. Incorporating indices as an integral part of this translation, we guarantee correctness of the corresponding transformation rules carried out in a complicated branching-time framework. In order to achieve a refutation step and temporal resolution rules are defined to be applied between clauses generated. Step (classical) resolution can be used between formulae if we are sure that once the constraints on the left hand side are satisfied at the same moment of time, then so are the the right hand side constraints. If the information in a set of formulae of the normal form concerns a situation where some proposition must occur at all future moments (along some or all future paths), and if it is also constrained to be false at some point in the future (along the same path), then a specific temporal resolution rule can be applied. Again, use of indices in defining the resolution rules to work correctly in the branching-time framework is essential. A resolution algorithm is formulated and performed on a number of examples. The main properties of this algorithm, namely, termination, soundness and completeness are established. An algorithm to apply the resolution rule, the most expensive part of the clausal resolution method, has been provided much in the spirit of the analogous methods developed for the linear-time case. Development of the resolution method is more complicated in the case of CTL*. Major difficulties in transforming of CTL* formulae into the desired normal form are identified and linked to the syntactic and semantic features of this very expressive logic. Similar to CTL, the technique developed for CTL* is firstly based upon Emerson's method of the reduction of nesting of path quantifiers to the degree 2. However, unlike in the case of CTL, but similar to linear-time temporal logic, in CTL* we also must reduce the nesting of temporal operators. Different types of nesting of temporal operators for this logic are identified and corresponding rewrite rules to reduce the nesting of each type are formulated and justified. Since application of these rewrite rules reduces the nesting of temporal operators to the desired degree 1, it forms a basis for developing the rest of the required transformation rules enabling us to obtain in this way the full transformation procedure for CTL*. The successful extension of Fisher's normal form to branching-time logic CTL, together with the algorithm for the clausal resolution for CTL, makes the resolution method developed practically suitable for implementation. Also, the investigation into extending the resolution technique to capture CTL* shows the potential of using the normal form to analyze other systems important in the area of automated theorem proving, in particular, temporal fixpoint logics.

Getting my thesis

My doctoral thesis on "resolution in branching-time temporal logic" can be obtained in one of the following ways:

To get a paper copy of the original MMU thesis, please, contact me for the details.

Click here to download full text as gzipped .ps file.

Related publications

Clausal Resolution approach was developed by M.Fisher in
M. Fisher. A Resolution Method for Temporal Logic ,

(in Proceedings of Twelfth International Joint Conference on Artificial Intelligence (IJCAI) , held in Sydney, Australia, August 1991. Published by Morgan Kaufmann).
Fisher, M. A Normal Form for Temporal Logics and its Applications in Theorem-Proving and Execution. Journal of Logic and Computation, 7(4):429-456, August 1997.

C. Dixon.

Strategies for Temporal Resolution,
PhD thesis, The University of Manchester, September 1995. Also Technical Report number UMCS-95-12-1, ISSN 1361-6153, Department of Computer Science, University of Manchester, December 1995. (It's a large file so be warned!)
Dixon, C.,

Temporal Resolution using a Breadth-First Search Algorithm,
in the Annals of Mathematics and Artificial Intelligence, volume 22, special issue on Temporal Representation and Reasoning 1998. Baltzer Science Publishers. ISSN 1012-2443.
The key elements of the resolution method, namely the normal form, the concept of step resolution and a novel temporal resolution rule introduced, justified, and applied in the context of the computation tree logic CTL are described in

A.Bolotov and M.Fisher.

A Resolution Method for CTL Branching Time Temporal Logic.
In IV International Workshop on Temporal Representation and Reasoning (TIME'97), Published by the IEEE, 1997. Please note the IEEE copyright.
Full version of this paper:
A.Bolotov and M.Fisher.

A Clausal Resolution Method for CTL Branching Time Temporal Logic.
In Journal of Experimental and Theoretical Artificial Intelligence, Taylor & Francis, 11, 1999, pp 77-93. Preliminary version is here

A.Bolotov and C.Dixon

Resolution for Branching Time Temporal Logics: Applying the Temporal Resolution Rule.
To appear in the proceedings of TIME2000.
Our approach of developing clausal resolution for the full branching-time logic logic CTL* is described in
A.Bolotov, C.Dixon, and M.Fisher.

Clausal resolution for CTL*. (Please, note the Springer-Verlag copyright.)
Proc. 24-th International Symposium on Mathematical Foundations of Computer Science (MFCS'99), volume 1672 of Lecture Notes in Computer Science, pages 137-148, Springer-Verlag, 1999.
Other related information on research in this area and links can be found in Logic and Computation research group in the University of Liverpool.