Philosophy:Modal μ-calculus

From HandWiki

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

(The notions of free and bound variables are as usual, where [math]\displaystyle{ \nu }[/math] is the only binding operator.)

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

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

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

The notation [math]\displaystyle{ \mu Z. \phi }[/math] (and its dual) are inspired from the lambda calculus; the intent is to denote the least (and respectively greatest) fixed point of the expression [math]\displaystyle{ \phi }[/math] where the "minimization" (and respectively "maximization") are in the variable [math]\displaystyle{ Z }[/math], much like in lambda calculus [math]\displaystyle{ \lambda Z. \phi }[/math] is a function with formula [math]\displaystyle{ \phi }[/math] in bound variable [math]\displaystyle{ Z }[/math];[6] see the denotational semantics below for details.

Denotational semantics

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

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

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

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

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

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

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

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

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

Examples

  • [math]\displaystyle{ \nu Z.\phi \wedge [a]Z }[/math] is interpreted as "[math]\displaystyle{ \phi }[/math] is true along every a-path".[7] The idea is that "[math]\displaystyle{ \phi }[/math] is true along every a-path" can be defined axiomatically as that (weakest) sentence [math]\displaystyle{ Z }[/math] which implies [math]\displaystyle{ \phi }[/math] and which remains true after processing any a-label. [8]
  • [math]\displaystyle{ \mu Z.\phi \vee \langle a \rangle Z }[/math] is interpreted as the existence of a path along a-transitions to a state where [math]\displaystyle{ \phi }[/math] 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] [math]\displaystyle{ \nu Z.\left (\bigvee_{a\in A}\langle a\rangle\top\wedge \bigwedge_{a\in A}[a]Z \right) }[/math]

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

Notes

  1. ↑ Scott, Dana; Bakker, Jacobus (1969). "A theory of programs". Unpublished Manuscript. 
  2. ↑ Kozen, Dexter (1982). "Results on the propositional μ-calculus". ICALP. 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. ↑ 7.0 7.1 Bradfield and Stirling, p. 731
  8. ↑ Bradfield and Stirling, p. 6
  9. ↑ 9.0 9.1 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. https://books.google.com/books?id=e6ST-AVC27AC&pg=PA159. 
  10. ↑ Klaus Schneider (2004). Verification of reactive systems: formal methods and algorithms. Springer. p. 521. ISBN 978-3-540-00296-3. https://books.google.com/books?id=Z92bL1VrD_sC&pg=PA521. 
  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) 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". The Handbook of Modal Logic. Elsevier. pp. 721–756. http://homepages.inf.ed.ac.uk/jcb/Research/pubs.html#mlh-chapter. 
  • Emerson, E. Allen (1996). "Model Checking and the Mu-calculus". 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



Retrieved from "https://handwiki.org/wiki/index.php?title=Philosophy:Modal_μ-calculus&oldid=3288518"