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

1. Scott, Dana; Bakker, Jacobus (1969). "A theory of programs". Unpublished Manuscript.
2. 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.
3. Clarke p.108, Theorem 6; Emerson p. 196
4. Arnold and Niwiński, pp. viii-x and chapter 6
5. Arnold and Niwiński, pp. viii-x and chapter 4
6. Arnold and Niwiński, p. 14
7. Bradfield and Stirling, p. 731
8. Bradfield and Stirling, p. 6
9. 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.
10. Klaus Schneider (2004). Verification of reactive systems: formal methods and algorithms. Springer. p. 521. ISBN 978-3-540-00296-3.
11. 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.
12. 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. pp. 250–259. doi:10.1145/73560.73582. ISBN 0897912527.

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) ; 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