A Calculus for Mobile Ad-hoc Networks with Static Location Binding

We present a process calculus for mobile ad hoc networks which is a natural continuation of our earlier work on the process calculus CMAN [J.C. Godskesen. A calculus for mobile ad hoc networks. In Proceedings of the 9th International Conference, COORDINATION 2007, volume 4467 of LNCS, pages 132–150, Paphos, Cyprus, June 2007. Springer–Verlag]. Essential to the new calculus is the novel restricted treatment of node mobility imposed by hiding of location names using a static binding operator, and we introduce the more general notion of unidirectional links instead of bidirectional links. We define a natural weak reduction semantics and a reduction congruence and prove our weak contextual bisimulation equivalence to be a sound and complete co-inductive characterization of the reduction congruence.The two changes to the calculus in [J.C. Godskesen. A calculus for mobile ad hoc networks. In Proceedings of the 9th International Conference, COORDINATION 2007, volume 4467 of LNCS, pages 132–150, Paphos, Cyprus, June 2007. Springer–Verlag] yields a much simpler bisimulation semantics, and importantly and in contrast to [J.C. Godskesen. A calculus for mobile ad hoc networks. In Proceedings of the 9th International Conference, COORDINATION 2007, volume 4467 of LNCS, pages 132–150, Paphos, Cyprus, June 2007. Springer–Verlag] we manage to provide a non-contextual weak bisimulation congruence facilitating ease of proofs and being strictly contained in the contextual bisimulation.