Modal μ-calculus – Wikipedia

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

${displaystyle nu }$

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

${displaystyle mu Z.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

${displaystyle phi }$

where the “minimization” (and respectively “maximization”) are in the variable

${displaystyle Z}$

, much like in lambda calculus

${displaystyle lambda Z.phi }$

is a function with formula

${displaystyle phi }$

in bound variable

${displaystyle Z}$

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

Denotational semantics[edit]

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

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

where:

Given a labelled transition system

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

and an interpretation

${displaystyle i}$

of the variables

${displaystyle Z}$

of the

${displaystyle mu }$

-calculus,

${displaystyle [![cdot ]!]_{i}:phi to 2^{S}}$

, is the function defined by the following rules:

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

• 
  ${displaystyle [![phi vee psi ]!]_{i}=[![phi ]!]_{i}cup [![psi ]!]_{i}}$

  ;

• 
  ${displaystyle [![langle arangle phi ]!]_{i}={sin Smid exists tin S,(s,t)in R_{a}wedge tin [![phi ]!]_{i}}}$

  ;

• 
  ${displaystyle [![mu Z.phi ]!]_{i}=bigcap {Tsubseteq Smid [![phi ]!]_{i[Z:=T]}subseteq T}}$

  

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

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

:

The interpretations of

${displaystyle [a]phi }$

and

${displaystyle langle arangle phi }$

are in fact the “classical” ones from dynamic logic. Additionally, the operator

${displaystyle mu }$

can be interpreted as liveness (“something good eventually happens”) and

${displaystyle nu }$

as safety (“nothing bad ever happens”) in Leslie Lamport’s informal classification.^[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]

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.

External links[edit]