Generalised Communication for Interacting Agents

Process algebra for quantitative evaluation are based on either of the two following mechanisms for communication: binary, where a channel is shared by exactly two agents, or multiway, where all agents sharing a channel must synchronise. In this paper we consider an intermediate form which we call generalised communication, where only m agents out of n potentially available are involved in the communication. We study this in the context of the stochastic process algebra PEPA, of which we conservatively extend the syntax and semantics. We give an intuitive interpretation in terms of bandwidth assignments to agents communicating over a shared medium. We validate this semantics using a real implementation of a simple peer-to-peer protocol, for which our performance model yields predictions with high accuracy. We prove a result of lumpability that exploits symmetries between identical communicating agents, yielding good scalability of the underlying continuous-time Markov chain (CTMC) with respect to increasing population levels. Furthermore, we present an algorithm that derives the lumped chain directly, without having to generate the full CTMC first.