# A Process Algebra for Link Layer Protocols

## TL;DR

This paper introduces a process algebra tailored for link layer protocols, enabling formal modeling of frame collisions and analysis of CSMA/CA variants, revealing their strengths and limitations in handling specific network problems.

## Contribution

It presents a novel process algebra for link layer protocols with mechanisms for modeling collisions and formalizes liveness properties, applied to analyze CSMA/CA protocols.

## Key findings

- Virtual carrier sensing overcomes hidden and exposed station problems
- Protocol cannot guarantee packet delivery even with probability 1
- Analysis confirms effectiveness of virtual sensing in specific scenarios

## Abstract

We propose a process algebra for link layer protocols, featuring a unique mechanism for modelling frame collisions. We also formalise suitable liveness properties for link layer protocols specified in this framework. To show applicability we model and analyse two versions of the Carrier-Sense Multiple Access with Collision Avoidance (CSMA/CA) protocol. Our analysis confirms the hidden station problem for the version without virtual carrier sensing. However, we show that the version with virtual carrier sensing not only overcomes this problem, but also the exposed station problem with probability 1. Yet the protocol cannot guarantee packet delivery, not even with probability 1.