Compositionality of Hennessy–Milner logic by structural operational semantics

Wan Fokkink; Rob van Glabbeek; Paulien de Wind

doi:10.1016/j.tcs.2005.11.035

Compositionality of Hennessy–Milner logic by structural operational semantics

Wan Fokkink, Rob van Glabbeek, Paulien de Wind

Research output: Contribution to journal › Article › 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
Number of pages	20
Journal	Theoretical Computer Science
Volume	354
Issue number	3
Early online date	19 Dec 2005
DOIs	https://doi.org/10.1016/j.tcs.2005.11.035
Publication status	Published - 4 Apr 2006

Keywords / Materials (for Non-textual outputs)

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

Access to Document

10.1016/j.tcs.2005.11.035Licence: All Rights Reserved

https://www.sciencedirect.com/science/article/pii/S0304397505008819Licence: All Rights Reserved

Cite this

@article{0e8ac0ea8a9d430ebfa273ca1252398f,

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

keywords = "Structural operational semantics, Modal logic, Compositional proof system, Congruence, ntyft/ntyxt format",

author = "Wan Fokkink and {van Glabbeek}, Rob and Wind, {Paulien de}",

note = "Foundations of Computation Theory (FCT 2003)",

year = "2006",

month = apr,

day = "4",

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, Wan

AU - van Glabbeek, Rob

AU - Wind, Paulien de

N1 - Foundations of Computation Theory (FCT 2003)

PY - 2006/4/4

Y1 - 2006/4/4

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.

KW - Structural operational semantics

KW - Modal logic

KW - Compositional proof system

KW - Congruence

KW - ntyft/ntyxt format

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

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Cite this