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" (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'. 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:

$\mathrm{\Phi }::=\text{<mrow data-mjx-texclass="ORD">tt</mrow>}|\text{<mrow data-mjx-texclass="ORD">ff</mrow>}|{\mathrm{\Phi }}_1\wedge {\mathrm{\Phi }}_2|{\mathrm{\Phi }}_1\vee {\mathrm{\Phi }}_2|[Act]\mathrm{\Phi }|⟨Act⟩\mathrm{\Phi }$

That is, a formula can be

constant truth $\text{<mrow data-mjx-texclass="ORD">tt</mrow>}$

always true

constant false $\text{<mrow data-mjx-texclass="ORD">ff</mrow>}$

always false

formula conjunction

formula disjunction

$[Act]\mathrm{\Phi }$ formula

for all Act-derivatives, Φ must hold

$⟨Act⟩\mathrm{\Phi }$ formula

for some Act-derivative, Φ must hold

Formal semantics

Let $L=(S,\mathsf{A}\mathsf{c}\mathsf{t},\to )$ be a labeled transition system, and let $\mathsf{H}\mathsf{M}\mathsf{L}$ be the set of HML formulae. The satisfiability relation ${\displaystyle }\models \subseteq (S\times \mathsf{H}\mathsf{M}\mathsf{L})$ relates states of the LTS to the formulae they satisfy, and is defined as the smallest relation such that, for all states $s\in S$ and formulae $\varphi ,{\varphi }_1,{\varphi }_2\in \mathsf{H}\mathsf{M}\mathsf{L}$,

• $s\models \text{<mrow data-mjx-texclass="ORD">tt</mrow>}$,
• there is no state $s\in S$ for which $s\models \text{<mrow data-mjx-texclass="ORD">ff</mrow>}$,
• if there exists a state $s^{\prime }\in S$ such that $s\stackrel{a}{\to }{s}^{\prime }$ and $s^{\prime }\models \varphi$, then $s\models ⟨a⟩\varphi$,
• if for all $s^{\prime }\in S$ such that $s\stackrel{a}{\to }{s}^{\prime }$ it holds that $s^{\prime }\models \varphi$, then $s\models [a]\varphi$,
• if $s\models {\varphi }_1$, then $s\models {\varphi }_1\vee {\varphi }_2$,
• if $s\models {\varphi }_2$, then $s\models {\varphi }_1\vee {\varphi }_2$,
• if $s\models {\varphi }_1$ and $s\models {\varphi }_2$, then $s\models {\varphi }_1\wedge {\varphi }_2$.

See also

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

Sources

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