www.prismmodelchecker.org

Aloha Protocol

Contents

Related publications: [KNPS19]

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);

const int D; // deadline

// 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
View: printable version          Download: aloha_backoff3.prism

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)]
View: printable version          Download: aloha_backoff3_zero.props

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.

plot: the minimum expected time that player 1 can guantee of eventually sending its packet    plot: the minimum expected time that the coalition of players 2 and 3 can guantee of eventually sending their packets

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.

plot: maximum probability user 1 can ensure they send the packet within a deadline (bcmax=1)    plot: maximum probability users 2 and 3 can ensure they send their packets within a deadline (bcmax=1)

plot: maximum probability user 1 can ensure they send the packet within a deadline (bcmax=2)    plot: maximum probability users 2 and 3 can ensure they send their packets within a deadline (bcmax=2)

plot: maximum probability user 1 can ensure they send the packet within a deadline (bcmax=4)    plot: maximum probability users 2 and 3 can ensure they send their packets within a deadline (bcmax=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)])
View: printable version          Download: aloha_backoff3_nonzero.props

Through strategy synthesis, we find the collaboration is dependent on q and, in the case of deadline properties, D. In particular, given more time (i.e., larger values of D), there is more chance for the users to collaborate sending in different slots. While, if q is large, it is unlikely users need to repeatedly try and send their packets, and therefore again can send in different slots. As the coalition has more messages to send, their probabilities are lower. However, even for two users, the probabilities are different, since, although it is advantageous to collaborate and only one user tries first, if transmission fails, then both users try to send as this is the best option for their individual goals.

plot: the minimum expected time of player 1 eventually sending its packet    plot: the minimum expected time of the coalition of players 2 and 3 eventually sending their packets
plot: maximum probability user 1 sends their packet within a deadline (bcmax=1)    plot: maximum probability users 2 and 3 send their packets within a deadline (bcmax=1)

plot: maximum probability user 1 sends their packet within a deadline (bcmax=2)    plot: maximum probability users 2 and 3 send their packets within a deadline (bcmax=2)

plot: maximum probability user 1 sends their packet within a deadline (bcmax=1)    plot: maximum probability users 2 and 3 send their packets within a deadline (bcmax=4)

Case Studies