A Stochastic Process Algebra Model for the Analysis of the Alternating Bit Protocol