J.I. Zucker (1993): The propositional mu-calculus and its use in model checking, in Functional Programming, Concurrency, Simulation and Automated Reasoning, ed. P.E. Lauer, [text.ps]

Abstract. This paper, and the preceding one, survey two types of formalism which has proved to be particularly successful for efficient automatic verification, or "model checking", of concurrent systems. In the previous paper we considered branching time propositional temporal logics, and now we turn to a more general formalism, the propositional mu-calculus.

The emphasis, as before, is on a broad understanding rather than on technical details.