An Observational Theory for Mobile Ad Hoc Networks (full version)

We propose a process calculus to study the behavioural theory of Mobile Ad Hoc Networks. The operational semantics of our calculus is given both in terms of a Reduction Semantics and in terms of a Labelled Transition Semantics. We prove that the two semantics coincide. The labelled transition system is then used to derive the notions of (weak) simulation and bisimulation for ad hoc networks. The labelled bisimilarity completely characterises reduction barbed congruence, a standard branching-time and contextually-defined program equivalence. We then use our (bi)simulation proof method to formally prove a number of non-trivial properties of ad hoc networks.