Clausal Resolution for the Temporal Mu-Calculus

This is an EPSRC funded project. The grant holder is Professor Michael Fisher. This page contains the following information concerning this project:

Introduction - Project Overview
Related publications

Introduction - Project Overview

In the area of formal specification and verification of concurrent and distributed systems, mu-calculi play a significant role. It is commonly recognised that these reactive systems represent one of the most important classes of systems in computer science. Although analysis of these systems is difficult, it has been tackled, in recent years, using modal and temporal logics. In particular, a number of useful concepts, such as safety, liveness and fairness can be formally specified by temporal logics ranging from simple linear-time logics to more expressive branching-time logics such as computation tree logic (CTL) and its extension. While this approach has been successful, there are common circumstances that are not even expressible in CTL*, for example the fact that a property occurs at every even moment of time. Thus, more expressive logical facilities than those found in simple linear or branching-time logics are required; it is for these reasons that we consider temporal mu-calculus. Temporal mu-calculus is an extension of propositional temporal logic with fixed points representing maximal and minimal solutions to temporal equations. One of the crucial features of the mu-calculus is its use of a recursion operator as a basic connective, thus allowing the representation of recurrent properties in a natural way. These features of the mu-calculus allow it to be applied in, for example, hardware specification and verification, with such problems as proving that an n-bit adder meets its specification or verifying properties of a circuit that should hold for all instants of time. Further, when looking for regularities in systems, including those that have parameterised behavioral specifications, one of the key approaches used involves observing a particular fixed point is reached; a case ideal for the mu-calculus. In classifying formal verification methods, two major approaches can be distinguished, namely algorithmic and deductive methods. While the algorithmic approach, for example model checking, is fully automated its application is generally restricted to finite-state systems. On the other hand, deductive methods based on theorem-proving can handle arbitrarily complex systems providing uniform proofs, but in most cases require guidance and assistance. In this respect, an investigation into increased automation in deductive methods is essential if these methods are to be used in real applications. Thus, we consider a resolution-based approach, which has been shown to be both efficient and flexible in the case of both classical and standard temporal logics. Given the above observations, and considering the range of applications where both the expressiveness of mu-calculus and effective mechanisation are required, leads us to the principal task of this project: an analysis of the temporal mu-calculus based on clausal resolution. Development of an efficient deductive system for the mu-calculus is also an important theoretical goal. Recently, mu-calculus has been studied in terms of an axiomatic approach, using game-theoretic techniques, tableaux methods, automata and model checking. However, resolution-based approaches, very efficient in other areas, have not yet been investigated in this framework. We have proposed a novel clausal resolution method for the linear-time temporal logic. This approach has three key components: the translation to a normal form (SNF), the application of step, or classical-style, resolution and the application of a novel temporal resolution rule. The transformation of formulae to SNF involves special `unfolding' rules based on the fixed-point characterisation of temporal operators, while the temporal resolution rule itself is linked to mu-calculus since its central aim is to resolve a set of SNF clauses representing the ``always in the future'' operator (a maximal fixed point) with a ``sometime in the future'' formula (a minimal fixed point). The normal form, together with the renaming techniques used to generate it, have provided a significant methodological tool which has allowed the clausal resolution approach to be extended to sophisticated logics such as temporal logics of knowledge and belief and branching-time temporal logic. Work on the implementation of the resolution procedure has also led to both efficient implementation techniques, and improvements in heuristics. Thus, the aim of this project is to develop a clausal resolution method for the temporal mu-calculus. We believe that the success of this research will bring significant contributions, allowing the incorporation of a variety of refinement and optimisation mechanisms for resolution already developed for classical, modal and temporal logics, and leading to improved practical verification techniques for complex reactive systems.

Ongoing work

The general problem structure that we are trying to solve is graphically presented as follows.
 
 
Figure 1: Problem structure

Thus, we can see the attraction of model-checking: if specification is given as a finite state machine then its translation to automata is polynomial.
In contrast, verification of formulae in the Normal Form is usually exponential since it involves some form of proof (in our case, clausal resolution). However, we are often able to use either improved proof strategies or restricted forms of the normal form in order to improve the practical efficiency of such proof.

Click below to see the definition of the normal form

The following has been shown in our research papers:
 

  •  B'uchi automaton can be represented in our Normal form.

  •  
  •  The flat linear-time fixpoint logic can be translated into our normal form.

  • Click below to see the representation of "even(p)" in the normal form.
     


    Research papers

  •  (with C.Dixon and M.Fisher)

  •     Clausal Resolution for Linear-time Temporal  Mu-calculus. (submitted)
     
  •  (with C.Dixon and M.Fisher)

  •     On the Relationship between `w'-automata and Temporal Logic Normal Form. In the proceedings of the Advances in Modal Logic - International Conference on Temporal Logic 2000, Leipzig, October, 2000.
     
     

    Related publications

    Clausal Resolution approach was developed by M.Fisher in
  • Fisher, M.,  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.

  • The development of the implementation aspects of this approach can be found in the following papers written by C.Dixon

  • 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.
  • 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!)

    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 can be found here

    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.


    Presentations

    General Normal form for Temporal logic. Presented at the
    16th annual British Colloquium for Theoretical Computer Science (BCTCS16)
    hosted by the Department of Computer Science,University of Liverpool between 10-12th April 2000.
    Clausal Resolution for Linear-time mu-calculus. Presented at the theory seminar,
    Laboratory for Foundatons of Computer Science, Department of Computer Science, University of Edinburgh, October, 2000.
    Other related information on research in this area and links can be found in the