Hennessy–Milner logic

A formula is defined by the following BNF grammar for Act some set of actions:

:$\backslash Phi\; ::=\; \backslash textit\{tt\}\; \backslash ,\backslash ,\backslash ,\; |\; \backslash ,\backslash ,\backslash ,\backslash textit\{ff\}\backslash ,\backslash ,\backslash ,\; |\; \backslash ,\backslash ,\backslash ,\backslash Phi\_1\; \backslash land\; \backslash Phi\_2\; \backslash ,\backslash ,\backslash ,\; |\; \backslash ,\backslash ,\backslash ,\backslash Phi\_1\; \backslash lor\; \backslash Phi\_2\backslash ,\backslash ,\backslash ,\; |\; \backslash ,\backslash ,\backslash ,[Act]\; \backslash Phi\backslash ,\backslash ,\backslash ,\; |\; \backslash ,\backslash ,\backslash ,\; \backslash langle\; Act\; \backslash rangle\; \backslash Phi$

That is, a formula can be

; constant truth $\backslash textit\{tt\}$: always true

; constant false $\backslash textit\{ff\}$: always false

; formula conjunction

; formula disjunction

; $\backslash scriptstyle\{[Act]\backslash Phi\}$ formula : for all Act-derivatives, Φ must hold

; $\backslash scriptstyle\{\backslash langle\; Act\; \backslash rangle\; \backslash Phi\}$ formula : for some Act-derivative, Φ must hold

Let $L\; =\; (S,\; \backslash mathsf\{Act\},\; \backslash rightarrow)$ be a labeled transition system (LTS), and let

$\backslash mathsf\{HML\}$ be the set of HML formulae. The satisfiability

relation $\{\}\; \backslash models\; \{\}\; \backslash subseteq\; (S\; \backslash times\; \backslash mathsf\{HML\})$ relates states of the LTS

to the formulae they satisfy, and is defined as the smallest relation such that, for all states $s\; \backslash in\; S$

and formulae $\backslash phi,\; \backslash phi\_1,\; \backslash phi\_2\; \backslash in\; \backslash mathsf\{HML\}$,

• $s\; \backslash models\; \backslash textit\{tt\}$,
• there is no state $s\; \backslash in\; S$ for which $s\; \backslash models\; \backslash textit\{ff\}$,
• if there exists a state $s\text{'}\; \backslash in\; S$ such that $s\; \backslash xrightarrow\{a\}\; s\text{'}$ and $s\text{'}\; \backslash models\; \backslash phi$, then $s\; \backslash models\; \backslash langle\; a\; \backslash rangle\; \backslash phi$,
• if for all $s\text{'}\; \backslash in\; S$ such that $s\; \backslash xrightarrow\{a\}\; s\text{'}$ it holds that $s\text{'}\; \backslash models\; \backslash phi$, then $s\; \backslash models\; [\; a\; ]\; \backslash phi$,
• if $s\; \backslash models\; \backslash phi\_1$, then $s\; \backslash models\; \backslash phi\_1\; \backslash lor\; \backslash phi\_2$,
• if $s\; \backslash models\; \backslash phi\_2$, then $s\; \backslash models\; \backslash phi\_1\; \backslash lor\; \backslash phi\_2$,
• if $s\; \backslash models\; \backslash phi\_1$ and $s\; \backslash models\; \backslash phi\_2$, then $s\; \backslash models\; \backslash phi\_1\; \backslash land\; \backslash phi\_2$.

• The modal μ-calculus, which extends HML with fixed point operators
• Dynamic logic, a multimodal logic with infinitely many modalities

• {{cite book|author=Colin P. Stirling|title=Modal and temporal properties of processes|url=https://archive.org/details/modaltemporalpro00stir|url-access=limited|year=2001|publisher=Springer|isbn=978-0-387-98717-0|pages=[https://archive.org/details/modaltemporalpro00stir/page/n42 32]–39}}
• Sören Holmström. 1988. "Hennessy-Milner Logic with Recursion as a Specification Language, and a Refinement Calculus based on It". In Proceedings of the BCS-FACS Workshop on Specification and Verification of Concurrent Systems, Charles Rattray (Ed.). Springer-Verlag, London, UK, 294–330.

{{DEFAULTSORT:Hennessy-Milner logic}}

Category:Concurrency (computer science)

Category:Formal specification

Category:Modal logic

Category:Logic in computer science

{{comp-sci-stub}}