Jacques Duparc: µ-calculus
The µ-calculus is the extension of modal logic with least and greatest ﬁxpoint operators. It ﬁrst appeared in an unpublished manuscript in [Bakker, J. Scott, D.  A theory of programs. Unpublished manuscript, IBM, Vienna, 1969.], and the ter- minology was ﬁxed in [Kozen, D.  Results on the Propositional µ-Calculus. Theoretical Computer Science, 27 (1983), 333-354.].
As a modal logic, the semantic of µ-calculus is usually given by Kripke models or equivalently transition systems or colored graphs. Transition systems play a central role in computer science for analyzing systems or processes operationally. Therefore, the modal µ-calculus provides formal framework where we can study the role of ﬁxpoints in transition systems, in other words, the role of ﬁxpoints in operational semantics. Moreover the µ-calculus is intimately related to infinite games, since the evaluation of a formula in a given structure require the usual evaluation game of modal logic to go on forever.
More generally the modal µ-calculus stands as an abstract framework to reason about ﬁxpoints in modal logics. Thus it is a meta formal system for many logics used in computer science. From the point of view of operational semantics, it is the right weakening of second order logics (the fragment of second order monadic logic invariant under bisimulation) with enough expressibility for practical use.
- Julian Bradfield, Colin Stirling: Modal mu-Calculi. In P. Blackburn, J. van Benthem, F. Wolter ed.: Handbook of Modal Logic, Elsevier (2006). Download preliminary version of the paper
Jacques Duparc is Professor of Formal Logic at the HEC Lausanne.