We propose a process algebra for wireless mesh networks that combines novel treatments of local broadcast, conditional unicast and data structures. In this framework, we model the Ad-hoc On-Demand Distance Vector (AODV) routing protocol and (dis)prove crucial properties such as loop freedom and packet delivery.
@article{arxiv.1512.07319,
title = {A Process Algebra for Wireless Mesh Networks},
author = {Ansgar Fehnker and Rob van Glabbeek and Peter Höfner and Annabelle McIver and Marius Portmann and Wee Lum Tan},
journal= {arXiv preprint arXiv:1512.07319},
year = {2015}
}
Comments
arXiv admin note: substantial text overlap with arXiv:1312.7645