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
editA formula is defined by the following BNF grammar for Act some set of actions:
That is, a formula can be
- constant truth
- always true
- constant false
- always false
- formula conjunction
- formula disjunction
formula
- for all Act-derivatives, Φ must hold
formula
- for some Act-derivative, Φ must hold
Formal semantics
editLet be a labeled transition system, and let
be the set of HML formulae. The satisfiabilityrelation
relates states of the LTSto the formulae they satisfy, and is defined as the smallest relation such that, for all states
and formulae
,
,
- there is no state
for which
,
- if there exists a state
such that
and
, then
,
- if for all
such that
it holds that
, then
,
- if
, then
,
- if
, then
,
- if
and
, then
.
See also
edit- The modal μ-calculus, which extends HML with fixed point operators
- Dynamic logic, a multimodal logic with infinitely many modalities
References
edit- ^ Hennessy, Matthew; Milner, Robin (1980-07-14). "On observing nondeterminism and concurrency". Automata, Languages and Programming. Lecture Notes in Computer Science. Vol. 85. Springer, Berlin, Heidelberg. pp. 299–309. doi:10.1007/3-540-10003-2_79. ISBN 978-3540100034.
- ^ Holmström, Sören (1990). "Hennessy-Milner Logic with recursion as a specification language, and a refinement calculus based on it". Specification and Verification of Concurrent Systems. Workshops in Computing. pp. 294–330. doi:10.1007/978-1-4471-3534-0_15. ISBN 978-3-540-19581-8.
Sources
edit- 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.