The propositional μ-calculus and its use in model checking

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 μ-calculus. The emphasis, as before, is on a broad understanding rather than on technical details.