THE MODAL µ-CALCULUS: A SURVEY
Abstract
The modal µ-calculus is an extension of modal logic with two operators µ and ν, which give the least and greatest fixpoints of monotone operators on powersets. This powerful logic is widely used in computer science, in the area of verification of correctness of concurrent systems. In this survey we review both the theoretical aspects of the modal µ-calculus and its applications to computer science.
Keywords:
µ-calculus, fixed points, model checkingDetails
- Issue
- Vol. 9 No. 3 (2005)
- Section
- Review
- Published
- 2005-09-30
- Licencja:
-
This work is licensed under a Creative Commons Attribution 4.0 International License.
