Compositionality of Hennessy-Milner logic by structural operational semantics

W.J. Fokkink; R.J. van Glabbeek; P. de Wind

doi:10.1016/j.tcs.2005.11.035

Compositionality of Hennessy-Milner logic by structural operational semantics

W.J. Fokkink, R.J. van Glabbeek, P. de Wind

Research output: Contribution to Journal › Article › Academic › peer-review

Abstract

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 language	English
Pages (from-to)	421-440
Journal	Theoretical Computer Science
Volume	354
Issue number	3
DOIs	https://doi.org/10.1016/j.tcs.2005.11.035
Publication status	Published - 2006

Bibliographical note

DBLP:journals/tcs/FokkinkGW06

Access to Document

10.1016/j.tcs.2005.11.035

Persistent URL (handle)

Copy link address

Cite this

@article{14f97d5dec78485d91de53e0343533c2,

title = "Compositionality of Hennessy-Milner logic by structural operational semantics",

abstract = "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.",

author = "W.J. Fokkink and {van Glabbeek}, R.J. and {de Wind}, P.",

note = "DBLP:journals/tcs/FokkinkGW06 ",

year = "2006",

doi = "10.1016/j.tcs.2005.11.035",

language = "English",

volume = "354",

pages = "421--440",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier",

number = "3",

}

TY - JOUR

T1 - Compositionality of Hennessy-Milner logic by structural operational semantics

AU - Fokkink, W.J.

AU - van Glabbeek, R.J.

AU - de Wind, P.

N1 - DBLP:journals/tcs/FokkinkGW06

PY - 2006

Y1 - 2006

N2 - 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.

AB - 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.

U2 - 10.1016/j.tcs.2005.11.035

DO - 10.1016/j.tcs.2005.11.035

M3 - Article

SN - 0304-3975

VL - 354

SP - 421

EP - 440

JO - Theoretical Computer Science

JF - Theoretical Computer Science

IS - 3

ER -

Compositionality of Hennessy-Milner logic by structural operational semantics

Abstract

Bibliographical note

Access to Document

Persistent URL (handle)

Fingerprint

Cite this