Towards a probabilistic calculus for mobile ad hoc networks

In this paper we present a probabilistic calculus for formally modeling and reasoning about Mobile Ad Hoc Networks (MANETs) with unreliable connections and mobility of nodes. In our calculus, a MANET node can locally broadcast messages to a group of nodes within its physical transmission range. The group probability is also introduced since two distinct nodes within different groups should receive messages from the same sender with different possibilities. Our calculus naturally captures essential features of MANETs, i.e., local broadcast, mobility and probability. Moreover, we give a formal operational semantics of the calculus in terms of the labeled transition system and define the notion of open bisimulation. Finally, we illustrate our calculus with a toy example.