PhD Thesis: Clausal Resolution for Branching-time Logics
Supervisor - Professor Michael
Oral examination - June, 1st, 2000, passed without corrections.
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)
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
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.
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.
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!)
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.
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
Full version of this paper:
A.Bolotov and M.Fisher.
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
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 the CARD
research group WWW-page.