Broadcast calculus interpreted in CCS upto bisimulation

8Citations
Citations of this article
5Readers
Mendeley users who have this article in their library.

Abstract

A function M is given that takes any process p in the calculus of broadcasting systems CBS and returns a CCS process M(p) with special actions {hear?, heard!, say?, said!} such that a broadcast of ω by p is matched by the sequence say? τ* said(ω) by M(p) and a reception of v by hear(v) ? tau;* heard!. It is shown that p ∼ M(p), where ∼ is a bisimulation equivalence using the above matches, and that M(p) has no CCS behaviour not covered by ∼. Thus the abstraction of a globally synchronising broadcast can be implemented by sequences of local synchronisations. The criteria of correctness are unusual, and arguably stronger than requiring equivalences to be preserved - the latter does not guarantee that meaning is preserved. Since ∼ is not a native CCS equivalence, it is a matter of dicussion what the result says about Holmer's (CONCUR'93) conjecture, partially proved by Ene and Muntean (FCT'99), that CCS cannot interpret CBS upto preservation of equivalence. © 2002 Published by Elsevier Science B.V.

Cite

CITATION STYLE

APA

Prasad, K. V. S. (2002). Broadcast calculus interpreted in CCS upto bisimulation. In Electronic Notes in Theoretical Computer Science (Vol. 52, pp. 83–100). https://doi.org/10.1016/S1571-0661(04)00218-X

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free