# zbMATH — the first resource for mathematics

Broadcast calculus interpreted in CCS upto bisimulation. (English) Zbl 1260.68276
Aceto, Luca (ed.) et al., EXPRESS’01. Proceedings of the 8th international workshop on expressiveness in concurrency, a satellite workshop of CONCUR 2001, Aalborg, Denmark, August 20, 2001. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 52, No. 1, 83-100 (2002).
Summary: 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 $$\{\mathsf{hear}?$$, $$\mathsf{heard}!$$, $$\mathsf{say}?$$, $$\mathsf{said}!\}$$ such that a broadcast of $$\omega$$ by $$p$$ is matched by the sequence $$\mathsf{say}?$$ $$\tau^{*}$$ $$\mathsf{said}(\omega)$$ by $$M(p)$$ and a reception of $$\upsilon$$ by $$\mathsf{hear}(v)?$$ $$\tau^{*}$$ $$\mathsf{heard}!$$. It is shown that $$p \sim M(p)$$, where $$\sim$$ is a bisimulation equivalence using the above matches, and that $$M(p)$$ has no CCS behaviour not covered by $$\sim$$. 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 $$\sim$$ is not a native CCS equivalence, it is a matter of dicussion what the result says about U. Holmer’s [Lect. Notes Comput. Sci. 715, 188–201 (1993)] conjecture, partially proved by C. Ene and T. Muntean [Lect. Notes Comput. Sci. 1684, 258–268 (1999; Zbl 0946.68096)], that CCS cannot interpret CBS upto preservation of equivalence.
For the entire collection see [Zbl 1260.68008].

##### MSC:
 68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: