Modal μ-calculus – Wikipedia

From Wikipedia, the free encyclopedia

In theoretical computer science, the modal μ-calculus (, 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

μZ.ϕ{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

Z{displaystyle Z}

, much like in lambda calculus

λZ.ϕ{displaystyle lambda Z.phi }

is a function with formula

ϕ{displaystyle phi }

in bound variable

Z{displaystyle Z}

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

Denotational semantics[edit]

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

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

where:

Given a labelled transition system

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

and an interpretation

i{displaystyle i}

of the variables

Z{displaystyle Z}

of the

μ{displaystyle mu }

-calculus,

[[⋅]]i:ϕ→2S{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:


  • [[ϕ∨ψ]]i=[[ϕ]]i∪[[ψ]]i{displaystyle [![phi vee psi ]!]_{i}=[![phi ]!]_{i}cup [![psi ]!]_{i}}

    ;

  • [[⟨a⟩ϕ]]i={s∈S∣∃t∈S,(s,t)∈Ra∧t∈[[ϕ]]i}{displaystyle [![langle arangle phi ]!]_{i}={sin Smid exists tin S,(s,t)in R_{a}wedge tin [![phi ]!]_{i}}}

    ;

  • [[μZ.ϕ]]i=⋂{T⊆S∣[[ϕ]]i[Z:=T]⊆T}{displaystyle [![mu Z.phi ]!]_{i}=bigcap {Tsubseteq Smid [![phi ]!]_{i[Z:=T]}subseteq T}}

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

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

:

The interpretations of

[a]ϕ{displaystyle [a]phi }

and

⟨a⟩ϕ{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]

  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. ^ a b Bradfield and Stirling, p. 731
  8. ^ Bradfield and Stirling, p. 6
  9. ^ a b 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: 250–259. doi:10.1145/73560.73582. ISBN 0897912527.

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]