Modal μ-calculus

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]

Syntax

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:

• each proposition and each variable is a formula;
• if ${\displaystyle \phi }$ and ${\displaystyle \psi }$ are formulas, then ${\displaystyle \phi \wedge \psi }$ is a formula;
• if ${\displaystyle \phi }$ is a formula, then ${\displaystyle \neg \phi }$ is a formula;
• if ${\displaystyle \phi }$ is a formula and ${\displaystyle a}$ is an action, then ${\displaystyle [a]\phi }$ is a formula; (pronounced either: ${\displaystyle a}$ box ${\displaystyle \phi }$ or after ${\displaystyle a}$ necessarily ${\displaystyle \phi }$)
• if ${\displaystyle \phi }$ is a formula and ${\displaystyle Z}$ a variable, then ${\displaystyle \nu Z.\phi }$ is a formula, provided that every free occurrence of ${\displaystyle Z}$ in ${\displaystyle \phi }$ occurs positively, i.e. within the scope of an even number of negations.

(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:

• ${\displaystyle \phi \lor \psi }$ meaning ${\displaystyle \neg (\neg \phi \land \neg \psi )}$
• ${\displaystyle \langle a\rangle \phi }$ (pronounced either: ${\displaystyle a}$ diamond ${\displaystyle \phi }$ or after ${\displaystyle a}$ possibly ${\displaystyle \phi }$) meaning ${\displaystyle \neg [a]\neg \phi }$
• ${\displaystyle \mu Z.\phi }$ means ${\displaystyle \neg \nu Z.\neg \phi [Z:=\neg Z]}$, where ${\displaystyle \phi [Z:=\neg Z]}$ means substituting ${\displaystyle \neg Z}$ for ${\displaystyle Z}$ in all free occurrences of ${\displaystyle Z}$ in ${\displaystyle \phi }$.

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

Models of (propositional) μ-calculus are given as labelled transition systems ${\displaystyle (S,R,V)}$ where:

• ${\displaystyle S}$ is a set of states;
• ${\displaystyle R}$ maps to each label ${\displaystyle a}$ a binary relation on ${\displaystyle S}$;
• ${\displaystyle V:P\to 2^{S}}$, maps each proposition ${\displaystyle p\in P}$ to the set of states where the proposition is true.

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:

• ${\displaystyle [\![p]\!]_{i}=V(p)}$;
• ${\displaystyle [\![Z]\!]_{i}=i(Z)}$;
• ${\displaystyle [\![\phi \wedge \psi ]\!]_{i}=[\![\phi ]\!]_{i}\cap [\![\psi ]\!]_{i}}$;
• ${\displaystyle [\![\neg \phi ]\!]_{i}=S\smallsetminus [\![\phi ]\!]_{i}}$;
• ${\displaystyle [\![[a]\phi ]\!]_{i}=\{s\in S\mid \forall t\in S,(s,t)\in R_{a}\rightarrow t\in [\![\phi ]\!]_{i}\}}$;
• ${\displaystyle [\![\nu Z.\phi ]\!]_{i}=\bigcup \{T\subseteq S\mid T\subseteq [\![\phi ]\!]_{i[Z:=T]}\}}$, where ${\displaystyle i[Z:=T]}$ maps ${\displaystyle Z}$ to ${\displaystyle T}$ while preserving the mappings of ${\displaystyle i}$ everywhere else.

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

• ${\displaystyle [\![\phi \vee \psi ]\!]_{i}=[\![\phi ]\!]_{i}\cup [\![\psi ]\!]_{i}}$;
• ${\displaystyle [\![\langle a\rangle \phi ]\!]_{i}=\{s\in S\mid \exists t\in S,(s,t)\in R_{a}\wedge t\in [\![\phi ]\!]_{i}\}}$;
• ${\displaystyle [\![\mu Z.\phi ]\!]_{i}=\bigcap \{T\subseteq S\mid [\![\phi ]\!]_{i[Z:=T]}\subseteq T\}}$

Less formally, this means that, for a given transition system ${\displaystyle (S,R,V)}$:

• ${\displaystyle p}$ holds in the set of states ${\displaystyle V(p)}$;
• ${\displaystyle \phi \wedge \psi }$ holds in every state where ${\displaystyle \phi }$ and ${\displaystyle \psi }$ both hold;
• ${\displaystyle \neg \phi }$ holds in every state where ${\displaystyle \phi }$ does not hold.
• ${\displaystyle [a]\phi }$ holds in a state ${\displaystyle s}$ if every ${\displaystyle a}$-transition leading out of ${\displaystyle s}$ leads to a state where ${\displaystyle \phi }$ holds.
• ${\displaystyle \langle a\rangle \phi }$ holds in a state ${\displaystyle s}$ if there exists ${\displaystyle a}$-transition leading out of ${\displaystyle s}$ that leads to a state where ${\displaystyle \phi }$ holds.
• ${\displaystyle \nu Z.\phi }$ holds in any state in any set ${\displaystyle T}$ such that, when the variable ${\displaystyle Z}$ is set to ${\displaystyle T}$, then ${\displaystyle \phi }$ holds for all of ${\displaystyle T}$. (From the Knaster–Tarski theorem it follows that ${\displaystyle [\![\nu Z.\phi ]\!]_{i}}$ is the greatest fixed point of ${\displaystyle T\mapsto [\![\phi ]\!]_{i[Z:=T]}}$, and ${\displaystyle [\![\mu Z.\phi ]\!]_{i}}$ its least fixed point.)

The interpretations of ${\displaystyle [a]\phi }$ and ${\displaystyle \langle a\rangle \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

• ${\displaystyle \nu Z.\phi \wedge [a]Z}$ is interpreted as "${\displaystyle \phi }$ is true along every a-path".^[7] The idea is that "${\displaystyle \phi }$ is true along every a-path" can be defined axiomatically as that (weakest) sentence ${\displaystyle Z}$ which implies ${\displaystyle \phi }$ and which remains true after processing any a-label. ^[8]
• ${\displaystyle \mu Z.\phi \vee \langle a\rangle Z}$ is interpreted as the existence of a path along a-transitions to a state where ${\displaystyle \phi }$ holds.^[9]
• The property of a state being deadlock-free, meaning no path from that state reaches a dead end, is expressed by the formula^[9]
  $${\displaystyle \nu Z.\left(\bigvee _{a\in A}\langle a\rangle \top \wedge \bigwedge _{a\in A}[a]Z\right)}$$

  

Decision problems

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

• Finite model theory
• Alternation-free modal μ-calculus

Notes

References

• 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

• Sophie Pinchinat, Logic, Automata & Games video recording of a lecture at ANU Logic Summer School '09

This page was last edited on 21 May 2024, at 18:43