Abstract

The temporal mu-calculus is a powerful language which extends traditional propositional temporal logics with fixpoint operators and in which properties of a wide range of computational entities may be succinctly specified. However, while a range of automata-theoretic techniques concerning temporal mu-calculi have been developed, more work on efficient deductive methods for such logics is needed. We show how formulae within linear temporal mu-calculus can be transformed into a specific normal form whilst preserving satisfiability and unsatisfiability. This normal form has already served as the basis for a clausal resolution method for a range of temporal logics (such as PLTL and CTL) and so our translation now allows us to apply clausal resolution techniques to the linear-time temporal mu-calculus.

This is joint work with Michael Fisher and Clare Dixon.