On Cool Congruence Formats for Weak Bisimulations

Rob Jan van Glabbeek

doi:10.1007/11560647_21

On Cool Congruence Formats for Weak Bisimulations

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

Abstract / Description of output

In TCS 146, Bard Bloom presented rule formats for four main notions of bisimulation with silent moves. He proved that weak bisimulation equivalence is a congruence for any process algebra defined by WB cool rules, and established similar results for rooted weak bisimulation (Milner's ``observational congruence''), branching bisimulation and rooted branching bisimulation. This study reformulates Bloom's results in a more accessible form and contributes analogues for (rooted) $-bisimulation and (rooted) delay bisimulation. Moreover, finite equational axiomatisations of rooted weak bisimulation equivalence are provided that are sound and complete for finite processes in any RWB cool process algebra. These require the introduction of auxiliary operators with lookahead. Finally, a challenge is presented for which Bloom's formats fall short and further improvement is called for.

Original language	English
Title of host publication	Theoretical Aspects of Computing -- ICTAC 2005: Second International Colloquium, Hanoi, Vietnam, October 17-21, 2005, Proceedings
Editors	Dang Van Hung, Martin Wirsing
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	318-333
Number of pages	16
ISBN (Electronic)	978-3-540-32072-2
ISBN (Print)	978-3-540-29107-7
DOIs	https://doi.org/10.1007/11560647_21
Publication status	Published - 21 Oct 2005
Event	The 2nd International Colloquium on Theoretical Aspects of Computing, 2005 - Hanoi, Viet Nam Duration: 17 Oct 2005 → 21 Oct 2005 Conference number: 2

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin, Heidelberg
Volume	3722
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	The 2nd International Colloquium on Theoretical Aspects of Computing, 2005
Abbreviated title	ICTAC 2005
Country/Territory	Viet Nam
City	Hanoi
Period	17/10/05 → 21/10/05

Access to Document

10.1007/11560647_21Licence: All Rights Reserved

https://link.springer.com/chapter/10.1007/11560647_21Licence: All Rights Reserved

Cite this

@inproceedings{247dcf151de64f32ba3c32d497000b7c,

title = "On Cool Congruence Formats for Weak Bisimulations",

abstract = "In TCS 146, Bard Bloom presented rule formats for four main notions of bisimulation with silent moves. He proved that weak bisimulation equivalence is a congruence for any process algebra defined by WB cool rules, and established similar results for rooted weak bisimulation (Milner's ``observational congruence''), branching bisimulation and rooted branching bisimulation. This study reformulates Bloom's results in a more accessible form and contributes analogues for (rooted) $-bisimulation and (rooted) delay bisimulation. Moreover, finite equational axiomatisations of rooted weak bisimulation equivalence are provided that are sound and complete for finite processes in any RWB cool process algebra. These require the introduction of auxiliary operators with lookahead. Finally, a challenge is presented for which Bloom's formats fall short and further improvement is called for.",

author = "{van Glabbeek}, {Rob Jan}",

year = "2005",

month = oct,

day = "21",

doi = "10.1007/11560647_21",

language = "English",

isbn = "978-3-540-29107-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "318--333",

editor = "{Van Hung}, Dang and Martin Wirsing",

booktitle = "Theoretical Aspects of Computing -- ICTAC 2005: Second International Colloquium, Hanoi, Vietnam, October 17-21, 2005, Proceedings",

address = "United Kingdom",

note = "The 2nd International Colloquium on Theoretical Aspects of Computing, 2005, ICTAC 2005 ; Conference date: 17-10-2005 Through 21-10-2005",

}

van Glabbeek, RJ 2005, On Cool Congruence Formats for Weak Bisimulations. in D Van Hung & M Wirsing (eds), Theoretical Aspects of Computing -- ICTAC 2005: Second International Colloquium, Hanoi, Vietnam, October 17-21, 2005, Proceedings. Lecture Notes in Computer Science, vol. 3722, Springer, Berlin, Heidelberg, pp. 318-333, The 2nd International Colloquium on Theoretical Aspects of Computing, 2005, Hanoi, Viet Nam, 17/10/05. https://doi.org/10.1007/11560647_21

On Cool Congruence Formats for Weak Bisimulations. / van Glabbeek, Rob Jan.
Theoretical Aspects of Computing -- ICTAC 2005: Second International Colloquium, Hanoi, Vietnam, October 17-21, 2005, Proceedings. ed. / Dang Van Hung; Martin Wirsing. Berlin, Heidelberg: Springer, 2005. p. 318-333 (Lecture Notes in Computer Science; Vol. 3722).

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

TY - GEN

T1 - On Cool Congruence Formats for Weak Bisimulations

AU - van Glabbeek, Rob Jan

N1 - Conference code: 2

PY - 2005/10/21

Y1 - 2005/10/21

N2 - In TCS 146, Bard Bloom presented rule formats for four main notions of bisimulation with silent moves. He proved that weak bisimulation equivalence is a congruence for any process algebra defined by WB cool rules, and established similar results for rooted weak bisimulation (Milner's ``observational congruence''), branching bisimulation and rooted branching bisimulation. This study reformulates Bloom's results in a more accessible form and contributes analogues for (rooted) $-bisimulation and (rooted) delay bisimulation. Moreover, finite equational axiomatisations of rooted weak bisimulation equivalence are provided that are sound and complete for finite processes in any RWB cool process algebra. These require the introduction of auxiliary operators with lookahead. Finally, a challenge is presented for which Bloom's formats fall short and further improvement is called for.

AB - In TCS 146, Bard Bloom presented rule formats for four main notions of bisimulation with silent moves. He proved that weak bisimulation equivalence is a congruence for any process algebra defined by WB cool rules, and established similar results for rooted weak bisimulation (Milner's ``observational congruence''), branching bisimulation and rooted branching bisimulation. This study reformulates Bloom's results in a more accessible form and contributes analogues for (rooted) $-bisimulation and (rooted) delay bisimulation. Moreover, finite equational axiomatisations of rooted weak bisimulation equivalence are provided that are sound and complete for finite processes in any RWB cool process algebra. These require the introduction of auxiliary operators with lookahead. Finally, a challenge is presented for which Bloom's formats fall short and further improvement is called for.

U2 - 10.1007/11560647_21

DO - 10.1007/11560647_21

M3 - Conference contribution

SN - 978-3-540-29107-7

T3 - Lecture Notes in Computer Science

SP - 318

EP - 333

BT - Theoretical Aspects of Computing -- ICTAC 2005: Second International Colloquium, Hanoi, Vietnam, October 17-21, 2005, Proceedings

A2 - Van Hung, Dang

A2 - Wirsing, Martin

PB - Springer

CY - Berlin, Heidelberg

T2 - The 2nd International Colloquium on Theoretical Aspects of Computing, 2005

Y2 - 17 October 2005 through 21 October 2005

ER -

On Cool Congruence Formats for Weak Bisimulations

Abstract / Description of output

Publication series

Conference

Access to Document

Fingerprint

Cite this