Connectivity and communication interference are two key aspects in mobile ad-hoc
networks (MANETs). This paper proposes a process algebraic model targeted at the
analysis of both such aspects. The framework includes a probabilistic process calculus and
a suite of analytical techniques based on a probabilistic observational congruence and an
interference-sensitive preorder. The former enables the verification of behavioural
equivalences; the latter makes it possible to evaluate the interference level of behaviourally …