In this paper we extend our clausal resolution method for
linear temporal logics to a branching-time framework. The
branching-time temporal logics considered are Computation
Tree Logic (CTL), often regarded as the simplest useful
logic of this class, and Extended CTL (ECTL), which
is CTL extended with fairness operators. The key elements
of the resolution method, namely the normal form, the concept
of step resolution and a novel temporal resolution rule,
are introduced and justified with respect to both these logics.
A completeness argument is provided, together with
an example of the use of the temporal resolution method.
Finally, we consider future work, in particular extension of
the method yet further, to CTL, and implementation of the
approach by utilising techniques developed for linear-time
temporal resolution.
1 Introduction
Temporal logic, which was originally developed as a
logical framework in which to describe tense in natural
languages [13], is now recognized as an essential tool for
reasoning about programs. The sequence of states of a
program’s execution can be considered as a sequence of
moments, or states, within a temporal logic. Thus, proofs
about the correctness of programs correspond to proofs
within an appropriate temporal logic [5]. A particular area
in which temporal logics have been extensively used is in
the specification and verification of properties of concurrent
and distributed systems [12]. The power of the temporal
language allows the representation of a variety of complex
properties relating to these systems, such as liveness,
deadlock and invariance.
As the applications that require concurrent and distributed
solutions have become more refined, so the corresponding
logical tools have been extended. In representing
the behaviour of concurrent systems, the ability to refer to
a range of possible execution paths is seen as important.
Thus, there is a need for methods incorporating branchingtime
temporal logics [1]. Here, the underlying model of
time is of a choice of possibilities branching into the future.
Such branching-time temporal logics have been developed
and applied to the specification of concurrent and
distributed systems [2].
It has been observed that most correctness properties of
concurrent programs (that do not deal with fairness) can
be expressed in a branching-time logic called Computation
Tree Logic (CTL), first proposed in [1]. There are several
extensions of CTL of which CTL is commonly considered
as a full branching-time logic [9]. However, the core
logics we concentrate on, are CTL and its extension Extended
CTL (ECTL) [5], which incorporates simple fairness
constraints. It has been shown that CTL and ECTL
can be respectively extended to CTL and ECTL, where
boolean combinations of temporal modalities are allowed.
Here, CTl is of equivalent expressive power to CTL [6],
however, ECTL is strictly more expressive than ECTL.
Much of the research into the verification of concurrent
and distributed systems has centred around the modelchecking
technique utilising CTL. Here the satisfiability of
a CTL formula is checked with respect to a model derived
from a finite-state program [2], [8]. Due to the success
of this approach, together with a lack of direct applications
of proof in branching-time temporal logics, relatively little
research has been carried out on efficient decision procedures
for such logics. The work that has been produced has
mainly been concerned with basic tableau and automata
methods for these logics [6]. However, in recent years several
applications of branching-time temporal logics requiring
improved proof methods have been developed, most
notably the specification and verification of multi-agent
systems [14]. This has led to the requirement for more
refined, and potentially more efficient, proof methods.
For linear discrete temporal logics we have developed a
proof method based upon clausal temporal resolution [10].
Due to its simple, yet flexible, formulation, this approach
has been shown to be particularly amenable to efficient implementation
[4]. It is based upon a normal form that can