# 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}}$.