## 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

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 language | English |
---|---|

Title of host publication | Proceedings of the 13th International Conference on Concurrency Theory |

Subtitle of host publication | 13th International Conference Brno, Czech Republic, August 20–23, 2002 Proceedings |

Place of Publication | London, UK, UK |

Publisher | Springer-Verlag |

Pages | 98 |

ISBN (Electronic) | 978-3-540-45694-0 |

ISBN (Print) | 978-3-540-44043-7 |

DOIs | |

Publication status | Published - 2002 |

### Publication series

Name | CONCUR '02 |
---|---|

Publisher | Springer-Verlag |