# Modal μ-calculus – Wikipedia

From Wikipedia, the free encyclopedia

In theoretical computer science, the **modal μ-calculus** (**Lμ**, **L _{μ}**, 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,^{[1]} and was further developed by Dexter Kozen^{[2]} into the version most used nowadays. It is used to describe properties of labelled transition systems and for verifying these properties. Many temporal logics can be encoded in the μ-calculus, including CTL* and its widely used fragments—linear temporal logic and computational tree logic.^{[3]}

An algebraic view is to see it as an algebra of monotonic functions over a complete lattice, with operators consisting of functional composition plus the least and greatest fixed point operators; from this viewpoint, the modal μ-calculus is over the lattice of a power set algebra.^{[4]} The game semantics of μ-calculus is related to two-player games with perfect information, particularly infinite parity games.^{[5]}

Let *P* (propositions) and *A* (actions) be two finite sets of symbols, and let Var be a countably infinite set of variables. The set of formulas of (propositional, modal) μ-calculus is defined as follows:

(The notions of free and bound variables are as usual, where

is the only binding operator.)

Given the above definitions, we can enrich the syntax with:

The first two formulas are the familiar ones from the classical propositional calculus and respectively the minimal multimodal logic **K**.

The notation

μZ.ϕ{displaystyle mu Z.phi }ϕ{displaystyle phi } (and its dual) are inspired from the lambda calculus; the intent is to denote the least (and respectively greatest) fixed point of the expression

Z{displaystyle Z} where the “minimization” (and respectively “maximization”) are in the variable

λZ.ϕ{displaystyle lambda Z.phi } , much like in lambda calculus

ϕ{displaystyle phi } is a function with formula

Z{displaystyle Z} in bound variable

^{[6]} see the denotational semantics below for details.

## Denotational semantics[edit]

Models of (propositional) μ-calculus are given as labelled transition systems

(S,R,V){displaystyle (S,R,V)}where:

Given a labelled transition system

(S,R,V){displaystyle (S,R,V)}i{displaystyle i} and an interpretation

Z{displaystyle Z} of the variables

μ{displaystyle mu } of the

[[⋅]]i:ϕ→2S{displaystyle [![cdot ]!]_{i}:phi to 2^{S}} -calculus,

, is the function defined by the following rules:

By duality, the interpretation of the other basic formulas is:

[[ϕ∨ψ]]i=[[ϕ]]i∪[[ψ]]i{displaystyle [![phi vee psi ]!]_{i}=[![phi ]!]_{i}cup [![psi ]!]_{i}} ;

[[⟨a⟩ϕ]]i={s∈S∣∃t∈S,(s,t)∈Ra∧t∈[[ϕ]]i}{displaystyle [![langle arangle phi ]!]_{i}={sin Smid exists tin S,(s,t)in R_{a}wedge tin [![phi ]!]_{i}}} ;

[[μZ.ϕ]]i=⋂{T⊆S∣[[ϕ]]i[Z:=T]⊆T}{displaystyle [![mu Z.phi ]!]_{i}=bigcap {Tsubseteq Smid [![phi ]!]_{i[Z:=T]}subseteq T}}

Less formally, this means that, for a given transition system

(S,R,V){displaystyle (S,R,V)}:

The interpretations of

[a]ϕ{displaystyle [a]phi }⟨a⟩ϕ{displaystyle langle arangle phi } and

μ{displaystyle mu } are in fact the “classical” ones from dynamic logic. Additionally, the operator

ν{displaystyle nu } can be interpreted as liveness (“something good eventually happens”) and

^{[7]}

### Examples[edit]

## Decision problems[edit]

Satisfiability of a modal μ-calculus formula is EXPTIME-complete.^{[10]} Like for linear temporal logic,^{[11]} the model checking, satisfiability and validity problems of linear modal μ-calculus are PSPACE-complete.^{[12]}

## See also[edit]

**^**Scott, Dana; Bakker, Jacobus (1969). “A theory of programs”.*Unpublished manuscript*.**^**Kozen, Dexter (1982). “Results on the propositional μ-calculus”.*Automata, Languages and Programming*. ICALP. Vol. 140. pp. 348–359. doi:10.1007/BFb0012782. ISBN 978-3-540-11576-2.**^**Clarke p.108, Theorem 6; Emerson p. 196**^**Arnold and Niwiński, pp. viii-x and chapter 6**^**Arnold and Niwiński, pp. viii-x and chapter 4**^**Arnold and Niwiński, p. 14- ^
^{a}^{b}Bradfield and Stirling, p. 731 **^**Bradfield and Stirling, p. 6- ^
^{a}^{b}Erich Grädel; Phokion G. Kolaitis; Leonid Libkin; Maarten Marx; Joel Spencer; Moshe Y. Vardi; Yde Venema; Scott Weinstein (2007).*Finite Model Theory and Its Applications*. Springer. p. 159. ISBN 978-3-540-00428-8. **^**Klaus Schneider (2004).*Verification of reactive systems: formal methods and algorithms*. Springer. p. 521. ISBN 978-3-540-00296-3.**^**Sistla, A. P.; Clarke, E. M. (1985-07-01). “The Complexity of Propositional Linear Temporal Logics”.*J. ACM*.**32**(3): 733–749. doi:10.1145/3828.3837. ISSN 0004-5411.**^**Vardi, M. Y. (1988-01-01). “A Temporal Fixpoint Calculus”.*Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*. POPL ’88. New York, NY, USA: ACM: 250–259. doi:10.1145/73560.73582. ISBN 0897912527.

## References[edit]

- Clarke, Edmund M. Jr.; Orna Grumberg; Doron A. Peled (1999).
*Model Checking*. Cambridge, Massachusetts, USA: MIT press. ISBN 0-262-03270-8., chapter 7, Model checking for the μ-calculus, pp. 97–108 - Stirling, Colin. (2001).
*Modal and Temporal Properties of Processes*. New York, Berlin, Heidelberg: Springer Verlag. ISBN 0-387-98717-7., chapter 5, Modal μ-calculus, pp. 103–128 - André Arnold; Damian Niwiński (2001).
*Rudiments of μ-Calculus*. Elsevier. ISBN 978-0-444-50620-7., chapter 6, The μ-calculus over powerset algebras, pp. 141–153 is about the modal μ-calculus - Yde Venema (2008) Lectures on the Modal μ-calculus; was presented at The 18th European Summer School in Logic, Language and Information
- Bradfield, Julian & Stirling, Colin (2006). “Modal mu-calculi”. In P. Blackburn; J. van Benthem & F. Wolter (eds.).
*The Handbook of Modal Logic*. Elsevier. pp. 721–756. - Emerson, E. Allen (1996). “Model Checking and the Mu-calculus”.
*Descriptive Complexity and Finite Models*. American Mathematical Society. pp. 185–214. 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.

## Recent Comments