A calculus of countable broadcasting systems

In this paper we propose a process algebra named CCB (a Calculus of Countable Broadcasting Systems). We define an observational congruence relation in CCB after basic definitions of CCB, and give a sound and complete axiom system for the congruence relation of finite agents. CCB is developed for analyzing a multi-agent model with broadcast communication. The most important property of CCB is that a broadcaster of a message can know the number of receivers of the message after broadcasting. The property is not easily described in the other process algebras. The multi-agent model is useful for constructing extensible systems. A disadvantage of the multi-agent model is that agents must be designed very carefully because unexpected behavior may arise by interactions between the agents. Therefore we want to analyze behavior of the agents.