  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.
