  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.
