# Hennessy–Milner logic

(Redirected from Hennessy-Milner logic)

In computer science, Hennessy–Milner logic (HML) is a multimodal logic used to specify properties of a labeled transition system, 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'.[1] Recursion is enabled with the use of maximum and minimum fixed points.

## Syntax

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

$\Phi ::= tt \,\,\, | \,\,\,ff\,\,\, | \,\,\,\Phi_1 \land \Phi_2 \,\,\, | \,\,\,\Phi_1 \lor \Phi_2\,\,\, | \,\,\,[L] \Phi\,\,\, | \,\,\, \langle L \rangle \Phi$

That is, a formula can be

constant truth
always true
constant false
always false
formula conjunction
formula disjunction
$\scriptstyle{[L]\Phi}$ formula
for all L-derivatives, Φ must hold
$\scriptstyle{\langle L \rangle \Phi}$ formula
for some L-derivative, Φ must hold