A process algebra for link layer protocols

DOI10.1007/978-3-030-17184-1_24MaRDI QIDQ6070802zbMATH OpenOpenAlexFDO

Authors Rob van Glabbeek, Peter Höfner, Michael Markl

Publication date 24 November 2023

Published in Programming Languages and Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1907.13329

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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.

Recommendations

• A timed process algebra for wireless networks with an application in routing (extended abstract)
• Probabilistic model checking of the CSMA/CD protocol using PRISM and APMC
• A process algebra for wireless mesh networks
• Modelling MAC-layer communications in wireless systems
• scientific article; zbMATH DE number 2090709

Cited in

(1)

• Angelic processes for CSP via the UTP

This page was built for publication: A process algebra for link layer protocols

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6070802)