Modal mu-calculus

Summary

The modal $\mu$-calculus extends modal logic with a least fixed point operator $\mu$ and a greatest fixed point operator $\nu$. Formulas are evaluated at the states of a labelled transition system, and fixed points express recursive properties such as reachability and invariance. It contains computation tree logic and linear temporal logic by translation, so it serves as a common target logic for model checking.