Bisimulations for a Calculus of Broadcasting Systems

We develop a theory of bisimulation equivalence for the broadcast calculus CBS. Both the strong and weak versions of bisimulation congruence we study are justi ed in terms of a characterisation as the largest CBS congruences contained in an appropriate version of barbed bisimulation. We then present sound and complete proof systems for both the strong and weak congruences over nite expressions. The rst system we give contains an in nitary proof rule to accommodate input pre xes. We improve on this by presenting a nitary proof system where judgements are relative to properties of the data domain.

• Type: Conference
• Year: 1995
• Where: CONCUR
• Authors: Matthew Hennessy, Julian Rathke
• Keywords: Bisimulation, Bisimulation Equivalence, CONCUR 1995, Distributed And Parallel Computing, Nitary Proof