Compositionality of Hennessy–Milner logic by structural operational semantics

Wan Fokkink, Rob van Glabbeek, Paulien de Wind

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

This paper presents a method for the decomposition of HML formulas. It can be used to decide whether a process algebra term satisfies a HML formula, by checking whether subterms satisfy certain formulas, obtained by decomposing the original formula. The method uses the structural operational semantics of the process algebra. The main contribution of this paper is the extension of an earlier decomposition method for the De Simone format from the Ph.D. thesis of Larsen in 1986, to more general formats.
Original languageEnglish
Pages (from-to)421-440
Number of pages20
JournalTheoretical Computer Science
Issue number3
Early online date19 Dec 2005
Publication statusPublished - 4 Apr 2006

Keywords / Materials (for Non-textual outputs)

  • Structural operational semantics
  • Modal logic
  • Compositional proof system
  • Congruence
  • ntyft/ntyxt format


Dive into the research topics of 'Compositionality of Hennessy–Milner logic by structural operational semantics'. Together they form a unique fingerprint.

Cite this