Modal %CE%BC-calculus
Get Modal %CE%BC-calculus essential facts below. View Videos or join the Modal %CE%BC-calculus discussion. Add Modal %CE%BC-calculus to your PopFlock.com topic list for future reference or share this resource on social media.
Modal %CE%BC-calculus

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 ${\displaystyle \nu }$, 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 V 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 ${\displaystyle \phi }$ and ${\displaystyle \psi }$ are formulas, then ${\displaystyle \phi \wedge \psi }$ is a formula.
• if ${\displaystyle \phi }$ is a formula, then ${\displaystyle \neg \phi }$ is a formula;
• if ${\displaystyle \phi }$ is a formula and ${\displaystyle a}$ is an action, then ${\displaystyle [a]\phi }$ is a formula;(pronounced either: ${\displaystyle a}$ box ${\displaystyle \phi }$ or after ${\displaystyle a}$ necessarily ${\displaystyle \phi }$)
• if ${\displaystyle \phi }$ is a formula and ${\displaystyle Z}$ a variable, then ${\displaystyle \nu Z.\phi }$ is a formula, provided that every free occurrence of ${\displaystyle Z}$ in ${\displaystyle \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 ${\displaystyle \nu }$ is the only binding operator.)

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

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

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

The notation ${\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 ${\displaystyle Z}$, much like in lambda calculus ${\displaystyle \lambda Z.\phi }$ is a function with formula ${\displaystyle \phi }$ in bound variable ${\displaystyle Z}$;[6] see the denotational semantics below for details.

## Denotational semantics

Models of (propositional) ?-calculus are given as labelled transition systems ${\displaystyle (S,R,V)}$ where:

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

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

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

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

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

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

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

The interpretations of ${\displaystyle [a]\phi }$ and ${\displaystyle \langle a\rangle \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

• ${\displaystyle \nu Z.\phi \wedge [a]Z}$ is interpreted as "${\displaystyle \phi }$ is true along every a-path".[7] The idea is that "${\displaystyle \phi }$ is true along every a-path" can be defined axiomatically as that (weakest) sentence ${\displaystyle Z}$ which implies ${\displaystyle \phi }$ and which remains true after processing any a-label. [8]
• ${\displaystyle \mu Z.\phi \vee \langle a\rangle Z}$ is interpreted as the existence of a path along a-transitions to a state where ${\displaystyle \phi }$ holds.[9]
• The property of a system being deadlock-free, meaning having no states without outgoing transitions and furthermore that a path to such a state does not exist, is expressed by the formula[9]
${\displaystyle \nu Z.\left(\bigvee _{a\in A}\langle a\rangle \top \wedge \bigwedge _{a\in A}[a]Z\right)}$

## Decision problems

Satisfiability of a modal ?-calculus formula is EXPTIME-complete.[10] As for Linear Temporal Logic,[11] model checking, satisfiability and validity problems of linear modal ?-calculus are PSPACE-complete.[12]

## Notes

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. 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

• Clarke, Jr., Edmund M.; 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.