A Timed Calculus for Mobile Ad Hoc Networks

TL;DR

This paper introduces a timed calculus tailored for Mobile Ad Hoc Networks, capturing local broadcast, node mobility, and interference, with formal semantics and application to MAC-layer protocols.

Contribution

It presents a novel timed calculus with reduction and labelled semantics, specifically modeling interference and mobility in MANETs, and applies it to protocol analysis.

Findings

Formal semantics for interference modeling

Equivalence proof between semantics

Application to MAC-layer protocols

Abstract

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.