Hennessy–Milner logic

In computer science, Hennessy–Milner logic (HML) is a dynamic logic used to specify properties of a labeled transition system (LTS), a structure similar to an automaton. It was introduced in 1980 by Matthew Hennessy and Robin Milner in their paper "On observing nondeterminism and concurrency"[1] (ICALP).

Another variant of the HML involves the use of recursion to extend the expressibility of the logic, and is commonly referred to as 'Hennessy-Milner Logic with recursion'.[2] Recursion is enabled with the use of maximum and minimum fixed points.

Syntax

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

${\displaystyle \Phi$ ::={\textit {tt}}\,\,\,|\,\,\,{\textit {ff}}\,\,\,|\,\,\,\Phi _{1}\land \Phi _{2}\,\,\,|\,\,\,\Phi _{1}\lor \Phi _{2}\,\,\,|\,\,\,[Act]\Phi \,\,\,|\,\,\,\langle Act\rangle \Phi }

That is, a formula can be

constant truth ${\displaystyle {\textit {tt}}}$

always true

constant false ${\displaystyle {\textit {ff}}}$

always false

formula conjunction

formula disjunction

${\displaystyle \scriptstyle {[Act]\Phi }}$ formula

for all Act-derivatives, Φ must hold

${\displaystyle \scriptstyle {\langle Act\rangle \Phi }}$ formula

for some Act-derivative, Φ must hold

Formal semantics

Let ${\displaystyle L=(S,{\mathsf {Act}},\rightarrow )}$ be a labeled transition system, and let ${\displaystyle {\mathsf {HML}}}$ be the set of HML formulae. The satisfiability relation ${\displaystyle {}\models {}\subseteq (S\times {\mathsf {HML}})}$ relates states of the LTS to the formulae they satisfy, and is defined as the smallest relation such that, for all states ${\displaystyle s\in S}$ and formulae ${\displaystyle \phi ,\phi _{1},\phi _{2}\in {\mathsf {HML}}}$,

• ${\displaystyle s\models {\textit {tt}}}$,
• if there exists a state ${\displaystyle s'\in S}$ such that ${\displaystyle s{\xrightarrow {a}}s'}$ and ${\displaystyle s'\models \phi }$, then ${\displaystyle s\models \langle a\rangle \phi }$,
• if for all ${\displaystyle s'\in S}$ such that ${\displaystyle s{\xrightarrow {a}}s'}$ it holds that ${\displaystyle s'\models \phi }$, then ${\displaystyle s\models [a]\phi }$,
• if ${\displaystyle s\models \phi _{1}}$, then ${\displaystyle s\models \phi _{1}\lor \phi _{2}}$,
• if ${\displaystyle s\models \phi _{2}}$, then ${\displaystyle s\models \phi _{1}\lor \phi _{2}}$,
• if ${\displaystyle s\models \phi _{1}}$ and ${\displaystyle s\models \phi _{2}}$, then ${\displaystyle s\models \phi _{1}\land \phi _{2}}$.

See also

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

References

1. Hennessy, Matthew; Milner, Robin (1980-07-14). On observing nondeterminism and concurrency. Automata, Languages and Programming. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg. pp. 299–309. doi:10.1007/3-540-10003-2_79. ISBN 978-3540100034.
2. Holmström, Sören (1990). "Hennessy-Milner Logic with Recursion as a Specification Language, and a Refinement Calculus based on It". Proceedings of the BCS-FACS Workshop on Specification and Verification of Concurrent Systems: 294–330.

Sources

• Colin P. Stirling (2001). Modal and temporal properties of processes. Springer. pp. 32–39. ISBN 978-0-387-98717-0.
• 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.