A Lean-Congruence Format for EP-Bisimilarity

Rob van Glabbeek; Peter Höfner; Weiyou Wang

doi:10.4204/EPTCS.387.6

A Lean-Congruence Format for EP-Bisimilarity

Rob van Glabbeek, Peter Höfner, Weiyou Wang

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract / Description of output

Enabling preserving bisimilarity is a refinement of strong bisimilarity that preserves safety as well as liveness properties. To define it properly, labelled transition systems needed to be upgraded with a successor relation, capturing concurrency between transitions enabled in the same state. We enrich the well-known De Simone format to handle inductive definitions of this successor relation. We then establish that ep-bisimilarity is a congruence for the operators, as well as lean congruence for recursion, for all (enriched) De Simone languages.

Original language	English
Title of host publication	Proceedings Combined 30th International Workshop on Expressiveness in Concurrency and 20th Workshop on Structural Operational Semantics (EXPRESS/SOS2023)
Editors	Claudio Antares Mezzina, Georgiana Caltais
Publisher	Open Publishing Association
Pages	59-75
Number of pages	17
Volume	387
DOIs	https://doi.org/10.4204/EPTCS.387.6
Publication status	Published - 14 Sept 2023
Event	Combined 30th International Workshop on Expressiveness in Concurrency and 20th Workshop on Structural Operational Semantics - Antwerp, Belgium Duration: 18 Sept 2023 → … https://express-sos.github.io/

Publication series

Name	Electronic Proceedings in Theoretical Computer Science
Publisher	Open Publishing Association
ISSN (Electronic)	2075-2180

Conference

Conference	Combined 30th International Workshop on Expressiveness in Concurrency and 20th Workshop on Structural Operational Semantics
Abbreviated title	EXPRESS/SOS 2023
Country/Territory	Belgium
City	Antwerp
Period	18/09/23 → …
Internet address	https://express-sos.github.io/

Access to Document

10.4204/EPTCS.387.6Licence: Creative Commons: Attribution (CC-BY)

A Lean-Congruence_VAN GLABBEEK_DOA11082023_VOR_CC BYFinal published version, 351 KBLicence: Creative Commons: Attribution (CC-BY)

https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?EXPRESS_SOS2023.6Licence: Creative Commons: Attribution (CC-BY)

Cite this

van Glabbeek, R., Höfner, P., & Wang, W. (2023). A Lean-Congruence Format for EP-Bisimilarity. In C. A. Mezzina, & G. Caltais (Eds.), Proceedings Combined 30th International Workshop on Expressiveness in Concurrency and 20th Workshop on Structural Operational Semantics (EXPRESS/SOS2023) (Vol. 387, pp. 59-75). (Electronic Proceedings in Theoretical Computer Science). Open Publishing Association. https://doi.org/10.4204/EPTCS.387.6

van Glabbeek, Rob ; Höfner, Peter ; Wang, Weiyou. / A Lean-Congruence Format for EP-Bisimilarity. Proceedings Combined 30th International Workshop on Expressiveness in Concurrency and 20th Workshop on Structural Operational Semantics (EXPRESS/SOS2023). editor / Claudio Antares Mezzina ; Georgiana Caltais. Vol. 387 Open Publishing Association, 2023. pp. 59-75 (Electronic Proceedings in Theoretical Computer Science).

@inproceedings{8718589ee59f4e68808713742d71acc3,

title = "A Lean-Congruence Format for EP-Bisimilarity",

abstract = "Enabling preserving bisimilarity is a refinement of strong bisimilarity that preserves safety as well as liveness properties. To define it properly, labelled transition systems needed to be upgraded with a successor relation, capturing concurrency between transitions enabled in the same state. We enrich the well-known De Simone format to handle inductive definitions of this successor relation. We then establish that ep-bisimilarity is a congruence for the operators, as well as lean congruence for recursion, for all (enriched) De Simone languages.",

author = "{van Glabbeek}, Rob and Peter H{\"o}fner and Weiyou Wang",

note = "Funding Information: Supported by Royal Society Wolfson Fellowship RSWF\R1\221008 Publisher Copyright: {\textcopyright} R.J. van Glabbeek, P. H{\"o}fner & W. Wang.; Combined 30th International Workshop on Expressiveness in Concurrency and 20th Workshop on Structural Operational Semantics, EXPRESS/SOS 2023 ; Conference date: 18-09-2023",

year = "2023",

month = sep,

day = "14",

doi = "10.4204/EPTCS.387.6",

language = "English",

volume = "387",

series = "Electronic Proceedings in Theoretical Computer Science",

publisher = "Open Publishing Association",

pages = "59--75",

editor = "Mezzina, {Claudio Antares} and Georgiana Caltais",

booktitle = "Proceedings Combined 30th International Workshop on Expressiveness in Concurrency and 20th Workshop on Structural Operational Semantics (EXPRESS/SOS2023)",

address = "Australia",

url = "https://express-sos.github.io/",

}

van Glabbeek, R, Höfner, P & Wang, W 2023, A Lean-Congruence Format for EP-Bisimilarity. in CA Mezzina & G Caltais (eds), Proceedings Combined 30th International Workshop on Expressiveness in Concurrency and 20th Workshop on Structural Operational Semantics (EXPRESS/SOS2023). vol. 387, Electronic Proceedings in Theoretical Computer Science, Open Publishing Association, pp. 59-75, Combined 30th International Workshop on Expressiveness in Concurrency and 20th Workshop on Structural Operational Semantics, Antwerp, Belgium, 18/09/23. https://doi.org/10.4204/EPTCS.387.6

A Lean-Congruence Format for EP-Bisimilarity. / van Glabbeek, Rob; Höfner, Peter; Wang, Weiyou.
Proceedings Combined 30th International Workshop on Expressiveness in Concurrency and 20th Workshop on Structural Operational Semantics (EXPRESS/SOS2023). ed. / Claudio Antares Mezzina; Georgiana Caltais. Vol. 387 Open Publishing Association, 2023. p. 59-75 (Electronic Proceedings in Theoretical Computer Science).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - A Lean-Congruence Format for EP-Bisimilarity

AU - van Glabbeek, Rob

AU - Höfner, Peter

AU - Wang, Weiyou

N1 - Funding Information: Supported by Royal Society Wolfson Fellowship RSWF\R1\221008 Publisher Copyright: © R.J. van Glabbeek, P. Höfner & W. Wang.

PY - 2023/9/14

Y1 - 2023/9/14

N2 - Enabling preserving bisimilarity is a refinement of strong bisimilarity that preserves safety as well as liveness properties. To define it properly, labelled transition systems needed to be upgraded with a successor relation, capturing concurrency between transitions enabled in the same state. We enrich the well-known De Simone format to handle inductive definitions of this successor relation. We then establish that ep-bisimilarity is a congruence for the operators, as well as lean congruence for recursion, for all (enriched) De Simone languages.

AB - Enabling preserving bisimilarity is a refinement of strong bisimilarity that preserves safety as well as liveness properties. To define it properly, labelled transition systems needed to be upgraded with a successor relation, capturing concurrency between transitions enabled in the same state. We enrich the well-known De Simone format to handle inductive definitions of this successor relation. We then establish that ep-bisimilarity is a congruence for the operators, as well as lean congruence for recursion, for all (enriched) De Simone languages.

U2 - 10.4204/EPTCS.387.6

DO - 10.4204/EPTCS.387.6

M3 - Conference contribution

VL - 387

T3 - Electronic Proceedings in Theoretical Computer Science

SP - 59

EP - 75

BT - Proceedings Combined 30th International Workshop on Expressiveness in Concurrency and 20th Workshop on Structural Operational Semantics (EXPRESS/SOS2023)

A2 - Mezzina, Claudio Antares

A2 - Caltais, Georgiana

PB - Open Publishing Association

T2 - Combined 30th International Workshop on Expressiveness in Concurrency and 20th Workshop on Structural Operational Semantics

Y2 - 18 September 2023

ER -

van Glabbeek R, Höfner P, Wang W. A Lean-Congruence Format for EP-Bisimilarity. In Mezzina CA, Caltais G, editors, Proceedings Combined 30th International Workshop on Expressiveness in Concurrency and 20th Workshop on Structural Operational Semantics (EXPRESS/SOS2023). Vol. 387. Open Publishing Association. 2023. p. 59-75. (Electronic Proceedings in Theoretical Computer Science). doi: 10.4204/EPTCS.387.6

A Lean-Congruence Format for EP-Bisimilarity

Abstract / Description of output

Publication series

Conference

Access to Document

Fingerprint

Cite this