Date Added: Jan 2012
With the widespread usage of the 802.11 protocol, it becomes important to study the protocol operation. In this paper, the authors propose a formal model for the point coordination function of the 802.11 MAC layer using systems of communicating machines. Their goal is to analyze the protocol for safety and liveness properties. These properties cannot be verified directly from the protocol description. Analysis shows that the PCF protocol is free from deadlocks and non-executable transitions. They also show that liveness is guaranteed in the PCF protocol.