Precongruence formats with lookahead through modal decomposition

Wan Fokkink; Rob J. Van Glabbeek

doi:10.4230/LIPIcs.CSL.2017.25

Precongruence formats with lookahead through modal decomposition

Wan Fokkink, Rob J. Van Glabbeek

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

Abstract

Bloom, Fokkink & van Glabbeek (2004) presented a method to decompose formulas from Hennessy-Milner logic with regard to a structural operational semantics specification. A term in the corresponding process algebra satisfies a Hennessy-Milner formula if and only if its subterms satisfy certain formulas, obtained by decomposing the original formula. They used this decomposition method to derive congruence formats in the realm of structural operational semantics. In this paper it is shown how this framework can be extended to specifications that include bounded lookahead in their premises. This extension is used in the derivation of a congruence format for the partial trace preorder.

Original language	English
Title of host publication	Computer Science Logic 2017, CSL 2017
Publisher	Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Volume	82
ISBN (Electronic)	9783959770453
DOIs	https://doi.org/10.4230/LIPIcs.CSL.2017.25
Publication status	Published - 1 Aug 2017
Event	26th Annual EACSL Conference on Computer Science Logic, CSL 2017 - Stockholm, Sweden Duration: 20 Aug 2017 → 24 Aug 2017

Conference

Conference	26th Annual EACSL Conference on Computer Science Logic, CSL 2017
Country/Territory	Sweden
City	Stockholm
Period	20/08/17 → 24/08/17

Keywords

Compositionality
Congruence
Lookahead
Modal Decomposition
Modal Logic
Structural Operational Semantics

Access to Document

10.4230/LIPIcs.CSL.2017.25

Cite this

@inproceedings{c906cc4324094def8ff0793581d2ec12,

title = "Precongruence formats with lookahead through modal decomposition",

abstract = "Bloom, Fokkink & van Glabbeek (2004) presented a method to decompose formulas from Hennessy-Milner logic with regard to a structural operational semantics specification. A term in the corresponding process algebra satisfies a Hennessy-Milner formula if and only if its subterms satisfy certain formulas, obtained by decomposing the original formula. They used this decomposition method to derive congruence formats in the realm of structural operational semantics. In this paper it is shown how this framework can be extended to specifications that include bounded lookahead in their premises. This extension is used in the derivation of a congruence format for the partial trace preorder.",

keywords = "Compositionality, Congruence, Lookahead, Modal Decomposition, Modal Logic, Structural Operational Semantics",

author = "Wan Fokkink and {Van Glabbeek}, {Rob J.}",

year = "2017",

month = aug,

day = "1",

doi = "10.4230/LIPIcs.CSL.2017.25",

language = "English",

volume = "82",

booktitle = "Computer Science Logic 2017, CSL 2017",

publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",

note = "26th Annual EACSL Conference on Computer Science Logic, CSL 2017 ; Conference date: 20-08-2017 Through 24-08-2017",

}

Fokkink, W & Van Glabbeek, RJ 2017, Precongruence formats with lookahead through modal decomposition. in Computer Science Logic 2017, CSL 2017. vol. 82, 25, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 26th Annual EACSL Conference on Computer Science Logic, CSL 2017, Stockholm, Sweden, 20/08/17. https://doi.org/10.4230/LIPIcs.CSL.2017.25

TY - GEN

T1 - Precongruence formats with lookahead through modal decomposition

AU - Fokkink, Wan

AU - Van Glabbeek, Rob J.

PY - 2017/8/1

Y1 - 2017/8/1

N2 - Bloom, Fokkink & van Glabbeek (2004) presented a method to decompose formulas from Hennessy-Milner logic with regard to a structural operational semantics specification. A term in the corresponding process algebra satisfies a Hennessy-Milner formula if and only if its subterms satisfy certain formulas, obtained by decomposing the original formula. They used this decomposition method to derive congruence formats in the realm of structural operational semantics. In this paper it is shown how this framework can be extended to specifications that include bounded lookahead in their premises. This extension is used in the derivation of a congruence format for the partial trace preorder.

AB - Bloom, Fokkink & van Glabbeek (2004) presented a method to decompose formulas from Hennessy-Milner logic with regard to a structural operational semantics specification. A term in the corresponding process algebra satisfies a Hennessy-Milner formula if and only if its subterms satisfy certain formulas, obtained by decomposing the original formula. They used this decomposition method to derive congruence formats in the realm of structural operational semantics. In this paper it is shown how this framework can be extended to specifications that include bounded lookahead in their premises. This extension is used in the derivation of a congruence format for the partial trace preorder.

KW - Compositionality

KW - Congruence

KW - Lookahead

KW - Modal Decomposition

KW - Modal Logic

KW - Structural Operational Semantics

UR - http://www.scopus.com/inward/record.url?scp=85028713738&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85028713738&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.CSL.2017.25

DO - 10.4230/LIPIcs.CSL.2017.25

M3 - Conference contribution

AN - SCOPUS:85028713738

VL - 82

BT - Computer Science Logic 2017, CSL 2017

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

T2 - 26th Annual EACSL Conference on Computer Science Logic, CSL 2017

Y2 - 20 August 2017 through 24 August 2017

ER -

Precongruence formats with lookahead through modal decomposition

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this