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]

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 }${\displaystyle \phi } and ${\displaystyle \psi }${\displaystyle \psi } are formulas, then ${\displaystyle \phi \wedge \psi }${\displaystyle \phi \wedge \psi } is a formula;
• if ${\displaystyle \phi }${\displaystyle \phi } is a formula, then ${\displaystyle \neg \phi }${\displaystyle \neg \phi } is a formula;
• if ${\displaystyle \phi }${\displaystyle \phi } is a formula and ${\displaystyle a}${\displaystyle a} is an action, then ${\displaystyle [a]\phi }${\displaystyle [a]\phi } is a formula; (pronounced either: ${\displaystyle a}${\displaystyle a} box ${\displaystyle \phi }${\displaystyle \phi } or after ${\displaystyle a}${\displaystyle a} necessarily ${\displaystyle \phi }${\displaystyle \phi })
• if ${\displaystyle \phi }${\displaystyle \phi } is a formula and ${\displaystyle Z}${\displaystyle Z} a variable, then ${\displaystyle \nu Z.\phi }${\displaystyle \nu Z.\phi } is a formula, provided that every free occurrence of ${\displaystyle Z}${\displaystyle Z} in ${\displaystyle \phi }${\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 }${\displaystyle \nu } is the only binding operator.)

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

• ${\displaystyle \phi \lor \psi }${\displaystyle \phi \lor \psi } meaning ${\displaystyle \neg (\neg \phi \land \neg \psi )}${\displaystyle \neg (\neg \phi \land \neg \psi )}
• ${\displaystyle \langle a\rangle \phi }${\displaystyle \langle a\rangle \phi } (pronounced either: ${\displaystyle a}${\displaystyle a} diamond ${\displaystyle \phi }${\displaystyle \phi } or after ${\displaystyle a}${\displaystyle a} possibly ${\displaystyle \phi }${\displaystyle \phi }) meaning ${\displaystyle \neg [a]\neg \phi }${\displaystyle \neg [a]\neg \phi }
• ${\displaystyle \mu Z.\phi }${\displaystyle \mu Z.\phi } means ${\displaystyle \neg \nu Z.\neg \phi [Z:=\neg Z]}${\displaystyle \neg \nu Z.\neg \phi [Z:=\neg Z]}, where ${\displaystyle \phi [Z:=\neg Z]}${\displaystyle \phi [Z:=\neg Z]} means substituting ${\displaystyle \neg Z}${\displaystyle \neg Z} for ${\displaystyle Z}${\displaystyle Z} in all free occurrences of ${\displaystyle Z}${\displaystyle Z} in ${\displaystyle \phi }${\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 }${\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 }${\displaystyle \phi } where the "minimization" (and respectively "maximization") are in the variable ${\displaystyle Z}${\displaystyle Z}, much like in lambda calculus ${\displaystyle \lambda Z.\phi }${\displaystyle \lambda Z.\phi } is a function with formula ${\displaystyle \phi }${\displaystyle \phi } in bound variable ${\displaystyle Z}${\displaystyle Z};^[6] see the denotational semantics below for details.

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

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

Given a labelled transition system ${\displaystyle (S,R,V)}${\displaystyle (S,R,V)} and an interpretation ${\displaystyle i}${\displaystyle i} of the variables ${\displaystyle Z}${\displaystyle Z} of the ${\displaystyle \mu }${\displaystyle \mu }-calculus, ${\displaystyle [\![\cdot ]\!]_{i}:\phi \to 2^{S}}${\displaystyle [\![\cdot ]\!]_{i}:\phi \to 2^{S}}, is the function defined by the following rules:

• ${\displaystyle [\![p]\!]_{i}=V(p)}${\displaystyle [\![p]\!]_{i}=V(p)};
• ${\displaystyle [\![Z]\!]_{i}=i(Z)}${\displaystyle [\![Z]\!]_{i}=i(Z)};
• ${\displaystyle [\![\phi \wedge \psi ]\!]_{i}=[\![\phi ]\!]_{i}\cap [\![\psi ]\!]_{i}}${\displaystyle [\![\phi \wedge \psi ]\!]_{i}=[\![\phi ]\!]_{i}\cap [\![\psi ]\!]_{i}};
• ${\displaystyle [\![\neg \phi ]\!]_{i}=S\smallsetminus [\![\phi ]\!]_{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 [\![[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]}\}}${\displaystyle [\![\nu Z.\phi ]\!]_{i}=\bigcup \{T\subseteq S\mid T\subseteq [\![\phi ]\!]_{i[Z:=T]}\}}, where ${\displaystyle i[Z:=T]}${\displaystyle i[Z:=T]} maps ${\displaystyle Z}${\displaystyle Z} to ${\displaystyle T}${\displaystyle T} while preserving the mappings of ${\displaystyle i}${\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 [\![\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 [\![\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\}}${\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 (S,R,V)}:

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

The interpretations of ${\displaystyle [a]\phi }${\displaystyle [a]\phi } and ${\displaystyle \langle a\rangle \phi }${\displaystyle \langle a\rangle \phi } are in fact the "classical" ones from dynamic logic. Additionally, the operator ${\displaystyle \mu }${\displaystyle \mu } can be interpreted as liveness ("something good eventually happens") and ${\displaystyle \nu }${\displaystyle \nu } as safety ("nothing bad ever happens") in Leslie Lamport's informal classification.^[7]

• ${\displaystyle \nu Z.\phi \wedge [a]Z}${\displaystyle \nu Z.\phi \wedge [a]Z} is interpreted as "${\displaystyle \phi }${\displaystyle \phi } is true along every a-path".^[7] The idea is that "${\displaystyle \phi }${\displaystyle \phi } is true along every a-path" can be defined axiomatically as that (weakest) sentence ${\displaystyle Z}${\displaystyle Z} which implies ${\displaystyle \phi }${\displaystyle \phi } and which remains true after processing any a-label. ^[8]
• ${\displaystyle \mu Z.\phi \vee \langle a\rangle Z}${\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 }${\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)}$${\displaystyle \nu Z.\left(\bigvee _{a\in A}\langle a\rangle \top \wedge \bigwedge _{a\in A}[a]Z\right)}

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]

Actually, the complexity of the satisfiability problem of graded modal μ-calculus is also EXPTIME-complete, even if the number in the modalities are written in binary (graded modal μ-calculus is an extension of standard modal μ-calculus with modalities "there are at least k successors such that...).^[13]

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

• 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.

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

• Modal logic
• Model checking

• Articles with short description
• Short description is different from Wikidata