HOME

TheInfoList



OR:

In
theoretical computer science Theoretical computer science (TCS) is a subset of general computer science and mathematics that focuses on mathematical aspects of computer science such as the theory of computation, lambda calculus, and type theory. It is difficult to circumsc ...
, the modal μ-calculus (Lμ, Lμ, sometimes just μ-calculus, although this can have a more general meaning) is an extension of
propositional In logic and linguistics, a proposition is the meaning of a declarative sentence. In philosophy, "meaning" is understood to be a non-linguistic entity which is shared by all sentences with the same meaning. Equivalently, a proposition is the no ...
modal logic (with many modalities) by adding the
least fixed point In order theory, a branch of mathematics, the least fixed point (lfp or LFP, sometimes also smallest fixed point) of a function from a partially ordered set to itself is the fixed point which is less than each other fixed point, according to the ...
operator μ and the
greatest fixed point In order theory, a branch of mathematics, the least fixed point (lfp or LFP, sometimes also smallest fixed point) of a function from a partially ordered set to itself is the fixed point which is less than each other fixed point, according to the ...
operator ν, thus a
fixed-point logic In mathematical logic, fixed-point logics are extensions of classical predicate logic that have been introduced to express recursion. Their development has been motivated by descriptive complexity theory and their relationship to database query l ...
. The (propositional, modal) μ-calculus originates with
Dana Scott Dana Stewart Scott (born October 11, 1932) is an American logician who is the emeritus Hillman University Professor of Computer Science, Philosophy, and Mathematical Logic at Carnegie Mellon University; he is now retired and lives in Berkeley, C ...
and
Jaco de Bakker Jacobus Willem (Jaco) de Bakker (7 March 1939 – 13 December 2012) was a Dutch theoretical computer scientist and professor at the Vrije Universiteit Amsterdam. Biography De Bakker studied mathematics at the Vrije Universiteit and the Univer ...
, and was further developed by Dexter Kozen into the version most used nowadays. It is used to describe properties of labelled transition systems and for
verifying Verification and validation (also abbreviated as V&V) are independent procedures that are used together for checking that a product, service, or system meets requirements and specifications and that it fulfills its intended purpose. These are ...
these properties. Many
temporal logic In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time (for example, "I am ''always'' hungry", "I will ''eventually'' be hungry", or "I will be hungry ''until'' I ...
s can be encoded in the μ-calculus, including CTL* and its widely used fragments—
linear temporal logic In logic, linear temporal logic or linear-time temporal logic (LTL) is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths, e.g., a condition will eventually be true, a condition will ...
and computational tree logic. An algebraic view is to see it as an
algebra Algebra () is one of the areas of mathematics, broad areas of mathematics. Roughly speaking, algebra is the study of mathematical symbols and the rules for manipulating these symbols in formulas; it is a unifying thread of almost all of mathem ...
of
monotonic function In mathematics, a monotonic function (or monotone function) is a function between ordered sets that preserves or reverses the given order. This concept first arose in calculus, and was later generalized to the more abstract setting of ord ...
s over a
complete lattice In mathematics, a complete lattice is a partially ordered set in which ''all'' subsets have both a supremum (join) and an infimum (meet). A lattice which satisfies at least one of these properties is known as a ''conditionally complete lattice.'' S ...
, with operators consisting of
functional composition In mathematics, function composition is an operation that takes two functions and , and produces a function such that . In this operation, the function is applied to the result of applying the function to . That is, the functions and ...
plus the least and greatest fixed point operators; from this viewpoint, the modal μ-calculus is over the lattice of a power set algebra. The
game semantics Game semantics (german: dialogische Logik, translated as '' dialogical logic'') is an approach to formal semantics that grounds the concepts of truth or validity on game-theoretic concepts, such as the existence of a winning strategy for a player ...
of μ-calculus is related to
two-player game A two-player game is a multiplayer game that is played by precisely two players. This is distinct from a solitaire game, which is played by only one player. Examples The following are some examples of two-player games. This list is not intended t ...
s with
perfect information In economics, perfect information (sometimes referred to as "no hidden information") is a feature of perfect competition. With perfect information in a market, all consumers and producers have complete and instantaneous knowledge of all market pr ...
, particularly infinite
parity game A parity game is played on a colored directed graph, where each node has been colored by a priority – one of (usually) finitely many natural numbers. Two players, 0 and 1, move a (single, shared) token along the edges of the graph. The owne ...
s.


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 \phi and \psi are formulas, then \phi \wedge \psi is a formula; * if \phi is a formula, then \neg \phi is a formula; * if \phi is a formula and a is an action, then \phi is a formula; (pronounced either: a box \phi or after a necessarily \phi) * if \phi is a formula and Z a variable, then \nu Z. \phi is a formula, provided that every free occurrence of Z in \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 \nu is the only binding operator.) Given the above definitions, we can enrich the syntax with: * \phi \lor \psi meaning \neg (\neg \phi \land \neg \psi) * \langle a \rangle \phi (pronounced either: a diamond \phi or after a possibly \phi) meaning \neg \neg \phi * \mu Z. \phi means \neg \nu Z. \neg \phi :=\neg Z/math>, where \phi :=\neg Z/math> means substituting \neg Z for Z in all free occurrences of Z in \phi . The first two formulas are the familiar ones from the classical
propositional calculus Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations ...
and respectively the minimal
multimodal logic A multimodal logic is a modal logic that has more than one primitive modal operator. They find substantial applications in theoretical computer science. Overview A modal logic with ''n'' primitive unary modal operators \Box_i, i\in \ is called an ...
K. The notation \mu Z. \phi (and its dual) are inspired from the
lambda calculus Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation t ...
; the intent is to denote the least (and respectively greatest) fixed point of the expression \phi where the "minimization" (and respectively "maximization") are in the variable Z, much like in lambda calculus \lambda Z. \phi is a function with formula \phi in
bound variable In mathematics, and in other disciplines involving formal languages, including mathematical logic and computer science, a free variable is a notation (symbol) that specifies places in an expression where substitution may take place and is n ...
Z; see the denotational semantics below for details.


Denotational semantics

Models of (propositional) μ-calculus are given as labelled transition systems (S, R, V) where: * S is a set of states; * R maps to each label a a binary relation on S; * V : P \to 2^S, maps each proposition p \in P to the set of states where the proposition is true. Given a labelled transition system (S, R, V) and an interpretation i of the variables Z of the \mu-calculus, ![\cdot!">cdot.html" ;"title="![\cdot">![\cdot!i:\phi \to 2^S, is the function defined by the following rules: * [\![p]\!]_i = V(p); * [\![Z]\!]_i = i(Z); * [\![\phi \wedge \psi]\!]_i = [\![\phi]\!]_i \cap [\![\psi]\!]_i; * [\![\neg \phi]\!]_i = S \smallsetminus [\![\phi]\!]_i; * \phi">![ \phi!">\phi">![ \phi!i = \; * [\![\nu Z. \phi]\!]_i = \bigcup \, where i[Z := T] maps Z to T while preserving the mappings of i everywhere else. By duality, the interpretation of the other basic formulas is: * ![\phi \vee \psi!">phi_\vee_\psi.html" ;"title="![\phi \vee \psi">![\phi \vee \psi!i = [\![\phi]\!]_i \cup [\![\psi]\!]_i; * [\![\langle a \rangle \phi]\!]_i = \; * [\![\mu Z. \phi]\!]_i = \bigcap \ Less formally, this means that, for a given transition system (S, R, V): * p holds in the set of states V(p); * \phi \wedge \psi holds in every state where \phi and \psi both hold; * \neg \phi holds in every state where \phi does not hold. * \phi holds in a state s if every a-transition leading out of s leads to a state where \phi holds. * \langle a\rangle \phi holds in a state s if there exists a-transition leading out of s that leads to a state where \phi holds. * \nu Z.\phi holds in any state in any set T such that, when the variable Z is set to T, then \phi holds for all of T. (From the Knaster–Tarski theorem it follows that ![\nu Z.\phi!">nu_Z.\phi.html" ;"title="![\nu Z.\phi">![\nu Z.\phi!i is the
greatest fixed point In order theory, a branch of mathematics, the least fixed point (lfp or LFP, sometimes also smallest fixed point) of a function from a partially ordered set to itself is the fixed point which is less than each other fixed point, according to the ...
of [\![\phi]\!]_, and [\![\mu Z. \phi]\!]_i its
least fixed point In order theory, a branch of mathematics, the least fixed point (lfp or LFP, sometimes also smallest fixed point) of a function from a partially ordered set to itself is the fixed point which is less than each other fixed point, according to the ...
.) The interpretations of \phi and \langle a\rangle \phi are in fact the "classical" ones from dynamic logic. Additionally, the operator \mu can be interpreted as
liveness Properties of an execution of a computer program —particularly for concurrent and distributed systems— have long been formulated by giving ''safety properties'' ("bad things don't happen") and ''liveness properties'' ("good things do happen"). ...
("something good eventually happens") and \nu as
safety Safety is the state of being "safe", the condition of being protected from harm or other danger. Safety can also refer to the control of recognized hazards in order to achieve an acceptable level of risk. Meanings There are two slightly di ...
("nothing bad ever happens") in
Leslie Lamport Leslie B. Lamport (born February 7, 1941 in Brooklyn) is an American computer scientist and mathematician. Lamport is best known for his seminal work in distributed systems, and as the initial developer of the document preparation system LaTeX and ...
's informal classification.Bradfield and Stirling, p. 731


Examples

* \nu Z.\phi \wedge is interpreted as "\phi is true along every ''a''-path". The idea is that "\phi is true along every ''a''-path" can be defined axiomatically as that (weakest) sentence Z which implies \phi and which remains true after processing any ''a''-label. * \mu Z.\phi \vee \langle a \rangle Z is interpreted as the existence of a path along ''a''-transitions to a state where \phi holds. * The property of a state being
deadlock In concurrent computing, deadlock is any situation in which no member of some group of entities can proceed because each waits for another member, including itself, to take action, such as sending a message or, more commonly, releasing a lo ...
-free, meaning no path from that state reaches a dead end, is expressed by the formula \nu Z.\left (\bigvee_\langle a\rangle\top\wedge \bigwedge_ \right)


Decision problems

Satisfiability In mathematical logic, a formula is ''satisfiable'' if it is true under some assignment of values to its variables. For example, the formula x+3=y is satisfiable because it is true when x=3 and y=6, while the formula x+1=x is not satisfiable over ...
of a modal μ-calculus formula is EXPTIME-complete. Like for linear temporal logic, the
model checking In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software system ...
, satisfiability and validity problems of linear modal μ-calculus are
PSPACE-complete In computational complexity theory, a decision problem is PSPACE-complete if it can be solved using an amount of memory that is polynomial in the input length ( polynomial space) and if every other problem that can be solved in polynomial space can ...
.


See also

*
Finite model theory Finite model theory is a subarea of model theory. Model theory is the branch of logic which deals with the relation between a formal language (syntax) and its interpretations (semantics). Finite model theory is a restriction of model theory to inte ...
* Alternation-free modal μ-calculus


Notes


References

*, chapter 7, Model checking for the μ-calculus, pp. 97–108 *, chapter 5, Modal μ-calculus, pp. 103–128 * , 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 * * *


External links

* Sophie Pinchinat
Logic, Automata & Games
video recording of a lecture at ANU Logic Summer School '09 {{DEFAULTSORT:Modal mu-calculus Modal logic Model checking