Connectivity and energy-aware preorders for mobile ad-hoc networks

Network connectivity and energy conservation are two major goals in mobile ad-hoc networks (MANETs). In this paper we propose a probabilistic, energy-aware, broadcast calculus for the analysis of both such aspects of MANETs. We first present a probabilistic behavioural congruence together with a co-inductive proof technique based on the notion of bisimulation. Then we define an energy-aware preorder over networks. The behavioural congruence allows us to verify whether two networks exhibit the same (probabilistic) connectivity behaviour, while the preorder makes it possible to evaluate the energy consumption of different, but behaviourally equivalent, networks. In practice, the quantitative evaluation of the models is carried out by resorting to the statistical model checking implemented in the PRISM tool, i.e., a simulation of the probabilistic model. We consider two case studies: first we evaluate the performance of the Location Aided Routing protocol, then we compare the energy efficiency of the Go-Back-N protocol with that of the Stop-And-Wait in a network with mobility.