A Probabilistic Energy-Aware Model for Mobile Ad-Hoc Networks

We propose a probabilistic, energy-aware, broadcast calculus for the analysis of mobile ad-hoc networks. The semantics of our model is expressed in terms of Segala's probabilistic automata driven by schedulers to resolve the nondeterministic choice among the probability distributions over target states. We develop a probabilistic observational congruence and a energy-aware preorder semantics. The observational congruence allows us to verify whether two networks exhibit the same observable probabilistic behaviour (connectivity), while the preorder is used to compare the energy consumption of different, but behaviourally equivalent, networks. As an application, we analyse and compare the energy consumption of two well-known automatic repeat request (ARQ)based error control protocols: stop-and-wait (SW) and go-back-N (GBN).