# Reliable Restricted Process Theory

## TL;DR

This paper explores the adaptation of Restricted Broadcast Process Theory to reliable communication in MANETs, analyzing its semantic implications and demonstrating its application through a routing protocol example.

## Contribution

It introduces a modified framework for reliable communication in Restricted Broadcast Process Theory and develops a new proof process for protocol correctness.

## Key findings

- Reliable communication affects the semantics of the process theory.
- The non-blocking property and behavioral equivalence are impacted by the adaptation.
- A novel proof process based on precongruence is proposed.

## Abstract

Malfunctions of a mobile ad hoc network (MANET) protocol caused by a conceptual mistake in the protocol design, rather than unreliable communication, can often be detected only by considering communication among the nodes in the network to be reliable. In Restricted Broadcast Process Theory, which was developed for the specification and verification of MANET protocols, the communication operator is lossy. Replacing unreliable with reliable communication invalidates existing results for this process theory. We examine the effects of this adaptation on the semantics of the framework with regard to the non-blocking property of communication in MANETs, the notion of behavioral equivalence relation and its axiomatization. We illustrate the applicability of our framework through a simple routing protocol. To prove its correctness, we introduce a novel proof process, based on a precongruence relation.