Bisimulations for a calculus of broadcasting systems

Abstract. We develop a theory of bisimulation equivalence for the broadcast calculus CBS. Both the strong and weak versions of bisimulation congruence we study are justified in terms of a characterisation as the largest CBS con-gruences contained in an appropriate version of barbed bisimulation. We then present sound and complete proof systems for both the strong and weak congruences over finite expressions. The first system we give contains an infinitaxy proof rule to accommodate input prefixes. We improve on this by presenting a finitary proof system wher e judgements are relative to properties of the data domain. 1 In t roduct ion The Broadcast Calculus, CBS, is a value-passing process calculus where process intercommunication s achieved by the broadcasting ofvalues. The calculus has been developed in series of papers [8, 9, 12] and has been implemented as an extension to Lazy ML, [10]. Here we are concerned with the development of a semantic theory for the Broad