Computing the minimum or maximum probability of reaching some set of states in an MDP, i.e. PRISM properties of the form:
Quantitative properties only (i.e. the probability is not 0/1 for at least some states).
We also only include properties that do not require fairness.
| Model | Property | PRISM property & description |
Extra parameters |
Min/max | Notes |
| consensus | c2 |
Pmin=? [ F "finished"&"all_coins_equal_1" ] Minimum probability that the protocol finishes with all coins equal to v=1 |
- | min | |
| consensus | disagree |
Pmax=? [ F "finished"&!"agree" ] Maximum probability of finishing protocol with coins not all equal |
- | max | |
| csma | all_before_max |
Pmax=? [ !"collision_max_backoff" U "all_delivered" ] Maximum probability all stations send successfully before a collision with max backoff |
- | max | |
| csma | all_before_min |
Pmin=? [ !"collision_max_backoff" U "all_delivered" ] Minimum probability all stations send successfully before a collision with max backoff |
- | min | |
| csma | some_before |
Pmin=? [ F min_backoff_after_success<K ] Minimum probability that some station eventually delivers with less than K backoffs |
- | min | |
| firewire_dl | deadline |
Pmin=? [ F s=9 ] Minimum probability of completing protocol within deadline |
- | min | |
| firewire_impl_dl | deadline |
Pmin=? [ F ((s1=8) & (s2=7)) | ((s1=7) & (s2=8)) ] Minimum probability of completing protocol within deadline |
- | min | |
| wlan | collisions |
Pmax=? [ F col=COL ] Maximum probability of COL collisions |
- | max | |
| wlan_dl | deadline |
Pmin=? [ F s1=12 & s2=12 ] Maximum probability of COL collisions |
- | max | |
| zeroconf | correct_max |
Pmax=? [ F (l=4 & ip=1) ] Maximum probability of configuring correctly |
- | max | |
| zeroconf | correct_min |
Pmin=? [ F (l=4 & ip=1) ] Minimum probability of configuring correctly |
- | min | |
| zeroconf_dl | deadline_max |
Pmax=? [ !(l0=4 & ip0=2) U t>=deadline ] Maximum probability of not using fresh IP address within deadline |
- | max | |
| zeroconf_dl | deadline_min |
Pmin=? [ !(l0=4 & ip0=2) U t>=deadline ] Minimum probability of not using fresh IP address within deadline |
- | min |
Checking whether the minimum or maximum probability of reaching some set of states in an MDP is 0 or 1, e.g. PRISM properties of the form:
We also only include properties that do not require fairness.
| Model | Property | PRISM property & description |
Extra parameters |
Min/max | Notes |
| consensus | c1 |
P>=1 [ F "finished" ] With probability 1, all processes finish the protocol |
- | min | |
| wlan | sent |
P>=1 [ F s1=12 & s2=12 ] With probability 1, eventually both stations have sent their packet correctly |
- | min | |
| firewire_abst | elected |
P>=1 [ F "done" ] A leader is always eventually elected with probability 1 |
- | min | |
| firewire | elected |
P>=1 [ F "done" ] A leader is always eventually elected with probability 1 |
- | min |
Computing the minimum or maximum expected accumulated reward/cost to reach some set of states in an MDP, i.e. PRISM properties of the form:
| Model | Property | PRISM property & description |
Extra parameters |
Min/max | Notes |
| consensus | steps_max |
R{"steps"}min=? [ F "finished" ] Maximum expected steps to finish |
- | max | |
| consensus | steps_min |
R{"steps"}min=? [ F "finished" ] Minimum expected steps to finish |
- | min | |
| csma | time_max |
R{"time"}max=?[ F "all_delivered" ]
Maximum expected time for all messages to be sent |
- | max | |
| csma | time_min |
R{"time"}min=?[ F "all_delivered" ]
Minimum expected time for all messages to be sent |
- | min | |
| firewire | time_max |
R{"time"}max=? [ F "done" ] Maximum expected time to elect a leader |
- | max | |
| firewire | time_min |
R{"time"}min=? [ F "done" ] Minimum expected time to elect a leader |
- | min | |
| firewire | time_sending |
R{"time_sending"}max=? [ F "done" ] Maximum expected time spent sending before electing a leader |
- | max | |
| firewire_abst | rounds |
R{"rounds"}max=? [F "done" ] Maximum expected rounds to elect a leader |
- | max | |
| firewire_abst | time_max |
R{"time"}max=? [F "done" ] Maximum expected time to elect a leader |
- | max | |
| firewire_abst | time_min |
R{"time"}min=? [F "done" ] Minimum expected time to elect a leader |
- | min | |
| wlan | cost_max |
R{"cost"}max=? [ F s1=12 & s2=12 ] Maximum expected cost for both stations to send correctly |
- | max | |
| wlan | cost_min |
R{"cost"}min=? [ F s1=12 & s2=12 ] Minimum expected cost for both stations to send correctly |
- | min | |
| wlan | num_collisions |
R{"collisions"}max=? [ F s1=12 & s2=12 ] Maximum expected collisions before both stations to send correctly |
- | max | |
| wlan | time_max |
R{"time"}max=? [ F s1=12 & s2=12 ] Maximum expected time for both stations to send correctly |
- | max | |
| wlan | time_min |
R{"time"}min=? [ F s1=12 & s2=12 ] Minimum expected time for both stations to send correctly |
- | min |