A simple probabilistic broadcast language

We propose a process calculus to model high level wireless systems, where the topology of a network is described by a graph. The calculus enjoys features which are proper of wireless networks, namely broadcast communication and probabilistic behaviour. We first focus on the problem of composing wireless networks, then we present a compositional theory based on a generalisation of the well known may-testing preorder. Also, we define an extensional semantics for our calculus, and the respective simulation preorder induced. We prove that our simulation preorder is sound with respect to the may testing preorder, thus providing a proof method for establishing whether two networks cannot be distinguished by any test. However, we also provide a counterexample showing that completeness of the simulation preorder, with respect to the may testing one, does not hold. We conclude the paper with an application of our theory to routing protocols.