[{"@context":"http:\/\/schema.org\/","@type":"BlogPosting","@id":"https:\/\/wiki.edu.vn\/en\/wiki\/modal-%ce%bc-calculus-wikipedia\/#BlogPosting","mainEntityOfPage":"https:\/\/wiki.edu.vn\/en\/wiki\/modal-%ce%bc-calculus-wikipedia\/","headline":"Modal \u03bc-calculus – Wikipedia","name":"Modal \u03bc-calculus – Wikipedia","description":"before-content-x4 From Wikipedia, the free encyclopedia after-content-x4 In theoretical computer science, the modal \u03bc-calculus (L\u03bc, L\u03bc, sometimes just \u03bc-calculus, although","datePublished":"2022-01-12","dateModified":"2022-01-12","author":{"@type":"Person","@id":"https:\/\/wiki.edu.vn\/en\/wiki\/author\/lordneo\/#Person","name":"lordneo","url":"https:\/\/wiki.edu.vn\/en\/wiki\/author\/lordneo\/","image":{"@type":"ImageObject","@id":"https:\/\/secure.gravatar.com\/avatar\/44a4cee54c4c053e967fe3e7d054edd4?s=96&d=mm&r=g","url":"https:\/\/secure.gravatar.com\/avatar\/44a4cee54c4c053e967fe3e7d054edd4?s=96&d=mm&r=g","height":96,"width":96}},"publisher":{"@type":"Organization","name":"Enzyklop\u00e4die","logo":{"@type":"ImageObject","@id":"https:\/\/wiki.edu.vn\/wiki4\/wp-content\/uploads\/2023\/08\/download.jpg","url":"https:\/\/wiki.edu.vn\/wiki4\/wp-content\/uploads\/2023\/08\/download.jpg","width":600,"height":60}},"image":{"@type":"ImageObject","@id":"https:\/\/wikimedia.org\/api\/rest_v1\/media\/math\/render\/svg\/c15bbbb971240cf328aba572178f091684585468","url":"https:\/\/wikimedia.org\/api\/rest_v1\/media\/math\/render\/svg\/c15bbbb971240cf328aba572178f091684585468","height":"","width":""},"url":"https:\/\/wiki.edu.vn\/en\/wiki\/modal-%ce%bc-calculus-wikipedia\/","wordCount":5245,"articleBody":"     (adsbygoogle = window.adsbygoogle || []).push({});before-content-x4From Wikipedia, the free encyclopedia       (adsbygoogle = window.adsbygoogle || []).push({});after-content-x4In theoretical computer science, the modal \u03bc-calculus (L\u03bc, L\u03bc, sometimes just \u03bc-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 \u03bc and the greatest fixed point operator \u03bd, thus a fixed-point logic.The (propositional, modal) \u03bc-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 \u03bc-calculus, including CTL* and its widely used fragments\u2014linear temporal logic and computational tree logic.[3]       (adsbygoogle = window.adsbygoogle || []).push({});after-content-x4An 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 \u03bc-calculus is over the lattice of a power set algebra.[4] The game semantics of \u03bc-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) \u03bc-calculus is defined as follows:(The notions of free and bound variables are as usual, where        (adsbygoogle = window.adsbygoogle || []).push({});after-content-x4\u03bd{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 \u03bcZ.\u03d5{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 \u03d5{displaystyle phi } where the “minimization” (and respectively “maximization”) are in the variable Z{displaystyle Z}, much like in lambda calculus \u03bbZ.\u03d5{displaystyle lambda Z.phi } is a function with formula \u03d5{displaystyle phi } in bound variable Z{displaystyle Z};[6]  see the denotational semantics below for details.Table of ContentsDenotational semantics[edit]Examples[edit]Decision problems[edit]See also[edit]References[edit]External links[edit]Denotational semantics[edit]Models of (propositional) \u03bc-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 \u03bc{displaystyle mu }-calculus, [[\u22c5]]i:\u03d5\u21922S{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:[[\u03d5\u2228\u03c8]]i=[[\u03d5]]i\u222a[[\u03c8]]i{displaystyle [![phi vee psi ]!]_{i}=[![phi ]!]_{i}cup [![psi ]!]_{i}};[[\u27e8a\u27e9\u03d5]]i={s\u2208S\u2223\u2203t\u2208S,(s,t)\u2208Ra\u2227t\u2208[[\u03d5]]i}{displaystyle [![langle arangle phi ]!]_{i}={sin Smid exists tin S,(s,t)in R_{a}wedge tin [![phi ]!]_{i}}};[[\u03bcZ.\u03d5]]i=\u22c2{T\u2286S\u2223[[\u03d5]]i[Z:=T]\u2286T}{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]\u03d5{displaystyle [a]phi } and  \u27e8a\u27e9\u03d5{displaystyle langle arangle phi } are in fact the “classical” ones from dynamic logic. Additionally, the operator \u03bc{displaystyle mu } can be interpreted as liveness (“something good eventually happens”) and \u03bd{displaystyle nu } as safety (“nothing bad ever happens”) in Leslie Lamport’s informal classification.[7]Examples[edit]Decision problems[edit]Satisfiability of a modal \u03bc-calculus formula is EXPTIME-complete.[10] Like for linear temporal logic,[11] the model checking, satisfiability and validity problems of linear modal \u03bc-calculus are PSPACE-complete.[12]See also[edit]^ Scott, Dana; Bakker, Jacobus (1969). “A theory of programs”. Unpublished manuscript.^ Kozen, Dexter (1982). “Results on the propositional \u03bc-calculus”. Automata, Languages and Programming. ICALP. Vol.\u00a0140. pp.\u00a0348\u2013359. doi:10.1007\/BFb0012782. ISBN\u00a0978-3-540-11576-2.^ Clarke p.108, Theorem 6; Emerson p.\u00a0196^ Arnold and Niwi\u0144ski, pp. viii-x and chapter 6^ Arnold and Niwi\u0144ski, pp. viii-x and chapter 4^ Arnold and Niwi\u0144ski, p. 14^ a b Bradfield and Stirling, p. 731^ Bradfield and Stirling, p. 6^ a b Erich Gr\u00e4del; 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.\u00a0159. ISBN\u00a0978-3-540-00428-8.^ Klaus Schneider (2004). Verification of reactive systems: formal methods and algorithms. Springer. p.\u00a0521. ISBN\u00a0978-3-540-00296-3.^ Sistla, A. P.; Clarke, E. M. (1985-07-01). “The Complexity of Propositional Linear Temporal Logics”. J. ACM. 32 (3): 733\u2013749. doi:10.1145\/3828.3837. ISSN\u00a00004-5411.^ 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\u2013259. doi:10.1145\/73560.73582. ISBN\u00a00897912527.References[edit]Clarke, Edmund M. Jr.; Orna Grumberg; Doron A. Peled (1999). Model Checking. Cambridge, Massachusetts, USA: MIT press. ISBN\u00a00-262-03270-8., chapter 7, Model checking for the \u03bc-calculus, pp.\u00a097\u2013108Stirling, Colin. (2001). Modal and Temporal Properties of Processes. New York, Berlin, Heidelberg: Springer Verlag. ISBN\u00a00-387-98717-7., chapter 5, Modal \u03bc-calculus, pp.\u00a0103\u2013128Andr\u00e9 Arnold; Damian Niwi\u0144ski (2001). Rudiments of \u03bc-Calculus. Elsevier. ISBN\u00a0978-0-444-50620-7., chapter 6, The \u03bc-calculus over powerset algebras, pp.\u00a0141\u2013153 is about the modal \u03bc-calculusYde Venema (2008) Lectures on the Modal \u03bc-calculus;  was presented at The 18th European Summer School in Logic, Language and InformationBradfield, Julian & Stirling, Colin (2006). “Modal mu-calculi”.  In P. Blackburn; J. van Benthem & F. Wolter (eds.). The Handbook of Modal Logic. Elsevier. pp.\u00a0721\u2013756.Emerson, E. Allen (1996). “Model Checking and the Mu-calculus”. Descriptive Complexity and Finite Models. American Mathematical Society. pp.\u00a0185\u2013214. ISBN\u00a00-8218-0517-7.Kozen, Dexter (1983). “Results on the Propositional \u03bc-Calculus”. Theoretical Computer Science. 27 (3): 333\u2013354. doi:10.1016\/0304-3975(82)90125-6.External links[edit]     (adsbygoogle = window.adsbygoogle || []).push({});after-content-x4"},{"@context":"http:\/\/schema.org\/","@type":"BreadcrumbList","itemListElement":[{"@type":"ListItem","position":1,"item":{"@id":"https:\/\/wiki.edu.vn\/en\/wiki\/#breadcrumbitem","name":"Enzyklop\u00e4die"}},{"@type":"ListItem","position":2,"item":{"@id":"https:\/\/wiki.edu.vn\/en\/wiki\/modal-%ce%bc-calculus-wikipedia\/#breadcrumbitem","name":"Modal \u03bc-calculus – Wikipedia"}}]}]