Probabilistic Models and Process Calculi for Mobile Ad Hoc Networks

Due to the wide use of communicating mobile devices, mobile ad hoc networks (MANETs) have gained in popularity in recent years. In order that the devices communicate properly, many protocols have been proposed working at different levels. Devices in an MANET are not stationary but may keep moving, thus the network topology may undergo constant changes. Moreover the devices in an MANET are loosely connected not depending on pre-installed infrastructure or central control components, they exchange messages via wireless connections which are less reliable compared to wired connections. Therefore the protocols for MANETs are usually more complicated and error-prone. In this thesis we discuss different models and their underlying theories which will facilitate the verification of protocols
for MANETs.

Process calculi have been used successfully as a formal method to verify and
analyze functional behaviors of concurrent systems e.g. free of deadlock, and they also have been extended with probability to verify quantitative properties e.g. “the sent message will arrive at the destination in 5 seconds with probability no less than 0.99”. In this thesis we extend the framework to deal with special issues in MANETs e.g. mobility and unreliable connections. Specially speaking,
1. We first propose a discrete probabilistic process calculus with which we can model in an MANET that the wireless connection is not reliable, and the network topology may undergo changes. We equip each wireless connection with a probability, and moreover we allow these probabilities to be changed according to some mobility rule to model the changes of the network topology.
2. Secondly we extend the discrete probabilistic process calculus in several directions: i) Generalize the notions of mobility rules which allow to change part of a network topology depending on an exponentially distributed random delay and a network topology constraint. ii) Introduce stochastic time behavior for processes running at network nodes. iii) A novel abstraction is proposed where several broadcasts may be simulated by one.
3. Various behavioral equivalences and their logical characterizations have been proposed to combat the infamous states space explosion problem of PAs, but unfortunately it is well known that the behavioral equivalences are strictly stronger than the logical equivalences induced by PCTL or PCTL*. We address this problem in this thesis by introducing a sequence of strong bisimulations, which will converge to the PCTL or PCTL* equivalence eventually. This work is then extended to CTMDPs.
4. Recently, MAs have been proposed as a compositional behavior model supporting both probabilistic transitions and exponentially distributed random delays. In this thesis, we introduce both early and late semantics for MAs based on which we define the early and late weak bisimulation respectively. We also show that the early weak bisimulation coincides with the previous variants while the late weak bisimulation is strictly coarser than them.