Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol