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
[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.
- Julian Bradfield and Colin Stirling, Modal logics and mu-calculi, [1]
- Specification Patterns [2]
- Property Pattern Mappings for RAFMC [3]
- more patterns: page 6 of [4]
 |
This mathematical logic-related article is a stub. You can help Wikipedia by expanding it. |
