A Process Calculus for Mobile Ad Hoc Networks

Anu Singh, C. R. Ramakrishnan, Scott A. Smolka


We present the omega-calculus, a process calculus for formally modeling and reasoning about Mobile Ad Hoc Wireless Networks (MANETs) and their protocols. The omega-calculus naturally captures essential characteristics of MANETs, including the ability of a MANET node to broadcast a message to any other node within its physical transmission range (and no others), and to move in and out of the transmission range of other nodes in the network. A key feature of the omega-calculus is the separation of a node's communication and computational behavior, described by an omega-process, from the description of its physical transmission range, referred to as an omega-process interface.

Our main technical results are as follows. We give a formal operational semantics of the omega-calculus in terms of labeled transition systems and show that the state reachability problem is decidable for finite-control omega-processes. We also prove that the omega-calculus is a conservative extension of the pi-calculus, and that late bisimulation (appropriately lifted from the pi-calculus to the omega-calculus) is a congruence. Congruence results are also established for a weak version of late bisimulation, which abstracts away from two types of internal actions: tau-actions, as in the pi-calculus, and mu-actions, signaling node movement. Finally, we illustrate the practical utility of the calculus by developing and analyzing a formal model of a leader-election protocol for MANETs.

Bibtex Entry:

author = {Anu Singh and  C. R. Ramakrishnan and  Scott A. Smolka},
title = {A Process Calculus for Mobile Ad Hoc Networks},
booktitle = {10th International Conference on Coordination Models and Languages (COORDINATION)},
address = {Oslo, Norway},
month = {June},
series = {Lecture Notes in Computer Science},
volume = {5052},
pages = {296--314},
publisher = {Springer},
year = {2008}

Full Paper: [pdf]

Home | Papers

C. R. Ramakrishnan