Related publications: [KNS02a]
This case study concerns probabilistic model checking of certain aspects of the IEEE 802.11 Wireless LAN. The international standard IEEE 802.11 was developed recently in recognition of the increased demand for wireless local area networks which permit interoperability of heterogeneous communication devices. In contrast to wired devices, stations of a wireless network cannot listen to their own transmission, and are therefore unable to employ medium access control schemes such as Carrier Sense Multiple Access with Collision Detection (CSMA/CD) in order to prevent simultaneous transmission on the channel. Instead, the IEEE 802.11 standard describes a Carrier Sense Multiple Access with Collision Avoidance (CSMA/CA) mechanism, using a randomised exponential backoff rule to minimise the likelihood of transmission collision.
We model a two-way handshake mechanism of the IEEE 802.11 medium access control scheme, operating in a fixed network topology, using the modelling formalism of probabilistic timed automata. This formalism allows both nondeterministic choice (which, for example, can be used to model the unspecified data packet length) and probabilistic choice (which, for example, is present in the randomised backoff procedure) to coexist in the same model.
We consider a probabilistic timed automata model WLAN of the IEEE 802.11 Wireless LAN which models two stations colliding - trying to send messages at the same time - and then entering the randomised exponential backoff procedure. The timing constraints of the model correspond to the Frequency Hopping Spread Spectrum (FHSS) physical layer, rounded by a factor of 50 (i.e. 1 time unit equals 50 μs) to reduce complexity. We constructed an MDP of the model using the integer semantics given in [KNS02a].
The mode consists of three components operating in parallel, namely chan (the channel) and sender_i for i=1,2 (the sending stations).
The probabilistic timed automaton representing the channel is shown in below. This automaton has two variables c1 and c2 which record the status of the packet being sent by station 1 and station 2 respectively, and which are updated both when a station starts sending a packet (event send) and when a station finishes sending a packet (event finish). These variables have the following interpretation: ci=0 - nothing being sent by station i; ci=1 - packet from station i being sent correctly; ci=2 - packet from station i being sent garbled.
The probabilistic timed automaton sender_1 representing station 1 is shown below and the automaton for station 2 is symmetric. The sender begins in SENSE with a data packet ready to send, and senses the channel. If the channel remains free for DIFS, then the sender enters its vulnerable period and starts sending a packet (event send), otherwise the station enters backoff via an urgent transition. The time taken to send a packet is nondeterministic (within TTMIN and TTMAX). The success of the transmission depends on whether a collision has occurred, and is recorded by setting the variable status to the value of the channel variable c1. The sender then immediately tests the channel (represented by the urgent location TESTC). If the channel is busy, the sender enters the backoff procedure, otherwise it waits for an acknowledgement. If the packet was sent correctly (status=1), then the destination station waits for SIFS and sends the acknowledgement; the sending station then receives this acknowledgement and finishes. On the other hand, if the packet was not sent correctly (status=2), then the destination station does nothing. In this case, the sender times-out and enters the backoff procedure.
In the backoff procedure, the sender first waits for the channel to be free for DIFS and then sets its backoff value according to the random assignment backoff:=RAND(bc) The automaton then decrements backoff by 1 if the channel remains free for ASLOT. However, if the channel is sensed busy within this slot, it waits until the channel becomes free and then waits for DIFS before resuming its backoff procedure. When the value of backoff reaches 0 the sender starts re-sending its data packet.
We use the parameters of the Frequency Hopping Spread Spectrum (FHSS) physical layer, with a transmission bit rate of 2Mbps for the data payload, as given below.
| variable | description | value |
| ASLOT | ength of each backoff slot | 50μs |
| CCA | time receiver needs to asses the medium | 27μs |
| Turnaround | time a station needs to change from receiving to sending | 20μs |
| SIFS | short interframe space | 28μs |
| DIFS | DCF interframe space | 128μs |
| TT_MIN | minimum time to send a packet | 224μs |
| TT_MAX | maximum time to send a packet | 15,717μs |
| ACK | time to send an acknowledgement | 205μs |
| ACK_TO | time sender waits for acknowledgement before timing-out | 300μs |
| AIRPROP | the air propagation time | 1μs |
| VULN | vulnerable period (AIRPROP+CCA+Turnaround) | 48μs |
The PRISM source code for this model is given below.
// WLAN PROTOCOL (two stations) // discrete time model // gxn/jzs 20/02/02 mdp // TIMING CONSTRAINTS // we have used the FHSS parameters // then scaled by the value of ASLOTTIME const int ASLOTTIME = 1; const int DIFS = 3; // due to scaling can be non-deterministically either 2 or 3 const int VULN = 1; // due to scaling can be non-deterministically either 0 or 1 const int TRANS_TIME_MAX = 315; // scaling up const int TRANS_TIME_MIN = 4; // scaling down const int ACK_TO = 6; const int ACK = 4; // due to scaling can be non-deterministically either 3 or 4 const int SIFS = 1; // due to scaling can be non-deterministically either 0 or 1 const int TIME_MAX = 315; // maximum constant used in timing constraints + 1 const int BOFF = 6; // max backoff (since contention window is [15,1023]) // THE MEDIUM/CHANNEL formula busy = c1>0 | c2>0; // channel is busy formula free = c1=0 & c2=0; // channel is free module medium col : [0..8]; // number of collisions // medium status c1 : [0..2]; c2 : [0..2]; // ci corresponds to messages associated with station i // 0 nothing being sent // 1 being sent correctly // 2 being sent garbled // begin sending message and nothing else currently being sent [send1] c1=0 & c2=0 -> (c1'=1); [send2] c2=0 & c1=0 -> (c2'=1); // begin sending message and something is already being sent // in this case both messages become garbled [send1] c1=0 & c2>0 -> (c1'=2) & (c2'=2) & col'=min(col+1,8); [send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2) & col'=min(col+1,8); // finish sending message [finish1] c1>0 -> (c1'=0); [finish2] c2>0 -> (c2'=0); endmodule // STATION 1 module station1 // clock for station 1 x1 : [0..TIME_MAX]; // local state s1 : [1..12]; // 1 sense // 2 wait until free before setting backoff // 3 wait for DIFS then set slot // 4 set backoff // 5 backoff // 6 wait until free in backoff // 7 wait for DIFS then resume backoff // 8 vulnerable // 9 transmit // 11 wait for SIFS and then ACK // 10 wait for ACT_TO // 12 done // BACKOFF // separate into slots slot1 : [0..63]; backoff1 : [0..15]; // BACKOFF COUNTER bc1 : [0..BOFF]; // SENSE // let time pass [time] s1=1 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX)); // ready to transmit [] s1=1 & (x1=DIFS | x1=DIFS-1) -> (s1'=8) & (x1'=0); // found channel busy so wait until free [] s1=1 & busy -> (s1'=2) & (x1'=0); // WAIT UNTIL FREE BEFORE SETTING BACKOFF // let time pass (no need for the clock x1 to change) [time] s1=2 & busy -> (s1'=2); // find that channel is free so check its free for DIFS before setting backoff [] s1=2 & free -> (s1'=3); // WAIT FOR DIFS THEN SET BACKOFF // let time pass [time] s1=3 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX)); // found channel busy so wait until free [] s1=3 & busy -> (s1'=2) & (x1'=0); // start backoff first uniformly choose slot // backoff counter 0 [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=0 -> (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,BOFF)); // backoff counter 1 [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=1 -> 1/2 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,BOFF)) + 1/2 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,BOFF)); // backoff counter 2 [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=2 -> 1/4 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,BOFF)) + 1/4 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,BOFF)) + 1/4 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,BOFF)) + 1/4 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,BOFF)); // backoff counter 3 [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=3 -> 1/8 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,BOFF)) + 1/8 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,BOFF)) + 1/8 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,BOFF)) + 1/8 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,BOFF)) + 1/8 : (s1'=4) & (x1'=0) & (slot1'=4) & (bc1'=min(bc1+1,BOFF)) + 1/8 : (s1'=4) & (x1'=0) & (slot1'=5) & (bc1'=min(bc1+1,BOFF)) + 1/8 : (s1'=4) & (x1'=0) & (slot1'=6) & (bc1'=min(bc1+1,BOFF)) + 1/8 : (s1'=4) & (x1'=0) & (slot1'=7) & (bc1'=min(bc1+1,BOFF)); // backoff counter 4 [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=4 -> 1/16 : (s1'=4) & (x1'=0) & (slot1'=0 ) & (bc1'=min(bc1+1,BOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=1 ) & (bc1'=min(bc1+1,BOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=2 ) & (bc1'=min(bc1+1,BOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=3 ) & (bc1'=min(bc1+1,BOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=4 ) & (bc1'=min(bc1+1,BOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=5 ) & (bc1'=min(bc1+1,BOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=6 ) & (bc1'=min(bc1+1,BOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=7 ) & (bc1'=min(bc1+1,BOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=8 ) & (bc1'=min(bc1+1,BOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=9 ) & (bc1'=min(bc1+1,BOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=10) & (bc1'=min(bc1+1,BOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=11) & (bc1'=min(bc1+1,BOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=12) & (bc1'=min(bc1+1,BOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=13) & (bc1'=min(bc1+1,BOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=14) & (bc1'=min(bc1+1,BOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=15) & (bc1'=min(bc1+1,BOFF)); // backoff counter 5 [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=5 -> 1/32 : (s1'=4) & (x1'=0) & (slot1'=0 ) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=1 ) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=2 ) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=3 ) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=4 ) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=5 ) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=6 ) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=7 ) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=8 ) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=9 ) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=10) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=11) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=12) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=13) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=14) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=15) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=16) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=17) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=18) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=19) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=20) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=21) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=22) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=23) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=24) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=25) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=26) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=27) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=28) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=29) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=30) & (bc1'=min(bc1+1,BOFF)) + 1/32 : (s1'=4) & (x1'=0) & (slot1'=31) & (bc1'=min(bc1+1,BOFF)); // backoff counter 6 [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=6 -> 1/64 : (s1'=4) & (x1'=0) & (slot1'=0 ) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=1 ) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=2 ) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=3 ) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=4 ) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=5 ) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=6 ) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=7 ) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=8 ) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=9 ) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=10) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=11) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=12) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=13) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=14) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=15) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=16) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=17) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=18) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=19) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=20) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=21) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=22) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=23) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=24) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=25) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=26) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=27) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=28) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=29) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=30) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=31) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=32) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=33) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=34) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=35) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=36) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=37) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=38) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=39) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=40) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=41) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=42) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=43) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=44) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=45) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=46) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=47) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=48) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=49) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=50) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=51) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=52) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=53) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=54) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=55) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=56) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=57) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=58) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=59) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=60) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=61) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=62) & (bc1'=min(bc1+1,BOFF)) + 1/64 : (s1'=4) & (x1'=0) & (slot1'=63) & (bc1'=min(bc1+1,BOFF)); // SET BACKOFF (no time can pass) // chosen slot now set backoff [] s1=4 -> 1/16 : (s1'=5) & (backoff1'=0) + 1/16 : (s1'=5) & (backoff1'=1) + 1/16 : (s1'=5) & (backoff1'=2) + 1/16 : (s1'=5) & (backoff1'=3) + 1/16 : (s1'=5) & (backoff1'=4) + 1/16 : (s1'=5) & (backoff1'=5) + 1/16 : (s1'=5) & (backoff1'=6) + 1/16 : (s1'=5) & (backoff1'=7) + 1/16 : (s1'=5) & (backoff1'=8) + 1/16 : (s1'=5) & (backoff1'=9) + 1/16 : (s1'=5) & (backoff1'=10) + 1/16 : (s1'=5) & (backoff1'=11) + 1/16 : (s1'=5) & (backoff1'=12) + 1/16 : (s1'=5) & (backoff1'=13) + 1/16 : (s1'=5) & (backoff1'=14) + 1/16 : (s1'=5) & (backoff1'=15); // BACKOFF // let time pass [time] s1=5 & x1<ASLOTTIME & free -> (x1'=min(x1+1,TIME_MAX)); // decrement backoff [] s1=5 & x1=ASLOTTIME & backoff1>0 -> (s1'=5) & (x1'=0) & (backoff1'=backoff1-1); [] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1>0 -> (s1'=5) & (x1'=0) & (backoff1'=15) & (slot1'=slot1-1); // finish backoff [] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1=0 -> (s1'=8) & (x1'=0); // found channel busy [] s1=5 & busy -> (s1'=6) & (x1'=0); // WAIT UNTIL FREE IN BACKOFF // let time pass (no need for the clock x1 to change) [time] s1=6 & busy -> (s1'=6); // find that channel is free [] s1=6 & free -> (s1'=7); // WAIT FOR DIFS THEN RESUME BACKOFF // let time pass [time] s1=7 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX)); // resume backoff (start again from previous backoff) [] s1=7 & (x1=DIFS | x1=DIFS-1) -> (s1'=5) & (x1'=0); // found channel busy [] s1=7 & busy -> (s1'=6) & (x1'=0); // VULNERABLE // let time pass [time] s1=8 & x1<VULN -> (x1'=min(x1+1,TIME_MAX)); // move to transmit [send1] s1=8 & (x1=VULN | x1=VULN-1) -> (s1'=9) & (x1'=0); // TRANSMIT // let time pass [time] s1=9 & x1<TRANS_TIME_MAX -> (x1'=min(x1+1,TIME_MAX)); // finish transmission successful [finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=1 -> (s1'=10) & (x1'=0); // finish transmission garbled [finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=2 -> (s1'=11) & (x1'=0); // WAIT FOR SIFS THEN WAIT FOR ACK // WAIT FOR SIFS i.e. c1=0 // check channel and busy: go into backoff [] s1=10 & c1=0 & x1=0 & busy -> (s1'=2); // chack channel and free: let time pass [time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); // let time pass [time] s1=10 & c1=0 & x1>0 & x1<SIFS -> (x1'=min(x1+1,TIME_MAX)); // ack is sent after SIFS (since SIFS-1=0 add condition that channel is free) [send1] s1=10 & c1=0 & (x1=SIFS | (x1=SIFS-1 & free)) -> (s1'=10) & (x1'=0); // WAIT FOR ACK i.e. c1=1 // let time pass [time] s1=10 & c1=1 & x1<ACK -> (x1'=min(x1+1,TIME_MAX)); // get acknowledgement so packet sent correctly and move to done [finish1] s1=10 & c1=1 & (x1=ACK | x1=ACK-1) -> (s1'=12) & (x1'=0) & (bc1'=0); // WAIT FOR ACK_TO // check channel and busy: go into backoff [] s1=11 & x1=0 & busy -> (s1'=2); // check channel and free: let time pass [time] s1=11 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); // let time pass [time] s1=11 & x1>0 & x1<ACK_TO -> (x1'=min(x1+1,TIME_MAX)); // no acknowledgement (go to backoff waiting DIFS first) [] s1=11 & x1=ACK_TO -> (s1'=3) & (x1'=0); // DONE [time] s1=12 -> (s1'=12); endmodule // STATION 2 (rename STATION 1) module station2=station1[x1=x2, s1=s2, s2=s1, c1=c2, c2=c1, slot1=slot2, backoff1=backoff2, bc1=bc2, send1=send2, finish1=finish2] endmodule // reward structure for expected number of collisions rewards "collisions" [send1] c1=0 & c2>0 : 1; // station one starts transmitting and station two is already transmitting [send2] c2=0 & c1>0 : 1; // station two starts transmitting and station one is already transmitting endrewards // reward structure for expected time // recall one time unit equals ASLOT(=50μs) rewards "time" [time] true : 50; endrewards // reward strcuture for expected cost // cost (per time unit) is set to: // 1 in locations where the channel is free, // 10 in locations where the channel is in use and a message is being sent correctly // 1000 in locations where a station is sending a garbled message // 2000 in locations where both stations are sending garbled messages rewards "cost" [time] c1=0 & c2=0 : 50; [time] c1=1 & c2=0 : 50*10; [time] c1=0 & c2=1 : 50*10; [time] c1=1 & c2=1 : 50*20; [time] c1=0 & c2=2 & bc1=0 & bc2=0 : 50*10; [time] c1=2 & c2=0 & bc1=0 & bc2=0 : 50*10; [time] c1=2 & c2=2 & bc1=0 & bc2=0 : 50*20; [time] c1=0 & c2=2 & (bc1>0 | bc2>0) : 50*1000; [time] c1=2 & c2=0 & (bc1>0 | bc2>0) : 50*1000; [time] c1=2 & c2=2 & (bc1>0 | bc2>0) : 50*2000; endrewards
When checking probabilistic reachability and expected reachability properties we vary the value of bcmax (the maximum value a station's backoff counter can take) from 0 up to 6. A station increases its backoff counter (up to the value of bcmax) each time a collision occurs and that the value of the backoff counter influences the range over which its next backoff is chosen. More precisely, a station's chooses its next backoff value uniformly from the range {0,1,..., 2(k+4-1)} when its backoff counter equals k.
When checking deadline properties (by adding an extra clock to the model and preventing progress once the clock reaches a certain deadline) we consider different values of TT_MAX, in particular the values 500, 1,250 and 2,500 (again rounding by a factor of 50 to reduce complexity).
For details on the correctness of the integer semantics when verifying probabilistic timed automata against performance measures see [KNPS06].
The tables below shows statistics for each model we have built. The first section gives the number of states in the MDP representing the model. The second part refers to the MTBDD which represents this MDP: the total number of nodes and the number of leaves (terminal nodes).
| bcmax: | States: | Nodes: | Leaves: | |
| 0 | 16,069 | 31,540 | 3 | |
| 1 | 34,855 | 39,436 | 4 | |
| 2 | 87,345 | 54,130 | 5 | |
| 3 | 217,082 | 64,756 | 6 | |
| 4 | 586,255 | 81,684 | 6 | |
| 5 | 1,774,068 | 92,744 | 7 | |
| 6 | 5,958,233 | 105,876 | 8 |
Deadline Models:
| TT_MAX=500 | ||||
| DEADLINE (μs): | States: | Nodes: | Leaves: | |
| 2,500 | 478,881 | 65,797 | 6 | |
| 5,000 | 71,521,898 | 153,032 | 8 | |
| 10,000 | 569,487,340 | 267,961 | 8 | |
| TT_MAX=1,250 | ||||
| DEADLINE (μs): | States: | Nodes: | Leaves: | |
| 2,500 | 534,850 | 71,822 | 6 | |
| 5,000 | 72,262,456 | 176,932 | 8 | |
| 10,000 | 575,779,335 | 361,675 | 8 | |
| TT_MAX=2,500 | ||||
| DEADLINE (μs): | States: | Nodes: | Leaves: | |
| 2,500 | 557,141 | 82,459 | 6 | |
| 5,000 | 72,676,168 | 216,971 | 8 | |
| 10,000 | 583,661,380 | 415,007 | 8 | |
The tables below gives the times taken to construct the models. There are two stages. Firstly, the system description (in our module based language) is parsed and converted to the MTBDD representing it. Secondly, reachability is performed to identify non-reachable states and the MTBDD is filtered accordingly. Reachability is performed using a BDD based fixpoint algorithm. The number of iterations for this process is also given.
| bcmax: | Construction: | Reachability: | |||
| Time (s): | Iter.s: | Time per iter. (s): | |||
| 0 | 8.39 | 346 | 0.0186 | ||
| 1 | 11.8 | 371 | 0.0268 | ||
| 2 | 17.4 | 396 | 0.0380 | ||
| 3 | 23.0 | 421 | 0.0493 | ||
| 4 | 29.0 | 446 | 0.0583 | ||
| 5 | 35.8 | 471 | 0.0681 | ||
| 6 | 44.3 | 496 | 0.0794 | ||
Deadline Models:
| TT_MAX=500 | ||||
| DEADLINE (μs): | Construction: | Reachability: | ||
| Time (s): | Iter.s: | Time per iter. (s): | ||
| 2,500 | 11.8 | 100 | 0.104 | |
| 5,000 | 61.2 | 222 | 0.253 | |
| 10,000 | 243 | 477 | 0.481 | |
| TT_MAX=1,250 | ||||
| DEADLINE (μs): | Construction: | Reachability: | ||
| Time (s): | Iter.s: | Time per iter. (s): | ||
| 2,500 | 13.4 | 99 | 0.121 | |
| 5,000 | 72.9 | 196 | 0.339 | |
| 10,000 | 472 | 417 | 1.03 | |
| TT_MAX=2,500 | ||||
| DEADLINE (μs): | Construction: | Reachability: | ||
| Time (s): | Iter.s: | Time per iter. (s): | ||
| 2,500 | 16.8 | 99 | 0.153 | |
| 5,000 | 94.9 | 196 | 0.459 | |
| 10,000 | 482 | 322 | 1.41 | |
We now report on the model checking results obtained using PRISM when considering a number of different parameters. We consider three different types performance measures:
Due to the size of the deadline models, all experiments on these models were performed with PRISM's MTBDD engine.
Probabilistic reachability: The following probabilistic reachability properties have been verified.
"With probability 1, eventually both stations have sent their packet correctly." In PCTL this is expressed by:
Model checking times:
| bcmax: | Iterations: | Time per iter. (s): | |
| 0 | 1,049 | 0.0158 | |
| 1 | 1,097 | 0.0237 | |
| 2 | 1,193 | 0.0378 | |
| 3 | 1,385 | 0.0669 | |
| 4 | 1,769 | 0.1295 | |
| 5 | 2,537 | 0.2184 | |
| 6 | 4,073 | 0.3602 |
"The maximum probability that either station's backoff counter reaches k." To verify this property we add an extra variable to the model which counts the number of collisions, and then find the maximum probability of this variable reaching k. In PRISM this is expressed by:
Model checking times:
| bcmax: | k=2 | k=4 | k=6 | k=8 | |||||
| iters: | time per iter (s): | iters: | time per iter (s): | iters: | time per iter (s): | iters: | time per iter (s): |
||
| 0 | 28 | 0.0353 | 170 | 0.2348 | 308 | 0.5483 | 436 | 0.0353 | |
| 1 | 28 | 0.0378 | 218 | 0.3188 | 447 | 0.7781 | 658 | 0.0378 | |
| 2 | 28 | 0.0425 | 218 | 0.3770 | 636 | 1.2197 | 1,019 | 0.0425 | |
| 3 | 28 | 0.0489 | 218 | 0.4340 | 825 | 2.1654 | 1,596 | 0.0489 | |
| 4 | 28 | 0.0528 | 218 | 0.4748 | 825 | 2.0959 | 2,313 | 0.0528 | |
| 5 | 28 | 0.0571 | 218 | 0.5146 | 825 | 2.2331 | 3,022 | 0.0571 | |
| 6 | 28 | 0.0585 | 218 | 0.5037 | 825 | 2.2494 | 3,022 | 0.0585 | |
Model checking results:
| bcmax: | k=2 | k=3 | k=4 | k=5 | k=6 | k=7 | k=8 | |
| 0 | 0.183594 | 0.033707 | 0.006188 | 0.001136 | 0.000209 | 0.000038 | 7.03e-6 | |
| 1 | 0.183594 | 0.017033 | 0.001580 | 0.000147 | 0.000014 | 1.26e-6 | 1.17e-7 | |
| 2 | 0.183594 | 0.017033 | 0.000794 | 0.000037 | 1.73e-6 | 8.05e-8 | 3.75e-9 | |
| 3 | 0.183594 | 0.017033 | 0.000794 | 0.000019 | 4.34e-7 | 1.01e-8 | 2.37e-10 | |
| 4 | 0.183594 | 0.017033 | 0.000794 | 0.000019 | 2.17e-7 | 2.54e-9 | 2.98e-11 | |
| 5 | 0.183594 | 0.017033 | 0.000794 | 0.000019 | 2.17e-7 | 1.27e-9 | 7.45e-12 | |
| 6 | 0.183594 | 0.017033 | 0.000794 | 0.000019 | 2.17e-7 | 1.27e-9 | 3.72e-12 |
Time-bounded probabilistic reachability: for the deadline models the following properties are verified:
In PCTL these is expressed by:
Pmin=? [ true U s1=12 & s2=12 & t<=T ]
Pmin=? [ true U (s1=12 | s2=12) & t<=T ]
Pmin=? [ true U s1=12 & t<=T ]
Model checking times:
| TT_MAX=500 | ||||||||
| DEADLINE (μs): | Iterations: | Time per iter. (s): | ||||||
| P1 | P2 | P3 | P1 | P2 | P3 | |||
| 2,500 | 73 | 92 | 89 | 0.061 | 0.166 | 0.115 | ||
| 5,000 | 187 | 215 | 215 | 1.06 | 1.44 | 1.78 | ||
| 10,000 | 445 | 465 | 469 | 12.6 | 10.4 | 11.7 | ||
| TT_MAX=1,250 | ||||||||
| DEADLINE (μs): | Iterations: | Time per iter. (s): | ||||||
| P1 | P2 | P3 | P1 | P2 | P3 | |||
| 2,500 | 59 | 71 | 71 | 0.044 | 0.060 | 0.051 | ||
| 5,000 | 142 | 164 | 170 | 0.285 | 0.650 | 0.596 | ||
| 10,000 | 358 | 405 | 410 | 8.44 | 8.54 | 8.79 | ||
| TT_MAX=2,500 | ||||||||
| DEADLINE (μs): | Iterations: | Time per iter. (s): | ||||||
| P1 | P2 | P3 | P1 | P2 | P3 | |||
| 2,500 | 8 | 10 | 10 | 0.047 | 0.072 | 0.052 | ||
| 5,000 | 108 | 132 | 132 | 0.093 | 0.239 | 0.160 | ||
| 10,000 | 227 | 354 | 354 | 3.02 | 3.21 | 2.77 | ||
Model checking results: in the graph below, for a selection of different values for DEADLINE, we have plotted the model checking results for each value of TT_MAX.
TT_MAX=500
TT_MAX=1,250
TT_MAX=2,500
Expected reachability: based on the reward structures given in the PRISM source code we consider the following expected reachability properties.
Maximum expected number of collisions before both stations correctly send their packets (R{"collisions"}max=? [ F s1=12 & s2=12 ])
Model checking times and results:
| bcmax: | Iterations: | Time per iter. (s): | Max expected collisions: | ||
| 0 | 340 | 0.0035 | 1.2248 | ||
| 1 | 422 | 0.0087 | 1.2023 | ||
| 2 | 616 | 0.0281 | 1.2014 | ||
| 3 | 1000 | 0.0807 | 1.2014 | ||
| 4 | 1565 | 0.2005 | 1.2014 | ||
| 5 | 3101 | 0.5403 | 1.2014 | ||
| 6 | 6169 | 1.8212 | 1.2014 |
Maximum expected time until both stations correctly deliver their packets (R{"time"}max=? [ F s1=12 & s2=12 ])
Model checking times:
| bcmax: | TT_MAX=2,500 | TT_MAX=15,000 | ||||
| Iterations: | Time per iter. (s): | Iterations: | Time per iter. (s): | |||
| 0 | 996 | 0.0009 | 3,743 | 0.0032 | ||
| 1 | 1,017 | 0.0026 | 3,130 | 0.0085 | ||
| 2 | 1,264 | 0.0097 | 3,019 | 0.0270 | ||
| 3 | 1,853 | 0.0420 | 3,398 | 0.0709 | ||
| 4 | 3,089 | 0.1312 | 4,390 | 0.1818 | ||
| 5 | 5,442 | 0.4398 | 6,813 | 0.4985 | ||
| 6 | 9,385 | 1.5949 | 10,848 | 1.6467 | ||
Model checking results:
| TT_MAX | bcmax | |||||||
| 0 | 1 | 2 | 3 | 4 | 5 | 6 | ||
| 500 | 3,792 | 3,865 | 3,882 | 3,883 | 3,883 | 3,883 | 3,883 | |
| 1,250 | 6,206 | 6,263 | 6,280 | 6,281 | 6,281 | 6,281 | 6,281 | |
| 2,500 | 10,230 | 10,261 | 10,276 | 10,277 | 10,277 | 10,277 | 10,277 | |
| 5,000 | 18,278 | 18,255 | 18,268 | 18,270 | 18,270 | 18,270 | 18,270 | |
| 10,000 | 34,401 | 34,265 | 34,274 | 34,275 | 34,275 | 34,275 | 34,275 | |
| 15,000 | 50,521 | 50,271 | 50,275 | 50,279 | 50,281 | 50,281 | 50,281 | |
| 15,800 | 52,944 | 52,677 | 52,681 | 52,682 | 52,682 | 52,682 | 52,682 | |
Maximum expected cost until both stations correctly deliver their packets (R{"cost"}max=? [ F s1=12 & s2=12 ])
Model checking times:
| bcmax: | TT_MAX=2,500 | TT_MAX=15,000 | ||||
| Iterations: | Time per iter. (s): | Iterations: | Time per iter. (s): | |||
| 0 | 1,251 | 0.0009 | 4,511 | 0.0038 | ||
| 1 | 1,210 | 0.0025 | 3,669 | 0.0086 | ||
| 2 | 1,469 | 0.0121 | 3,418 | 0.0260 | ||
| 3 | 2,120 | 0.0347 | 3,769 | 0.0683 | ||
| 4 | 3,330 | 0.1221 | 4,952 | 0.1804 | ||
| 5 | 5,974 | 0.3810 | 7,280 | 0.4989 | ||
| 6 | 10,406 | 1.4110 | 12,429 | 1.6510 | ||
Model checking results:
| TT_MAX | bcmax | |||||||
| 0 | 1 | 2 | 3 | 4 | 5 | 6 | ||
| 500 | 250,633 | 228,206 | 227,315 | 227,297 | 227,297 | 227,297 | 227,297 | |
| 1,250 | 617,953 | 561,758 | 559,505 | 559,457 | 559,456 | 559,456 | 559,456 | |
| 2,500 | 1,230,154 | 1,117,678 | 1,113,153 | 1,113,056 | 1,113,055 | 1,113,055 | 1,113,055 | |
| 5,000 | 2,454,555 | 2,229,519 | 2,220,450 | 2,220,254 | 2,220,252 | 2,220,252 | 2,220,252 | |
| 10,000 | 4,903,359 | 4,453,200 | 4,435,045 | 4,434,650 | 4,434,646 | 4,434,646 | 4,434,646 | |
| 15,000 | 7,352,163 | 6,676,882 | 6,649,639 | 6,649,046 | 6,649,040 | 6,649,040 | 6,649,040 | |
| 15,800 | 7,719,484 | 7,010,435 | 6,981,829 | 6,981,206 | 6,981,199 | 6,981,199 | 6,981,199 | |
Maximum expected time until either station correctly delivers its packet (R{"time"}max=? [ F s1=12 | s2=12 ])
Model checking times:
| bcmax: | TT_MAX=2,500 | TT_MAX=15,000 | ||||
| Iterations: | Time per iter. (s): | Iterations: | Time per iter. (s): | |||
| 0 | 918 | 0.0009 | 3,414 | 0.0033 | ||
| 1 | 927 | 0.0024 | 2,792 | 0.0108 | ||
| 2 | 1,159 | 0.0125 | 2,660 | 0.0340 | ||
| 3 | 1,712 | 0.0372 | 3,003 | 0.0716 | ||
| 4 | 2,893 | 0.2152 | 3,972 | 0.1988 | ||
| 5 | 5,032 | 0.3803 | 6,189 | 0.7594 | ||
| 6 | 9,130 | 1.4180 | 9,984 | 1.6505 | ||
Model checking results:
| TT_MAX | bcmax | |||||||
| 0 | 1 | 2 | 3 | 4 | 5 | 6 | ||
| 500 | 2,525 | 2,551 | 2,558 | 2,559 | 2,559 | 2,559 | 2,559 | |
| 1,250 | 4,190 | 4,199 | 4,206 | 4,207 | 4,207 | 4,207 | 4,207 | |
| 2,500 | 6,963 | 6,946 | 6,952 | 6,953 | 6,953 | 6,953 | 6,953 | |
| 5,000 | 12,512 | 12,441 | 12,445 | 12,446 | 12,446 | 12,446 | 12,446 | |
| 10,000 | 23,636 | 23,451 | 23,450 | 23,451 | 23,451 | 23,451 | 23,451 | |
| 15,000 | 34,761 | 34,462 | 34,457 | 34,457 | 34,457 | 34,457 | 34,457 | |
| 15,800 | 36,429 | 36,113 | 36,107 | 36,108 | 36,108 | 36,108 | 36,108 | |
Maximum expected cost until either station correctly delivers its packets (R{"cost"}max=? [ F s1=12 | s2=12 ])
Model checking times:
| bcmax: | TT_MAX=2,500 | TT_MAX=15,000 | ||||
| Iterations: | Time per iter. (s): | Iterations: | Time per iter. (s): | |||
| 0 | 1,247 | 0.0010 | 4,506 | 0.0034 | ||
| 1 | 1,200 | 0.0024 | 3,603 | 0.0084 | ||
| 2 | 1,452 | 0.0084 | 3,285 | 0.0256 | ||
| 3 | 2,096 | 0.0346 | 3,642 | 0.0682 | ||
| 4 | 3,276 | 0.1212 | 4,763 | 0.1800 | ||
| 5 | 5,856 | 0.3804 | 7,074 | 0.4995 | ||
| 6 | 9,651 | 1.4109 | 11,867 | 1.6513 | ||
Model checking results:
| TT_MAX | bcmax | |||||||
| 0 | 1 | 2 | 3 | 4 | 5 | 6 | ||
| 500 | 243,068 | 220,593 | 219,692 | 219,673 | 219,673 | 219,673 | 219,673 | |
| 1,250 | 602,888 | 546,644 | 544,381 | 544,333 | 544,332 | 544,332 | 544,332 | |
| 2,500 | 1,202,589 | 1,090,065 | 1,085,530 | 1,085,432 | 1,085,431 | 1,085,431 | 1,100,858 | |
| 5,000 | 2,401,991 | 2,176,906 | 2,167,828 | 2,167,630 | 2,167,628 | 2,167,628 | 2,167,628 | |
| 10,000 | 4,800,795 | 4,350,587 | 4,332,422 | 4,332,026 | 4,332,022 | 4,332,022 | 4,332,022 | |
| 15,000 | 7,199,599 | 6,524,268 | 6,497,017 | 6,496,422 | 6,496,416 | 6,496,416 | 6,496,416 | |
| 15,800 | 7,559,420 | 6,850,321 | 6,821,706 | 6,821,082 | 6,821,075 | 6,821,075 | 6,821,075 | |
Maximum expected time until station 1 correctly delivers its packet (R{"time"}max=? [ F s1=12 ])
Model checking times:
| bcmax: | TT_MAX=2,500 | TT_MAX=15,000 | ||||
| Iterations: | Time per iter. (s): | Iterations: | Time per iter. (s): | |||
| 0 | 824 | 0.0009 | 3,074 | 0.0061 | ||
| 1 | 924 | 0.0031 | 2,919 | 0.0098 | ||
| 2 | 1,201 | 0.0097 | 2,904 | 0.0296 | ||
| 3 | 1,774 | 0.0365 | 3,288 | 0.0740 | ||
| 4 | 3,012 | 0.1270 | 4,301 | 0.1932 | ||
| 5 | 5,247 | 0.7049 | 6,616 | 0.6965 | ||
| 6 | 9,274 | 1.4121 | 10,360 | 1.6465 | ||
Model checking results:
| TT_MAX | bcmax | |||||||
| 0 | 1 | 2 | 3 | 4 | 5 | 6 | ||
| 500 | 3,322 | 3,352 | 3,359 | 3,360 | 3,360 | 3,360 | 3,360 | |
| 1,250 | 5,572 | 5,581 | 5,586 | 5,587 | 5,587 | 5,587 | 5,587 | |
| 2,500 | 9,333 | 9,310 | 9,314 | 9,314 | 9,314 | 9,314 | 9,314 | |
| 5,000 | 16,855 | 16,768 | 16,769 | 16,769 | 16,770 | 16,770 | 16,770 | |
| 10,000 | 31,899 | 31,685 | 31,679 | 31,680 | 31,680 | 31,680 | 31,68 | |
| 15,000 | 46,943 | 46,601 | 46,589 | 46,590 | 46,590 | 46,590 | 46,590 | |
| 15,800 | 49,200 | 48,839 | 48,826 | 48,826 | 48,826 | 48,826 | 48,826 | |
Maximum expected cost until station 1 correctly delivers its packets (R{"cost"}max=? [ F s1=12 ])
Model checking times:
| bcmax: | TT_MAX=2,500 | TT_MAX=15,000 | ||||
| Iterations: | Time per iter. (s): | Iterations: | Time per iter. (s): | |||
| 0 | 1,250 | 0.0009 | 4,509 | 0.0034 | ||
| 1 | 1,206 | 0.0025 | 3,646 | 0.0083 | ||
| 2 | 1,462 | 0.0084 | 3,373 | 0.0262 | ||
| 3 | 2,109 | 0.0347 | 3,712 | 0.0681 | ||
| 4 | 3,300 | 0.1212 | 4,877 | 0.1801 | ||
| 5 | 5,923 | 0.3800 | 7,208 | 0.4975 | ||
| 6 | 10,095 | 1.4089 | 12,216 | 1.6523 | ||
Model checking results:
| TT_MAX | bcmax | |||||||
| 0 | 1 | 2 | 3 | 4 | 5 | 6 | ||
| 500 | 247,345 | 224,851 | 223,953 | 223,934 | 223,934 | 223,934 | 223,934 | |
| 1,250 | 611,400 | 555,091 | 552,829 | 552,781 | 552,780 | 552,780 | 552,780 | |
| 2,500 | 1,218,159 | 1,105,494 | 1,100,957 | 1,100,859 | 1,100,858 | 1,100,858 | 1,085,431 | |
| 5,000 | 2,431,675 | 2,206,299 | 2,197,211 | 2,197,014 | 2,197,012 | 2,197,012 | 2,197,012 | |
| 10,000 | 4,858,709 | 4,407,909 | 4,389,721 | 4,389,324 | 4,389,320 | 4,389,320 | 4,389,320 | |
| 15,000 | 7,285,742 | 6,609,518 | 6,582,229 | 6,581,635 | 6,581,628 | 6,581,628 | 6,581,628 | |
| 15,800 | 7,649,797 | 6,939,760 | 6,911,106 | 6,910,482 | 6,910,475 | 6,910,475 | 6,910,475 | |