The modal mu-calculus: a survey
Giacomo Lenzi · TASK Quarterly : scientific bulletin of Academic Computer Centre in Gdansk · 2005
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.