TY - GEN
T1 - Synchronous message passing
T2 - On the relation between bisimulation and refusal equivalence
AU - Broy, Manfred
PY - 2010
Y1 - 2010
N2 - To find congruence relations proved more difficult for synchronous message passing than for asynchronous message passing. As well-known, trace equivalence of state-machines, which represents to a congruence relation for asynchronous computations, is not a congruence relation for the classical operators of parallel composition as found in process algebras with synchronous message passing. In the literature we find two fundamentally different proposals to define congruence relations for synchronous message passing systems. One is using David Park's bisimulation used by Robin Milner for his Calculus of Communicating Systems (CCS) which introduces a class of relations between systems with synchronous message passing, the other one is an equivalence relation, introduced by the denotational semantics, given by Tony Hoare for a process algebra like Communicating Sequential Processes (CSP), based on so-called readiness, refusal and failure concepts. In this little note we analyze the question whether the equivalence relation, introduced by denotational semantics is in fact a bisimulation.
AB - To find congruence relations proved more difficult for synchronous message passing than for asynchronous message passing. As well-known, trace equivalence of state-machines, which represents to a congruence relation for asynchronous computations, is not a congruence relation for the classical operators of parallel composition as found in process algebras with synchronous message passing. In the literature we find two fundamentally different proposals to define congruence relations for synchronous message passing systems. One is using David Park's bisimulation used by Robin Milner for his Calculus of Communicating Systems (CCS) which introduces a class of relations between systems with synchronous message passing, the other one is an equivalence relation, introduced by the denotational semantics, given by Tony Hoare for a process algebra like Communicating Sequential Processes (CSP), based on so-called readiness, refusal and failure concepts. In this little note we analyze the question whether the equivalence relation, introduced by denotational semantics is in fact a bisimulation.
KW - Bisimulation
KW - Refusal equivalence
KW - Synchronous message passing
KW - Trace equivalence
UR - http://www.scopus.com/inward/record.url?scp=77950109327&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-11512-7_8
DO - 10.1007/978-3-642-11512-7_8
M3 - Conference contribution
AN - SCOPUS:77950109327
SN - 364211511X
SN - 9783642115110
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 118
EP - 126
BT - Concurrency, Compositionality, and Correctness - Essays in Honor of Willem-Paul de Roever
A2 - Dams, Dennis
A2 - Hannemann, Ulrich
A2 - Steffen, Martin
ER -