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.
KeywordsModel Check Propositional Variable Propositional Atom Fairness Property Propositional Constant
Unable to display preview. Download preview PDF.
- Bradfield, J. Stirling, C. (1990): Local model checking for infinite state spaces. Report no. ECS-LFCS-90-115, Laboratory for Foundations of Computer Science, University of Edinburgh.Google Scholar
- Cleaveland, R. (1990): Tableau-based model checking in the propositional mu-calculus. Acta Informatica 27, 725–747Google Scholar
- Cleaveland, R. (1992): The Concurrency Workbench. In this volume.Google Scholar
- Emerson, E.A., Lei, C.-L. (1986): Efficient model checking in fragments of the propositional mu-calculus (Extended abstract). In: Proc. IEEE Symp. on Logic in Computer Science, June 1986, Cambridge, MA, pp. 267–278Google Scholar
- Stirling, C., Walker, D. (1991): Local model checking in the modal mu-calculus. Theoretical Computer Science 89, 161–177.Google Scholar
- Winskel, G. (1989): A note on model checking the modal ν-calculus. In: 16th International Colloq. on Automata, Languages and Programming, Stresa, Italy, July 1989 (ed. G. Ausiello, M. Desani-Ciancaglini, S. Ronchi della Rocca). Lecture Notes in Conputer Science, vol. 372, Springer-Verlag, pp. 761–772Google Scholar
- J.I. Zucker (1992): Propositional temporal logics and their use in model checking. In this volume.Google Scholar