Modelling Probabilistic Wireless Networks

We propose a process calculus to model high level wireless systems, where thetopology of a network is described by a digraph. The calculus enjoys featureswhich are proper of wireless networks, namely broadcast communication andprobabilistic behaviour. We first focus on the problem of composing wirelessnetworks, then we present a compositional theory based on a probabilisticgeneralisation of the well known may-testing and must-testing pre- orders.Also, we define an extensional semantics for our calculus, which will be usedto define both simulation and deadlock simulation preorders for wirelessnetworks. We prove that our simulation preorder is sound with respect to themay-testing preorder; similarly, the deadlock simulation pre- order is soundwith respect to the must-testing preorder, for a large class of networks. Wealso provide a counterexample showing that completeness of the simulationpreorder, with respect to the may testing one, does not hold. We conclude thepaper with an application of our theory to probabilistic routing protocols