A broadcast-based calculus for communicating systems

Abstract

This paper presents a process calculus for reconfig-urable communicating systems which has broadcast as ba-sic communication primitive, and we provide an opera-tional semantics for this calculus. We illustrate the calculus through some examples, and we propose three behavioural equivalences for reasoning about systems of broadcasting processes, namely, barbed equivalence, step-equivalence and labelled bisimilarity. An important result, is that all these relations coincide, providing different ways to study the equivalence/non-equivalence of two systems. Then, we provide a direct characterization for the strong congruence relation induced by these equivalences. Finally, we give a complete axiomatisation for strong congruence. 1.