The Hennessy-Milner logic is a modal logic in computer science. It is used to specify properties of a labeled transition system, 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).
Syntax
A formula is defined by the following BNF grammar for L some set of actions:
![\Phi ::= tt \,\,\, | \,\,\,ff\,\,\, | \,\,\,\Phi_1 \land \Phi_2 \,\,\, | \,\,\,\Phi_1 \lor \Phi_2\,\,\, | \,\,\,[L] \Phi\,\,\, | \,\,\, \langle L \rangle \Phi](http://wpcontent.answers.com/math/b/2/5/b25c8e6343e365c749f702e4c033ec95.png)
That is, a formula can be
- constant truth
- always true
- constant false
- always false
- formula conjunction
- formula disjunction
![\scriptstyle{[L]\Phi}](http://wpcontent.answers.com/math/4/f/4/4f4e55a92dc7927766519463a446210b.png)
formula - for all L-derivatives, Φ must hold
formula - for some L-derivative, Φ must hold
 |
This mathematical logic-related article is a stub. You can help Wikipedia by expanding it. |
 |
This computer science article is a stub. You can help Wikipedia by expanding it. |
This entry is from Wikipedia, the leading user-contributed encyclopedia. It may not have been reviewed by professional editors (see full disclaimer)
