Top Qs
Timeline
Chat
Perspective

Hennessy–Milner logic

From Wikipedia, the free encyclopedia

Remove ads

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.

Remove ads

Syntax

Summarize
Perspective

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
Remove ads

Formal semantics

Let be a labeled transition system (LTS), 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 .
Remove ads

See also

References

Loading content...

Sources

Loading content...
Loading related searches...

Wikiwand - on

Seamless Wikipedia browsing. On steroids.

Remove ads