Termination in finite mean time of a CSMA/CA rule-based model

In a recent work, we introduced the notion of probabilistic rewrite system, and we proposed techniques to prove termination of such systems in finite mean time. In this paper, we model with probabilistic rewrite rules a WI-FI stations network running the CSMA/CA 802.11b protocol. Following this model and using the previously proposed framework, we prove that the protocol terminates in a finite mean time