CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Broadcast Calculus Interpreted in CCS upto Bisimulation

K. V. S. Prasad (Institutionen för datavetenskap)
Electronical Notes in Theoretical Computer Science (1571-0661). Vol. 52 (2001), 1, p. 83-100.
[Artikel, refereegranskad vetenskaplig]

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 υ by hear(v) τ∗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.

Denna post skapades 2014-02-04. Senast ändrad 2014-02-04.
CPL Pubid: 193381


Institutioner (Chalmers)

Institutionen för datavetenskap (1993-2001)


Datavetenskap (datalogi)

Chalmers infrastruktur