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.