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 is 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.

• 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.