A calculus of broadcasting systems

Abstract

Local area networks (LANs) and everyday speech inspire a model of communication by unbuffered broadcast. Computation proceeds by a sequence of messages, each transmitted by one agent and received by zero or more others. Transmission is autonomous, but reception is not. Each message is received instantaneously by all agents except the transmitter, but is read only by those who were monitoring it at the time; others discard it. As in CCS, agents learn about the environment only through the messages they read. Programming such a system is hard because we have to ensure that messages are read. Testing resembles a viva-voce examination. Observation, restriction and hidden actions differ from their CCS counterparts, as does testing equivalence. We capture this model in a Calculus of Broadcasting Systems (CBS). We use transition systems with transmit, read and discard actions. Discards are self-loops, and only auxiliary. We have some results on strong bisimulation and testing, but much work remains to make CBS tractable.