# Aloha Protocol

### Contents

Related publications: [KNPS19, KNPS20]

### Introduction

This case study concerns three users trying to send packets using the slotted ALOHA protocol. In a time slot, if a single user tries to send a packet, there is a probability (q) that the packet is sent; as more users try and send, then the probability of success decreases. If sending a packet fails, the number of slots a user waits before resending is set according to an exponential backoff scheme. More precisely, each user maintains a backoff counter which it increases each time there is a failure (up to bmax) and, if the counter equals k, randomly chooses the slots to wait from {0,1,...,2k-1}.

### Concurrent Stochastic Game Model

The PRISM code representing a concurrent stochastic game of this scenario is given below. The model has three parameters: bcmax the maximum backoff counter, q the probability a packet is sent when two users try and send and D used for time-bounded properties. There are three players corresponding to the users trying to send packets.

The PRISM model also includes a reward structure corresponding to the time passage. Notice that time only passes when users are waiting before resending.

```// model of aloha protocol with backoff scheme (three players)
// each player tries to send a single message

csg

player usr1 user1 endplayer
player usr2 user2 endplayer
player usr3 user3 endplayer

const int bcmax; // backoff limit
const int M=pow(2,bcmax)-1; // backoff counter (slots to wait)

// time can pass
formula tick = (s1=0 | s1=2 | s1=3) & (s2=0 | s2=2 | s2=3) & (s3=0 | s3=2 | s3=3) & (tr1=0 & tr2=0 & tr3=0);

// probability of successful transmission
const double beta=1;
const double q;
formula n = tr1+tr2+tr3;
formula rn = (n=3)? q/(pow(beta,2)*3) : (n=2)? q/(pow(beta,2)*2) : (n=1)? q : 0;

module user1

s1 : [0..3] init 0; // local state
tr1 : [0..1]; // try to transmit
bc1 : [0..M]; // backoff counter
cd1 : [0..bcmax]; // collision counter
t1 : [0..2]; // can only wait for two time units before trying

// wait or decide to try and transmit
[wait1] tick & (s1=0 | s1=3) & t1<2 -> (t1'=t1+1);
[trans1] tick & s1=0 -> (tr1'=1) & (t1'=0);
// transmit
[try1] tr1=1 -> (rn/n) : (s1'=3) & (tr1'=0)
+ (1-rn/n) : (s1'=1) & (tr1'=0) & (cd1'=min(bcmax,cd1+1));
// set backoff counter
[sbc1] s1=1 & cd1=1 -> 1/2 : (s1'=2) & (bc1'=0)
+ 1/2 : (s1'=2) & (bc1'=1);
[sbc1] s1=1 & cd1=2 -> 1/4 : (s1'=2) & (bc1'=0)
+ 1/4 : (s1'=2) & (bc1'=1)
+ 1/4 : (s1'=2) & (bc1'=2)
+ 1/4 : (s1'=2) & (bc1'=3);
[sbc1] s1=1 & cd1=3 -> 1/8 : (s1'=2) & (bc1'=0)
+ 1/8 : (s1'=2) & (bc1'=1)
+ 1/8 : (s1'=2) & (bc1'=2)
+ 1/8 : (s1'=2) & (bc1'=3)
+ 1/8 : (s1'=2) & (bc1'=4)
+ 1/8 : (s1'=2) & (bc1'=5)
+ 1/8 : (s1'=2) & (bc1'=6)
+ 1/8 : (s1'=2) & (bc1'=7);
[sbc1] s1=1 & cd1=4 -> 1/16 : (s1'=2) & (bc1'=0)
+ 1/16 : (s1'=2) & (bc1'=1)
+ 1/16 : (s1'=2) & (bc1'=2)
+ 1/16 : (s1'=2) & (bc1'=3)
+ 1/16 : (s1'=2) & (bc1'=4)
+ 1/16 : (s1'=2) & (bc1'=5)
+ 1/16 : (s1'=2) & (bc1'=6)
+ 1/16 : (s1'=2) & (bc1'=7)
+ 1/16 : (s1'=2) & (bc1'=8)
+ 1/16 : (s1'=2) & (bc1'=9)
+ 1/16 : (s1'=2) & (bc1'=10)
+ 1/16 : (s1'=2) & (bc1'=11)
+ 1/16 : (s1'=2) & (bc1'=12)
+ 1/16 : (s1'=2) & (bc1'=13)
+ 1/16 : (s1'=2) & (bc1'=14)
+ 1/16 : (s1'=2) & (bc1'=15);
[sbc1] s1=1 & cd1=5 -> 1/32 : (s1'=2) & (bc1'=0)
+ 1/32 : (s1'=2) & (bc1'=1)
+ 1/32 : (s1'=2) & (bc1'=2)
+ 1/32 : (s1'=2) & (bc1'=3)
+ 1/32 : (s1'=2) & (bc1'=4)
+ 1/32 : (s1'=2) & (bc1'=5)
+ 1/32 : (s1'=2) & (bc1'=6)
+ 1/32 : (s1'=2) & (bc1'=7)
+ 1/32 : (s1'=2) & (bc1'=8)
+ 1/32 : (s1'=2) & (bc1'=9)
+ 1/32 : (s1'=2) & (bc1'=10)
+ 1/32 : (s1'=2) & (bc1'=11)
+ 1/32 : (s1'=2) & (bc1'=12)
+ 1/32 : (s1'=2) & (bc1'=13)
+ 1/32 : (s1'=2) & (bc1'=14)
+ 1/32 : (s1'=2) & (bc1'=15)
+ 1/32 : (s1'=2) & (bc1'=16)
+ 1/32 : (s1'=2) & (bc1'=17)
+ 1/32 : (s1'=2) & (bc1'=18)
+ 1/32 : (s1'=2) & (bc1'=19)
+ 1/32 : (s1'=2) & (bc1'=20)
+ 1/32 : (s1'=2) & (bc1'=21)
+ 1/32 : (s1'=2) & (bc1'=22)
+ 1/32 : (s1'=2) & (bc1'=23)
+ 1/32 : (s1'=2) & (bc1'=24)
+ 1/32 : (s1'=2) & (bc1'=25)
+ 1/32 : (s1'=2) & (bc1'=26)
+ 1/32 : (s1'=2) & (bc1'=27)
+ 1/32 : (s1'=2) & (bc1'=28)
+ 1/32 : (s1'=2) & (bc1'=29)
+ 1/32 : (s1'=2) & (bc1'=30)
+ 1/32 : (s1'=2) & (bc1'=31);
[sbc1] s1=1 & cd1=6 -> 1/64 : (s1'=2) & (bc1'=0)
+ 1/64 : (s1'=2) & (bc1'=1)
+ 1/64 : (s1'=2) & (bc1'=2)
+ 1/64 : (s1'=2) & (bc1'=3)
+ 1/64 : (s1'=2) & (bc1'=4)
+ 1/64 : (s1'=2) & (bc1'=5)
+ 1/64 : (s1'=2) & (bc1'=6)
+ 1/64 : (s1'=2) & (bc1'=7)
+ 1/64 : (s1'=2) & (bc1'=8)
+ 1/64 : (s1'=2) & (bc1'=9)
+ 1/64 : (s1'=2) & (bc1'=10)
+ 1/64 : (s1'=2) & (bc1'=11)
+ 1/64 : (s1'=2) & (bc1'=12)
+ 1/64 : (s1'=2) & (bc1'=13)
+ 1/64 : (s1'=2) & (bc1'=14)
+ 1/64 : (s1'=2) & (bc1'=15)
+ 1/64 : (s1'=2) & (bc1'=16)
+ 1/64 : (s1'=2) & (bc1'=17)
+ 1/64 : (s1'=2) & (bc1'=18)
+ 1/64 : (s1'=2) & (bc1'=19)
+ 1/64 : (s1'=2) & (bc1'=20)
+ 1/64 : (s1'=2) & (bc1'=21)
+ 1/64 : (s1'=2) & (bc1'=22)
+ 1/64 : (s1'=2) & (bc1'=23)
+ 1/64 : (s1'=2) & (bc1'=24)
+ 1/64 : (s1'=2) & (bc1'=25)
+ 1/64 : (s1'=2) & (bc1'=26)
+ 1/64 : (s1'=2) & (bc1'=27)
+ 1/64 : (s1'=2) & (bc1'=28)
+ 1/64 : (s1'=2) & (bc1'=29)
+ 1/64 : (s1'=2) & (bc1'=30)
+ 1/64 : (s1'=2) & (bc1'=31)
+ 1/64 : (s1'=2) & (bc1'=32)
+ 1/64 : (s1'=2) & (bc1'=33)
+ 1/64 : (s1'=2) & (bc1'=34)
+ 1/64 : (s1'=2) & (bc1'=35)
+ 1/64 : (s1'=2) & (bc1'=36)
+ 1/64 : (s1'=2) & (bc1'=37)
+ 1/64 : (s1'=2) & (bc1'=38)
+ 1/64 : (s1'=2) & (bc1'=39)
+ 1/64 : (s1'=2) & (bc1'=40)
+ 1/64 : (s1'=2) & (bc1'=41)
+ 1/64 : (s1'=2) & (bc1'=42)
+ 1/64 : (s1'=2) & (bc1'=43)
+ 1/64 : (s1'=2) & (bc1'=44)
+ 1/64 : (s1'=2) & (bc1'=45)
+ 1/64 : (s1'=2) & (bc1'=46)
+ 1/64 : (s1'=2) & (bc1'=47)
+ 1/64 : (s1'=2) & (bc1'=48)
+ 1/64 : (s1'=2) & (bc1'=49)
+ 1/64 : (s1'=2) & (bc1'=50)
+ 1/64 : (s1'=2) & (bc1'=51)
+ 1/64 : (s1'=2) & (bc1'=52)
+ 1/64 : (s1'=2) & (bc1'=53)
+ 1/64 : (s1'=2) & (bc1'=54)
+ 1/64 : (s1'=2) & (bc1'=55)
+ 1/64 : (s1'=2) & (bc1'=56)
+ 1/64 : (s1'=2) & (bc1'=57)
+ 1/64 : (s1'=2) & (bc1'=58)
+ 1/64 : (s1'=2) & (bc1'=59)
+ 1/64 : (s1'=2) & (bc1'=60)
+ 1/64 : (s1'=2) & (bc1'=61)
+ 1/64 : (s1'=2) & (bc1'=62)
+ 1/64 : (s1'=2) & (bc1'=63);
[sbc1] s1=1 & cd1=7 -> 1/128 : (s1'=2) & (bc1'=0)
+ 1/128 : (s1'=2) & (bc1'=1)
+ 1/128 : (s1'=2) & (bc1'=2)
+ 1/128 : (s1'=2) & (bc1'=3)
+ 1/128 : (s1'=2) & (bc1'=4)
+ 1/128 : (s1'=2) & (bc1'=5)
+ 1/128 : (s1'=2) & (bc1'=6)
+ 1/128 : (s1'=2) & (bc1'=7)
+ 1/128 : (s1'=2) & (bc1'=8)
+ 1/128 : (s1'=2) & (bc1'=9)
+ 1/128 : (s1'=2) & (bc1'=10)
+ 1/128 : (s1'=2) & (bc1'=11)
+ 1/128 : (s1'=2) & (bc1'=12)
+ 1/128 : (s1'=2) & (bc1'=13)
+ 1/128 : (s1'=2) & (bc1'=14)
+ 1/128 : (s1'=2) & (bc1'=15)
+ 1/128 : (s1'=2) & (bc1'=16)
+ 1/128 : (s1'=2) & (bc1'=17)
+ 1/128 : (s1'=2) & (bc1'=18)
+ 1/128 : (s1'=2) & (bc1'=19)
+ 1/128 : (s1'=2) & (bc1'=20)
+ 1/128 : (s1'=2) & (bc1'=21)
+ 1/128 : (s1'=2) & (bc1'=22)
+ 1/128 : (s1'=2) & (bc1'=23)
+ 1/128 : (s1'=2) & (bc1'=24)
+ 1/128 : (s1'=2) & (bc1'=25)
+ 1/128 : (s1'=2) & (bc1'=26)
+ 1/128 : (s1'=2) & (bc1'=27)
+ 1/128 : (s1'=2) & (bc1'=28)
+ 1/128 : (s1'=2) & (bc1'=29)
+ 1/128 : (s1'=2) & (bc1'=30)
+ 1/128 : (s1'=2) & (bc1'=31)
+ 1/128 : (s1'=2) & (bc1'=32)
+ 1/128 : (s1'=2) & (bc1'=33)
+ 1/128 : (s1'=2) & (bc1'=34)
+ 1/128 : (s1'=2) & (bc1'=35)
+ 1/128 : (s1'=2) & (bc1'=36)
+ 1/128 : (s1'=2) & (bc1'=37)
+ 1/128 : (s1'=2) & (bc1'=38)
+ 1/128 : (s1'=2) & (bc1'=39)
+ 1/128 : (s1'=2) & (bc1'=40)
+ 1/128 : (s1'=2) & (bc1'=41)
+ 1/128 : (s1'=2) & (bc1'=42)
+ 1/128 : (s1'=2) & (bc1'=43)
+ 1/128 : (s1'=2) & (bc1'=44)
+ 1/128 : (s1'=2) & (bc1'=45)
+ 1/128 : (s1'=2) & (bc1'=46)
+ 1/128 : (s1'=2) & (bc1'=47)
+ 1/128 : (s1'=2) & (bc1'=48)
+ 1/128 : (s1'=2) & (bc1'=49)
+ 1/128 : (s1'=2) & (bc1'=50)
+ 1/128 : (s1'=2) & (bc1'=51)
+ 1/128 : (s1'=2) & (bc1'=52)
+ 1/128 : (s1'=2) & (bc1'=53)
+ 1/128 : (s1'=2) & (bc1'=54)
+ 1/128 : (s1'=2) & (bc1'=55)
+ 1/128 : (s1'=2) & (bc1'=56)
+ 1/128 : (s1'=2) & (bc1'=57)
+ 1/128 : (s1'=2) & (bc1'=58)
+ 1/128 : (s1'=2) & (bc1'=59)
+ 1/128 : (s1'=2) & (bc1'=60)
+ 1/128 : (s1'=2) & (bc1'=61)
+ 1/128 : (s1'=2) & (bc1'=62)
+ 1/128 : (s1'=2) & (bc1'=63)
+ 1/128 : (s1'=2) & (bc1'=64)
+ 1/128 : (s1'=2) & (bc1'=65)
+ 1/128 : (s1'=2) & (bc1'=66)
+ 1/128 : (s1'=2) & (bc1'=67)
+ 1/128 : (s1'=2) & (bc1'=68)
+ 1/128 : (s1'=2) & (bc1'=69)
+ 1/128 : (s1'=2) & (bc1'=70)
+ 1/128 : (s1'=2) & (bc1'=71)
+ 1/128 : (s1'=2) & (bc1'=72)
+ 1/128 : (s1'=2) & (bc1'=73)
+ 1/128 : (s1'=2) & (bc1'=74)
+ 1/128 : (s1'=2) & (bc1'=75)
+ 1/128 : (s1'=2) & (bc1'=76)
+ 1/128 : (s1'=2) & (bc1'=77)
+ 1/128 : (s1'=2) & (bc1'=78)
+ 1/128 : (s1'=2) & (bc1'=79)
+ 1/128 : (s1'=2) & (bc1'=80)
+ 1/128 : (s1'=2) & (bc1'=81)
+ 1/128 : (s1'=2) & (bc1'=82)
+ 1/128 : (s1'=2) & (bc1'=83)
+ 1/128 : (s1'=2) & (bc1'=84)
+ 1/128 : (s1'=2) & (bc1'=85)
+ 1/128 : (s1'=2) & (bc1'=86)
+ 1/128 : (s1'=2) & (bc1'=87)
+ 1/128 : (s1'=2) & (bc1'=88)
+ 1/128 : (s1'=2) & (bc1'=89)
+ 1/128 : (s1'=2) & (bc1'=90)
+ 1/128 : (s1'=2) & (bc1'=91)
+ 1/128 : (s1'=2) & (bc1'=92)
+ 1/128 : (s1'=2) & (bc1'=93)
+ 1/128 : (s1'=2) & (bc1'=94)
+ 1/128 : (s1'=2) & (bc1'=95)
+ 1/128 : (s1'=2) & (bc1'=96)
+ 1/128 : (s1'=2) & (bc1'=97)
+ 1/128 : (s1'=2) & (bc1'=98)
+ 1/128 : (s1'=2) & (bc1'=99)
+ 1/128 : (s1'=2) & (bc1'=100)
+ 1/128 : (s1'=2) & (bc1'=101)
+ 1/128 : (s1'=2) & (bc1'=102)
+ 1/128 : (s1'=2) & (bc1'=103)
+ 1/128 : (s1'=2) & (bc1'=104)
+ 1/128 : (s1'=2) & (bc1'=105)
+ 1/128 : (s1'=2) & (bc1'=106)
+ 1/128 : (s1'=2) & (bc1'=107)
+ 1/128 : (s1'=2) & (bc1'=108)
+ 1/128 : (s1'=2) & (bc1'=109)
+ 1/128 : (s1'=2) & (bc1'=110)
+ 1/128 : (s1'=2) & (bc1'=111)
+ 1/128 : (s1'=2) & (bc1'=112)
+ 1/128 : (s1'=2) & (bc1'=113)
+ 1/128 : (s1'=2) & (bc1'=114)
+ 1/128 : (s1'=2) & (bc1'=115)
+ 1/128 : (s1'=2) & (bc1'=116)
+ 1/128 : (s1'=2) & (bc1'=117)
+ 1/128 : (s1'=2) & (bc1'=118)
+ 1/128 : (s1'=2) & (bc1'=119)
+ 1/128 : (s1'=2) & (bc1'=120)
+ 1/128 : (s1'=2) & (bc1'=121)
+ 1/128 : (s1'=2) & (bc1'=122)
+ 1/128 : (s1'=2) & (bc1'=123)
+ 1/128 : (s1'=2) & (bc1'=124)
+ 1/128 : (s1'=2) & (bc1'=125)
+ 1/128 : (s1'=2) & (bc1'=126)
+ 1/128 : (s1'=2) & (bc1'=127);
[sbc1] s1=1 & cd1=8 -> 1/256 : (s1'=2) & (bc1'=0)
+ 1/256 : (s1'=2) & (bc1'=1)
+ 1/256 : (s1'=2) & (bc1'=2)
+ 1/256 : (s1'=2) & (bc1'=3)
+ 1/256 : (s1'=2) & (bc1'=4)
+ 1/256 : (s1'=2) & (bc1'=5)
+ 1/256 : (s1'=2) & (bc1'=6)
+ 1/256 : (s1'=2) & (bc1'=7)
+ 1/256 : (s1'=2) & (bc1'=8)
+ 1/256 : (s1'=2) & (bc1'=9)
+ 1/256 : (s1'=2) & (bc1'=10)
+ 1/256 : (s1'=2) & (bc1'=11)
+ 1/256 : (s1'=2) & (bc1'=12)
+ 1/256 : (s1'=2) & (bc1'=13)
+ 1/256 : (s1'=2) & (bc1'=14)
+ 1/256 : (s1'=2) & (bc1'=15)
+ 1/256 : (s1'=2) & (bc1'=16)
+ 1/256 : (s1'=2) & (bc1'=17)
+ 1/256 : (s1'=2) & (bc1'=18)
+ 1/256 : (s1'=2) & (bc1'=19)
+ 1/256 : (s1'=2) & (bc1'=20)
+ 1/256 : (s1'=2) & (bc1'=21)
+ 1/256 : (s1'=2) & (bc1'=22)
+ 1/256 : (s1'=2) & (bc1'=23)
+ 1/256 : (s1'=2) & (bc1'=24)
+ 1/256 : (s1'=2) & (bc1'=25)
+ 1/256 : (s1'=2) & (bc1'=26)
+ 1/256 : (s1'=2) & (bc1'=27)
+ 1/256 : (s1'=2) & (bc1'=28)
+ 1/256 : (s1'=2) & (bc1'=29)
+ 1/256 : (s1'=2) & (bc1'=30)
+ 1/256 : (s1'=2) & (bc1'=31)
+ 1/256 : (s1'=2) & (bc1'=32)
+ 1/256 : (s1'=2) & (bc1'=33)
+ 1/256 : (s1'=2) & (bc1'=34)
+ 1/256 : (s1'=2) & (bc1'=35)
+ 1/256 : (s1'=2) & (bc1'=36)
+ 1/256 : (s1'=2) & (bc1'=37)
+ 1/256 : (s1'=2) & (bc1'=38)
+ 1/256 : (s1'=2) & (bc1'=39)
+ 1/256 : (s1'=2) & (bc1'=40)
+ 1/256 : (s1'=2) & (bc1'=41)
+ 1/256 : (s1'=2) & (bc1'=42)
+ 1/256 : (s1'=2) & (bc1'=43)
+ 1/256 : (s1'=2) & (bc1'=44)
+ 1/256 : (s1'=2) & (bc1'=45)
+ 1/256 : (s1'=2) & (bc1'=46)
+ 1/256 : (s1'=2) & (bc1'=47)
+ 1/256 : (s1'=2) & (bc1'=48)
+ 1/256 : (s1'=2) & (bc1'=49)
+ 1/256 : (s1'=2) & (bc1'=50)
+ 1/256 : (s1'=2) & (bc1'=51)
+ 1/256 : (s1'=2) & (bc1'=52)
+ 1/256 : (s1'=2) & (bc1'=53)
+ 1/256 : (s1'=2) & (bc1'=54)
+ 1/256 : (s1'=2) & (bc1'=55)
+ 1/256 : (s1'=2) & (bc1'=56)
+ 1/256 : (s1'=2) & (bc1'=57)
+ 1/256 : (s1'=2) & (bc1'=58)
+ 1/256 : (s1'=2) & (bc1'=59)
+ 1/256 : (s1'=2) & (bc1'=60)
+ 1/256 : (s1'=2) & (bc1'=61)
+ 1/256 : (s1'=2) & (bc1'=62)
+ 1/256 : (s1'=2) & (bc1'=63)
+ 1/256 : (s1'=2) & (bc1'=64)
+ 1/256 : (s1'=2) & (bc1'=65)
+ 1/256 : (s1'=2) & (bc1'=66)
+ 1/256 : (s1'=2) & (bc1'=67)
+ 1/256 : (s1'=2) & (bc1'=68)
+ 1/256 : (s1'=2) & (bc1'=69)
+ 1/256 : (s1'=2) & (bc1'=70)
+ 1/256 : (s1'=2) & (bc1'=71)
+ 1/256 : (s1'=2) & (bc1'=72)
+ 1/256 : (s1'=2) & (bc1'=73)
+ 1/256 : (s1'=2) & (bc1'=74)
+ 1/256 : (s1'=2) & (bc1'=75)
+ 1/256 : (s1'=2) & (bc1'=76)
+ 1/256 : (s1'=2) & (bc1'=77)
+ 1/256 : (s1'=2) & (bc1'=78)
+ 1/256 : (s1'=2) & (bc1'=79)
+ 1/256 : (s1'=2) & (bc1'=80)
+ 1/256 : (s1'=2) & (bc1'=81)
+ 1/256 : (s1'=2) & (bc1'=82)
+ 1/256 : (s1'=2) & (bc1'=83)
+ 1/256 : (s1'=2) & (bc1'=84)
+ 1/256 : (s1'=2) & (bc1'=85)
+ 1/256 : (s1'=2) & (bc1'=86)
+ 1/256 : (s1'=2) & (bc1'=87)
+ 1/256 : (s1'=2) & (bc1'=88)
+ 1/256 : (s1'=2) & (bc1'=89)
+ 1/256 : (s1'=2) & (bc1'=90)
+ 1/256 : (s1'=2) & (bc1'=91)
+ 1/256 : (s1'=2) & (bc1'=92)
+ 1/256 : (s1'=2) & (bc1'=93)
+ 1/256 : (s1'=2) & (bc1'=94)
+ 1/256 : (s1'=2) & (bc1'=95)
+ 1/256 : (s1'=2) & (bc1'=96)
+ 1/256 : (s1'=2) & (bc1'=97)
+ 1/256 : (s1'=2) & (bc1'=98)
+ 1/256 : (s1'=2) & (bc1'=99)
+ 1/256 : (s1'=2) & (bc1'=100)
+ 1/256 : (s1'=2) & (bc1'=101)
+ 1/256 : (s1'=2) & (bc1'=102)
+ 1/256 : (s1'=2) & (bc1'=103)
+ 1/256 : (s1'=2) & (bc1'=104)
+ 1/256 : (s1'=2) & (bc1'=105)
+ 1/256 : (s1'=2) & (bc1'=106)
+ 1/256 : (s1'=2) & (bc1'=107)
+ 1/256 : (s1'=2) & (bc1'=108)
+ 1/256 : (s1'=2) & (bc1'=109)
+ 1/256 : (s1'=2) & (bc1'=110)
+ 1/256 : (s1'=2) & (bc1'=111)
+ 1/256 : (s1'=2) & (bc1'=112)
+ 1/256 : (s1'=2) & (bc1'=113)
+ 1/256 : (s1'=2) & (bc1'=114)
+ 1/256 : (s1'=2) & (bc1'=115)
+ 1/256 : (s1'=2) & (bc1'=116)
+ 1/256 : (s1'=2) & (bc1'=117)
+ 1/256 : (s1'=2) & (bc1'=118)
+ 1/256 : (s1'=2) & (bc1'=119)
+ 1/256 : (s1'=2) & (bc1'=120)
+ 1/256 : (s1'=2) & (bc1'=121)
+ 1/256 : (s1'=2) & (bc1'=122)
+ 1/256 : (s1'=2) & (bc1'=123)
+ 1/256 : (s1'=2) & (bc1'=124)
+ 1/256 : (s1'=2) & (bc1'=125)
+ 1/256 : (s1'=2) & (bc1'=126)
+ 1/256 : (s1'=2) & (bc1'=127)
+ 1/256 : (s1'=2) & (bc1'=128)
+ 1/256 : (s1'=2) & (bc1'=129)
+ 1/256 : (s1'=2) & (bc1'=130)
+ 1/256 : (s1'=2) & (bc1'=131)
+ 1/256 : (s1'=2) & (bc1'=132)
+ 1/256 : (s1'=2) & (bc1'=133)
+ 1/256 : (s1'=2) & (bc1'=134)
+ 1/256 : (s1'=2) & (bc1'=135)
+ 1/256 : (s1'=2) & (bc1'=136)
+ 1/256 : (s1'=2) & (bc1'=137)
+ 1/256 : (s1'=2) & (bc1'=138)
+ 1/256 : (s1'=2) & (bc1'=139)
+ 1/256 : (s1'=2) & (bc1'=140)
+ 1/256 : (s1'=2) & (bc1'=141)
+ 1/256 : (s1'=2) & (bc1'=142)
+ 1/256 : (s1'=2) & (bc1'=143)
+ 1/256 : (s1'=2) & (bc1'=144)
+ 1/256 : (s1'=2) & (bc1'=145)
+ 1/256 : (s1'=2) & (bc1'=146)
+ 1/256 : (s1'=2) & (bc1'=147)
+ 1/256 : (s1'=2) & (bc1'=148)
+ 1/256 : (s1'=2) & (bc1'=149)
+ 1/256 : (s1'=2) & (bc1'=150)
+ 1/256 : (s1'=2) & (bc1'=151)
+ 1/256 : (s1'=2) & (bc1'=152)
+ 1/256 : (s1'=2) & (bc1'=153)
+ 1/256 : (s1'=2) & (bc1'=154)
+ 1/256 : (s1'=2) & (bc1'=155)
+ 1/256 : (s1'=2) & (bc1'=156)
+ 1/256 : (s1'=2) & (bc1'=157)
+ 1/256 : (s1'=2) & (bc1'=158)
+ 1/256 : (s1'=2) & (bc1'=159)
+ 1/256 : (s1'=2) & (bc1'=160)
+ 1/256 : (s1'=2) & (bc1'=161)
+ 1/256 : (s1'=2) & (bc1'=162)
+ 1/256 : (s1'=2) & (bc1'=163)
+ 1/256 : (s1'=2) & (bc1'=164)
+ 1/256 : (s1'=2) & (bc1'=165)
+ 1/256 : (s1'=2) & (bc1'=166)
+ 1/256 : (s1'=2) & (bc1'=167)
+ 1/256 : (s1'=2) & (bc1'=168)
+ 1/256 : (s1'=2) & (bc1'=169)
+ 1/256 : (s1'=2) & (bc1'=170)
+ 1/256 : (s1'=2) & (bc1'=171)
+ 1/256 : (s1'=2) & (bc1'=172)
+ 1/256 : (s1'=2) & (bc1'=173)
+ 1/256 : (s1'=2) & (bc1'=174)
+ 1/256 : (s1'=2) & (bc1'=175)
+ 1/256 : (s1'=2) & (bc1'=176)
+ 1/256 : (s1'=2) & (bc1'=177)
+ 1/256 : (s1'=2) & (bc1'=178)
+ 1/256 : (s1'=2) & (bc1'=179)
+ 1/256 : (s1'=2) & (bc1'=180)
+ 1/256 : (s1'=2) & (bc1'=181)
+ 1/256 : (s1'=2) & (bc1'=182)
+ 1/256 : (s1'=2) & (bc1'=183)
+ 1/256 : (s1'=2) & (bc1'=184)
+ 1/256 : (s1'=2) & (bc1'=185)
+ 1/256 : (s1'=2) & (bc1'=186)
+ 1/256 : (s1'=2) & (bc1'=187)
+ 1/256 : (s1'=2) & (bc1'=188)
+ 1/256 : (s1'=2) & (bc1'=189)
+ 1/256 : (s1'=2) & (bc1'=190)
+ 1/256 : (s1'=2) & (bc1'=191)
+ 1/256 : (s1'=2) & (bc1'=192)
+ 1/256 : (s1'=2) & (bc1'=193)
+ 1/256 : (s1'=2) & (bc1'=194)
+ 1/256 : (s1'=2) & (bc1'=195)
+ 1/256 : (s1'=2) & (bc1'=196)
+ 1/256 : (s1'=2) & (bc1'=197)
+ 1/256 : (s1'=2) & (bc1'=198)
+ 1/256 : (s1'=2) & (bc1'=199)
+ 1/256 : (s1'=2) & (bc1'=200)
+ 1/256 : (s1'=2) & (bc1'=201)
+ 1/256 : (s1'=2) & (bc1'=202)
+ 1/256 : (s1'=2) & (bc1'=203)
+ 1/256 : (s1'=2) & (bc1'=204)
+ 1/256 : (s1'=2) & (bc1'=205)
+ 1/256 : (s1'=2) & (bc1'=206)
+ 1/256 : (s1'=2) & (bc1'=207)
+ 1/256 : (s1'=2) & (bc1'=208)
+ 1/256 : (s1'=2) & (bc1'=209)
+ 1/256 : (s1'=2) & (bc1'=210)
+ 1/256 : (s1'=2) & (bc1'=211)
+ 1/256 : (s1'=2) & (bc1'=212)
+ 1/256 : (s1'=2) & (bc1'=213)
+ 1/256 : (s1'=2) & (bc1'=214)
+ 1/256 : (s1'=2) & (bc1'=215)
+ 1/256 : (s1'=2) & (bc1'=216)
+ 1/256 : (s1'=2) & (bc1'=217)
+ 1/256 : (s1'=2) & (bc1'=218)
+ 1/256 : (s1'=2) & (bc1'=219)
+ 1/256 : (s1'=2) & (bc1'=220)
+ 1/256 : (s1'=2) & (bc1'=221)
+ 1/256 : (s1'=2) & (bc1'=222)
+ 1/256 : (s1'=2) & (bc1'=223)
+ 1/256 : (s1'=2) & (bc1'=224)
+ 1/256 : (s1'=2) & (bc1'=225)
+ 1/256 : (s1'=2) & (bc1'=226)
+ 1/256 : (s1'=2) & (bc1'=227)
+ 1/256 : (s1'=2) & (bc1'=228)
+ 1/256 : (s1'=2) & (bc1'=229)
+ 1/256 : (s1'=2) & (bc1'=230)
+ 1/256 : (s1'=2) & (bc1'=231)
+ 1/256 : (s1'=2) & (bc1'=232)
+ 1/256 : (s1'=2) & (bc1'=233)
+ 1/256 : (s1'=2) & (bc1'=234)
+ 1/256 : (s1'=2) & (bc1'=235)
+ 1/256 : (s1'=2) & (bc1'=236)
+ 1/256 : (s1'=2) & (bc1'=237)
+ 1/256 : (s1'=2) & (bc1'=238)
+ 1/256 : (s1'=2) & (bc1'=239)
+ 1/256 : (s1'=2) & (bc1'=240)
+ 1/256 : (s1'=2) & (bc1'=241)
+ 1/256 : (s1'=2) & (bc1'=242)
+ 1/256 : (s1'=2) & (bc1'=243)
+ 1/256 : (s1'=2) & (bc1'=244)
+ 1/256 : (s1'=2) & (bc1'=245)
+ 1/256 : (s1'=2) & (bc1'=246)
+ 1/256 : (s1'=2) & (bc1'=247)
+ 1/256 : (s1'=2) & (bc1'=248)
+ 1/256 : (s1'=2) & (bc1'=249)
+ 1/256 : (s1'=2) & (bc1'=250)
+ 1/256 : (s1'=2) & (bc1'=251)
+ 1/256 : (s1'=2) & (bc1'=252)
+ 1/256 : (s1'=2) & (bc1'=253)
+ 1/256 : (s1'=2) & (bc1'=254)
+ 1/256 : (s1'=2) & (bc1'=255);
// backs off
[boff1] tick & s1=2 & bc1>0 -> (bc1'=bc1-1); // decrement counter
[boff1] tick & s1=2 & bc1=0 -> (tr1'=1) & (s1'=0); // finish backoff so transmit again

endmodule

// construct further users through renaming
// (need to rename s2, s3, tr2 and tr3 as they appear in formulae)
module user2=user1[s1=s2,s2=s1,tr1=tr2,tr2=tr1,bc1=bc2,cd1=cd2,wait1=wait2,trans1=trans2,try1=try2,boff1=boff2,sbc1=sbc2,t1=t2] endmodule
module user3=user1[s1=s3,s3=s1,tr1=tr3,tr3=tr1,bc1=bc3,cd1=cd3,wait1=wait3,trans1=trans3,try1=try3,boff1=boff3,sbc1=sbc3,t1=t3] endmodule

// module for counting when time passes (slots)
module timer

t : [0..D+1];

[] tick -> (t'=min(D+1,t+1));

endmodule

// reward structure for time passage
rewards "time"
tick : 1;
endrewards
```

### Zero-Sum Properties

We first consider zero-sum properties in which some of the users try to send their packets and the others try to prevent this from happening. We consider the following properties:

• minimising the expected time for a coalition of users to send their packets;
• maximising the probability for a coalition of users to send their packets by a deadline.

These properties are formally specified as follows for the case of three users, where the coalition is either just the first user or the second and third users.

```// minimum expected time user 1 can guarantee to eventually send a packet
<<usr1>>R{"time"}min=?[F s1=3]

// minimum expected time users 2 and 3 can guarantee to eventually send their packets
<<usr2,usr3>>R{"time"}min=?[F s2=3 & s3=3]

// maximum probability user 1 can guarantee to send a packet within a deadline
<<usr1>>Pmax=?[F (s1=3 & t<=D)]

// maximum probability users 2 and 3 can guarantee to send their packets within a deadline
<<usr2,usr3>>Pmax=?[F (s2=3 & s3=3 & t<=D)]
```

Considering the minimum expected time that a coalition can guarantee of eventually sending their packets, the following graphs plot the results for the coalition of only user 1 (left) and the coalition of users 2 and 3 (right) as q and bcmax vary.

The results demonstrate that the expected time increases as the probability a packet is correctly sent decreases and the maximum value of the backoff counter increases. We also see that the expected time for the second coalition is larger, which is two be expected as this coalition consists of two users, rather than one, and therefore is the minimum expected time that can be guaranteed for two packets to be sent.

The graphs below plot the results for both the step-bounded property for the different coalitions of user 1 (left) and users 1 and 2 (right) as q and D vary for bcmax=1, 2 and 4.

### Nonzero-Sum Properties

We next consider nonzero-sum properties where two coalitions (the first user in a coalition on its own and the second and third users in a separate coalition) try and reach their individual goals. Again we consider two classes of properties:

• each coalition minimising the expected time to send their packets;
• each coalition maximising the probability of sending their packets by a deadline.
```// expected time user 1 eventually sends a packet
// and users 2 and 3 form a coalition to send their packets
<<usr1:usr2,usr3>>min=? (R{"time"}[F s1=3] + R{"time"}[F s2=3 & s3=3])

// probability user 1 eventually sends a packet by a deadline
// and users 2 and 3 form a coalition to send their packets by a deadline
<<usr1:usr2,usr3>>max=? (P[F (s1=3 & t<=D)] + P[F (s2=3 & s3=3 & t<=D)])
```