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

Olivier Bournez (1) , Florent Garnier (1) , Claude Kirchner (1)

1 PROTHEO - Constraints, automatic deduction and software properties proofs

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.

Domaines: Autre [cs.OH]

Olivier Bournez, Florent Garnier, Claude Kirchner. Termination in finite mean time of a CSMA/CA rule-based model. 2006. ⟨inria-00000774⟩