×

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.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Crisys project home page, http://ais.gmd.de/ap/crisys/.
[2] Andersen J., E. Harcourt and K. V. S. Prasad, A machine verified sorting algorithm, Technical Report RS-96-4, BRICS, Aarhus (1996).
[3] de Simone, R., Higher level synchronising devices in MEIJE-SCCS, Theoretical computer science, 37, 245-268, (1985) · Zbl 0598.68027
[4] Ene C. and T. Muntean, Expressiveness of broadcast communication, in: G. Ciobanu and G. Paun, editors, Fundamentals of Computation Theory, 12th International Symposium, FCT ’99, LNCS \bf1684 (1999), pp. 258-268. · Zbl 0946.68096
[5] Giménez E., An application of co-inductive types in coq: verification of the alternating bit protocol, in: Workshop on Types for Proofs and Programs, LNCS \bf1158 (1995), pp. 135-152.
[6] Harcourt E., P. Paczkowski and K. V. S. Prasad, A framework for representing value-passing parametric processes (1995), http://www.cs.chalmers.se/prasad/parametric.html.
[7] Hennessy, M.; Rathke, J., Bisimulations for a calculus of broadcasting systems, Theoretical computer science, 200, 225-260, (1998) · Zbl 0915.68065
[8] Holmer U., Translating broadcast communication into SCCS, in: E. Best, editor, CONCUR’93, LNCS \bf715 (1993), pp. 188-201.
[9] Jones S., Translating CBS to LML, Technical report, Department of Computer Science, Chalmers University of Technology (1993).
[10] Milner, R., Calculi for synchrony and asynchrony, Theoretical computer science, 25, 267-310, (1983) · Zbl 0512.68026
[11] Milner, R., “communication and concurrency,”, (1989), Prentice Hall
[12] Petersson J., Tools for a calculus of broadcasting systems, Licentiate thesis, Department of Computer Science, Chalmers University of Technology (1994).
[13] Prasad, K. V. S., Programming with broadcasts, in: E. Best, editor, CONCUR’93, LNCS \bf715 (1993), pp. 173-187.
[14] Prasad, K.V.S., A calculus of broadcasting systems, Science of computer programming, 25, 285-327, (1995)
[15] Prasad, K. V. S., Broadcasting in time, in: P. Ciancarini and C. Hankin, editors, COORDINATION’96, LNCS \bf1061 (1996), pp. 321-338.
[16] Runciman, C.; Wakeling, D., Profiling parallel functional computations, (), 236-251
[17] Wilhelmi S., A virtual TCBS machine on top of C++, Web site, Univ. of Karlsruhe (2000), http://goethe.ira.uka.de/wilhelmi/cbs/.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.