Introduction to Modal and Temporal Mu-Calculi (Abstract)

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

Modal mu-calculus is a logic obtained by adding fixpoint operators to ordinary modal logic, or Hennessy-Milner logic. The result is a very expressive logic, sufficient to subsume many other temporal logics such as CTL and CTL✱. The modal mu-calculus is easy to model-check, and so makes a good ‘back-end’ logic for tools; it has an interesting theory, with some major problems still open; but it also has a certain reputation for being hard to read and write.
This tutorial provides an introduction to the modal mu-calculus and related logics, suitable for those with some exposure to modal or temporal logic, but without prior knowledge of fixpoint logics.
I start by reviewing the basic semantic setting of processes modelled as transition systems,and briefly review basic modal logic and temporal logics such as CTL.
I then introduce the modal mu-calculus itself. I cover the formal syntax and semantics, and then give more informally the game-based intuition that is most useful in understanding formula of the logic.
I next describe global and local model-checking techniques.
Finally, I discuss the relationship between modal mu-calculus, automata and games, and some of the theoretical questions that have been and are now of interest.
The tutorial is based around the handbook chapter [1],written with Colin Stirling,which forms the text for the tutorial
Original languageEnglish
Title of host publicationProceedings of the 13th International Conference on Concurrency Theory
Subtitle of host publication13th International Conference Brno, Czech Republic, August 20–23, 2002 Proceedings
Place of PublicationLondon, UK, UK
ISBN (Electronic)978-3-540-45694-0
ISBN (Print)978-3-540-44043-7
Publication statusPublished - 2002

Publication series

NameCONCUR '02


Dive into the research topics of 'Introduction to Modal and Temporal Mu-Calculi (Abstract)'. Together they form a unique fingerprint.

Cite this