IJCAR 2001 Tutorial

Clausal Temporal Resolution

Tuesday 19th June 9:00-12:30

Overview

Temporal logic is a variety of non-classical logic that was originally developed in order to represent tense in natural language. Recently, it has achieved a significant role in the formal specification and verification of concurrent and distributed systems, providing a simple mechanism for concisely specifying a number of useful concepts, such as safety, liveness and fairness of computational entities. The increasing importance of temporal verification, in a variety of critical situations, has led to development of a range of proof methods for temporal logics. In this tutorial, we introduce, analyse and develop a clausal approach to resolution in temporal logics.

Objectives

This tutorial will provide an introduction to a key development within temporal proof. As such it will be primarily of value to those working in Computer Science or Artificial Intelligence, who wish to gain an understanding of this approach to temporal proof, but will also be of interest to philosophers and linguists with an interest in how the concept of temporal reasoning is treated in Artificial Intelligence and Computer Science. The tutorial will be supported by explanatory notes.

Content

The tutorial begins by introducing the basic concepts of temporal logics, particularly propositional discrete linear temporal logics. We show how arbitrary specifications in such a logic can be transformed into a simple and intuitive normal form, and then describe the novel resolution rules that can be applied to formulae in this form. We then progressively introduce more complex extensions of the basic approach, tackling clausal resolution within more complex temporal logics, and refinements of clausal temporal resolution itself. The tutorial incorporates a variety of examples, exhibiting the workings of the clausal temporal resolution approach.

Target Audience

We expect attendees to be researchers interested in the foundational aspects of temporal reasoning and temporal verification. The tutorial assumes general knowledge of proof methods (such as tableaux and resolution) and a basic understanding of classical logic (syntax, semantics, proof theory).

Presenters

  Clare Dixon
  Department of Computer Science, 
  The University of Liverpool
  Liverpool, L69 7ZF
  United Kingdom
  email C.Dixon@csc.liv.ac.uk
  tel   (+44 1 51) 794 3674 
  fax   (+44 1 51) 794 3715

  Michael Fisher
  Department of Computer Science, 
  The University of Liverpool
  Liverpool, L69 7ZF
  United Kingdom
  email M.Fisher@csc.liv.ac.uk
  tel   (+44 1 51) 794 6701 
  fax   (+44 1 51) 794 3715

Outline

9:00 - 9:45 Introduction to temporal logics/Separated Normal Form (SNF) syntax, semantics, varieties of temporal structure overview of Kuses of temporal logicsproof methods (tableaux, automaton, resolution) motivation, definition, intuition behind SNF translation of arbitrary formulae into SNF
9:45-10:30 Temporal Resolution Method basic cycle initial and step resolution temporal resolution searching for loops (for temporal resolution) overview of completeness arguments
10:30-11:00 Coffee Break
11:00-11:45 Extending with a Modal Dimension: Temporal Logic of Knowledge definition of modal syntax/semantics and SNF extension modal resolution and correspondence with modal axioms overview of completeness argument problems with interactions
11:45-12:30 Extensions and Restrictions (will include some of the following) definition of extensions to PTL extension to branching-time CTL extension to temporal mu-calculus extension to first-order temporal logic controlling step resolution restricting temporal resolution

References

C. Dixon. Search Strategies for Resolution in Temporal Logics. In Proceedings of the Thirteenth International Conference on Automated Deduction (CADE), 1996.
C. Dixon. Temporal Resolution using a Breadth-First Search Algorithm. Annals of Mathematics and Artificial Intelligence 22, 1998.
C. Dixon, M. Fisher and M. Wooldridge. Resolution for Temporal Logics of Knowledge. Journal of Logic and Computation 8(3). Oxford University Press, 1998.
M. Fisher and C. Dixon. Guiding Clausal Temporal Resolution. In Advances in Temporal Logic. Kluwer Academic Publishers, 2000.
M. Fisher, C. Dixon and M. Peim. Clausal Temporal Resolution. ACM Transactions on Computational Logic 2(1), 2001.
M. Fisher. A Normal Form for Temporal Logics and its Applications in Theorem-Proving and Execution. Journal of Logic and Computation 7(4). Oxford University Press, 1997.

Brief Resume of the Presenters:

Clare Dixon and Michael Fisher have both published and presented widely on the theory, implementation and application of temporal proof and are internationally recognised and respected for their work in this field.

Clare Dixon is an well known for developing practical proof techniques, not only for temporal logics, but also for logics combining temporal and modal dimensions. She has been responsible for key advances in these areas, particularly the development of effective loop search algorithms in temporal resolution and the extension of clausal resolution to temporal logics of knowledge. She also has a high profile in the international TIME workshops, the only annual forum specifically for research into temporal reasoning, co-chairing the 1999 workshop.

Michael Fisher has many years experience working on the specification, verification and implementation of concurrent and distributed systems, in particular utilising temporal logics both as a specification notation and as a programming language. He has been responsible for key advances in temporal logics, such as the introduction of the clausal temporal resolution approach, and the development of a variety of expressive executable temporal logics. In addition to being involved in the TIME workshops, he has also been involved in the International Conference on Temporal Logic.