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:

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
Let  be a labeled transition system, and let
 be the set of HML formulae. The satisfiability
relation  relates states of the LTS
to 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 
 The modal μ-calculus, which extends HML with fixed point operators
 Dynamic logic, a multimodal logic with infinitely many modalities

References

Sources
 
 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. Concurrency (computer science)
Formal specification
Modal logic
Logic in computer science