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
and
are formulas, then
is a formula;
* if
is a formula, then
is a formula;
* if
is a formula and
is an action, then
is a formula; (pronounced either:
box
or after
necessarily
)
* if
is a formula and
a variable, then
is a formula, provided that every free occurrence of
in
occurs positively, i.e. within the scope of an even number of negations.
(The notions of free and bound variables are as usual, where
is the only binding operator.)
Given the above definitions, we can enrich the syntax with:
*
meaning
*
(pronounced either:
diamond
or after
possibly
) meaning
*
means