Efficient Control of Temporal Reasoning
The aim of this PhD project is to develop techniques
to improve the efficiency of temporal reasoning. Such reasoning
underlies much of the research carried out within the Logic and Computation
Group. As temporal
reasoning is inherently complex, methods to prune the search space and
to guide the reasoner are essential. Improvements in efficiency will
thus allow these techniques to be applied to larger and more complex
problems, hence tackling new applications such as security of
distributed systems and knowledge representation.
Background
The representation of dynamic activity via a
temporal logic formalism is used in a wide variety of areas within
Computer Science and Artificial Intelligence, for example Robotics
[1], Databases [2], Program Specification [3], Hardware Verification
[4], and Agent-Based Systems [5]. Temporal logics are extensions of
classical logic that have been used successfully in the specification
of safety, liveness and fairness properties in a range of dynamic
systems. Such a logical representation of a system then permits the
analysis of the system's properties via logical proof. As part of our
ongoing research, we have developed a proof method for temporal logics
based upon the use of clausal resolution [6,7]. This has been defined,
proved correct, implemented and extended in a number of ways. While
this is a simple and powerful approach, the practical mechanisation of
temporal proof is often very expensive in terms of both time and space
required. For example, while our clausal temporal resolution approach
has been successfully employed for a range of problems, experiments
have shown that, in a number of cases, the basic method leads to the
generation of an unnecessarily large set of formulas during the
proof. As the majority of these formulas are irrelevant to the
refutation, it is clear that refinements are needed if more complex
reasoning tasks are to be attempted.
Project Outline
The second approach concerns such high-level strategies for guiding
proof search. In resolution-based theorem-provers developed for
classical logics, a particularly successful strategy for avoiding the
generation of redundant information during proof has been the set of
support strategy, which restricts the application of a resolution rule
(using semantic or syntactic information from the formula being
proved) thus pruning part of the search space. This has led to very
efficient proof techniques for classical logics, even reaching the
stage where automated theorem-proving systems can now solve open
problems within Mathematics [10]. We have examined the set of support
strategy within the context of temporal resolution [11], and have
shown how it can potentially aid the practical efficiency of temporal
reasoning systems. Thus, the core part of this project is to combine
the two approaches above and examine the practical efficiency of such
combined strategies.
Further strategies concerning the ordering of proof steps to be
undertaken have been developed for classical logics. Essentially,
components of each formula are given numerical values and inference
steps are dependent upon these values. The method of attributing these
values and deciding whether inferences are allowed controls what, and
how much, information can be derived. A second part of the project is
to analyse and, if possible, transfer such ordering strategies from
the classical to the temporal context. The final aspect of the project
concerns the application and analysis of the temporal reasoning system
developed on a range of larger examples, extracted from real-world
applications.
In simpler logics, clausal resolution has been shown to be amenable
to efficient implementation, often through the control of proof
using high-level strategies [8]. Thus, the aim of this project is
to attempt to develop, apply and analyse such strategies within the
context of temporal resolution. There are several ways that this
might be achieved, two of which we have already examined from a
theoretical viewpoint. The first approach, adopted in [9], is to
refine the temporal resolution method to allow the application of a
novel temporal resolution rule earlier in the proof. The output of
this rule application is then used to guide subsequent steps, thus
providing the potential for much more flexibility and avoiding the
generation of irrelevant information. Typically, in order to use
this approach effectively, a suitable sophisticated high-level
control strategy will be needed.
References
Project Environment
The work will take place within the
Logic and Computation Research Group within the Department of Computer
Science, under the supervision of Michael Fisher, who
has an international reputation in logic, agent-based systems and
programming languages, and Clare Dixon, who has
an international reputation in temporal reasoning, automated
theorem-proving, and verification.
If you require any further details concerning
this project, contact Michael Fisher (M.Fisher@csc.liv.ac.uk)