Modal mu-Calculus and its Alternation Hierarchy

Julian Bradfield

(University of Edinburgh)

The modal mu-calculus is a widely studied and widely used temporal logic for describing properties of systems, such as communications protocols and railway signalling systems. It's a simple but powerful logic, with its power coming from fixpoint operators, which allow the expression of looping properties. When different least and greatest fixpoints depend upon one another, more complex properties appear. For a long time, however, it was not known whether this so-called "alternation" of fixpoints need be taken to arbitrary depths, or whether one or two alternations might always suffice.

In this talk I aim to describe the "alternation hierarchy" problem and its solution for a general audience. Accordingly, the first part of the talk will be an introduction to the modal mu-calculus, concentrating on its intuitive operational meaning rather than its formal semantics, and with a quick look at its major properties and applications. Then I'll explain the notion of alternation and the alternation hierarchy, and why it is interesting to establish its strictness. I'll then describe the techniques used in the solution of the problem, which are conceptually quite simple. If time permits, I can then fill in a few details.
Tuesday 18th November 1997, 14:30
Seminar Room 322
Department of Computer Science