An Observational Theory for Mobile Ad Hoc Networks

10 years 6 months ago
An Observational Theory for Mobile Ad Hoc Networks
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.
Massimo Merro
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Authors Massimo Merro
Comments (0)