A Timed Calculus for Mobile Ad Hoc Networks
This work addresses modeling challenges in MANETs for researchers in network theory, but it appears incremental as it builds on existing calculi by adding timed aspects.
The paper tackled the problem of modeling Mobile Ad Hoc Networks (MANETs) by developing a timed calculus that incorporates local broadcast, node mobility, and communication interference, and applied it to study MAC-layer protocols, proving equivalence between reduction and labelled transition semantics.
We develop a timed calculus for Mobile Ad Hoc Networks embodying the peculiarities of local broadcast, node mobility and communication interference. We present a Reduction Semantics and a Labelled Transition Semantics and prove the equivalence between them. We then apply our calculus to model and study some MAC-layer protocols with special emphasis on node mobility and communication interference. A main purpose of the semantics is to describe the various forms of interference while nodes change their locations in the network. Such interference only occurs when a node is simultaneously reached by more than one ongoing transmission over the same channel.