Hennessy–Milner logic explained

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:

\Phi :: = it{tt} | it{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

it{tt} : always true

constant false

it{ff} : always false

formula conjunction

formula disjunction

\scriptstyle{[Act]\Phi} formula : for all Act-derivatives, Φ must hold\scriptstyle{\langle Act \rangle \Phi} formula : for some Act-derivative, Φ must hold

Formal semantics

Let

L = (S, Act , → ) be a labeled transition system, and letHML be the set of HML formulae. The satisfiabilityrelation {} \models {} \subseteq (S x HML ) relates states of the LTSto the formulae they satisfy, and is defined as the smallest relation such that, for all states s \in S and formulae \phi, \phi _{1,} \phi _{2} \in HML ,s \models it{tt} ,

• there is no state

s \in S for which s \models it{ff} ,

• if there exists a state

s' \in S such that s \xrightarrow{a} s' and s' \models \phi , then s \models \langle a \rangle \phi ,

• if for all

s' \in S such that s \xrightarrow{a} s' it holds that s' \models \phi , then s \models [ a ] \phi ,

• if

s \models \phi _{1} , then s \models \phi _{1} \lor \phi _{2} ,

• if

s \models \phi _{2} , then s \models \phi _{1} \lor \phi _{2} ,

• if

s \models \phi _{1} and s \models \phi _{2} , then 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. Book: Hennessy. Matthew. Milner. Robin. Automata, Languages and Programming . On observing nondeterminism and concurrency . 1980-07-14. Lecture Notes in Computer Science. 85 . en. Springer, Berlin, Heidelberg. 299–309. 10.1007/3-540-10003-2_79. 978-3540100034.
2. Book: Holmström, Sören. Specification and Verification of Concurrent Systems . Hennessy-Milner Logic with recursion as a specification language, and a refinement calculus based on it . Workshops in Computing . 1990. 294–330. 10.1007/978-1-4471-3534-0_15 . 978-3-540-19581-8 .

Sources

• Book: Colin P. Stirling. Modal and temporal properties of processes. limited. 2001. Springer. 978-0-387-98717-0. 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.