This talk will provide 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 modal mu-calculus, the result of adding fixpoint operators to basic modal logic. I cover the formal syntax and semantics, and then give more informally the game-based intuition that is most useful in understanding formulae of the logic.

I next describe global and local model-checking techniques.

Finally, I will 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 talk is based on parts of the chapter, written with Colin Stirling, 'Modal logics and mu-calculi: an introduction' in Handbook of Process Algebra (ed. Bergstra, Ponse and Smolka), 293-330, Elsevier, 2001.

A standard approach to proving properties of a cryptographic security protocol is to encode it within a process calculus, and then to apply standard techniqes from concurrency theory such as model-checking or equational reasoning. A promising recent development is to verify properties such as secrecy and authenticity via behavioural type systems. This tutorial reviews the known type systems and results in this area, and suggests areas for further research.