Mu calculus

From Wikipedia, the free encyclopedia

The μ-calculus (also modal μ calculus) is a class of temporal logics with a least fixpoint operator μ. It is used to describe properties of labelled transition systems and for verifying these properties.

The (propositional) μ-calculus was invented by Scott and De Bakker^[1], and further developed by Kozen into the version most people use nowadays.

Many temporal logics can be encoded in the μ-calculus, such as LTL, CTL and CTL*.^[2]

[edit] Notes

1. ^ Kozen p.333
2. ^ Clarke p.108, Theorem 6; Emerson p.196

[edit] References

• Clarke, Jr., Edmund M.; Orna Grumberg, Doron A. Peled (1999). Model Checking. Cambridge, Massachusetts, USA: MIT press. ISBN 0-262-03270-8. 

• Stirling, Colin. (2001). Modal and Temporal Properties of Processes. New York, Berlin, Heidelberg: Springer Verlag. ISBN 0-387-98717-7. 

• Emerson, E. Allen (1996). "Model Checking and the Mu-calculus". Descriptive Complexity and Finite Models: 185-214, American Mathematical Society. ISBN 0-8218-0517-7. 

• Kozen, Dexter (1983). "Results on the Propositional μ-Calculus". Theoretical Computer Science 27 (3): 333–354. doi:10.1016/0304-3975(82)90125-6.