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"{{Cite book|last1=Hennessy|first1=Matthew|last2=Milner|first2=Robin|title=Automata, Languages and Programming |chapter=On observing nondeterminism and concurrency |date=1980-07-14|series=Lecture Notes in Computer Science|volume=85 |language=en|publisher=Springer, Berlin, Heidelberg|pages=299–309|doi=10.1007/3-540-10003-2_79|isbn=978-3540100034}} (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'.{{cite book|last=Holmström|first=Sören|title=Specification and Verification of Concurrent Systems |chapter=Hennessy-Milner Logic with recursion as a specification language, and a refinement calculus based on it |series=Workshops in Computing |year=1990|pages=294–330|doi=10.1007/978-1-4471-3534-0_15 |isbn=978-3-540-19581-8 }} 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 ::= \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 \textit{tt}: always true

; constant false \textit{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, \mathsf{Act}, \rightarrow) be a labeled transition system (LTS), and let

\mathsf{HML} be the set of HML formulae. The satisfiability

relation {} \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 s \in S

and formulae \phi, \phi_1, \phi_2 \in \mathsf{HML},

  • s \models \textit{tt} ,
  • there is no state s \in S for which s \models \textit{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

References

Sources

  • {{cite book|author=Colin P. Stirling|title=Modal and temporal properties of processes|url=https://archive.org/details/modaltemporalpro00stir|url-access=limited|year=2001|publisher=Springer|isbn=978-0-387-98717-0|pages=[https://archive.org/details/modaltemporalpro00stir/page/n42 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.

{{DEFAULTSORT:Hennessy-Milner logic}}

Category:Concurrency (computer science)

Category:Formal specification

Category:Modal logic

Category:Logic in computer science

{{comp-sci-stub}}