Modal μ-calculus
In theoretical computer science, the modal μ-calculus (Lμ, Lμ, or propositional mu-calculus, sometimes just μ-calculus, although this can have a more general meaning) is an extension of propositional modal logic (with many modalities) by adding the least fixed point operator μ and the greatest fixed point operator ν, thus a fixed-point logic. The (propositional, modal) μ-calculus originates with Dana Scott and Jaco de Bakker, and was further developed by Dexter Kozen into the version most used nowadays.