Clausal Resolution for the Temporal Mu-Calculus

This was an EPSRC funded project. The grant holder was Professor Michael Fisher. Co-investigators: A.Bolotov and Clare Dixon.
Introduction - Project Overview
Project workshop
For the final report please contact Michael Fisher

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.

For further details relating to this project contact Michael Fisher

Main Research Page Research Interests