Computing the minimum or maximum probability of reaching some set of states in an MDP, i.e. PRISM properties of the form:

- Pmin=? [ F ... ] or Pmax=? [ F ... ]
- Pmin=? [ ... U ... ] or Pmax=? [ ... U ... ]

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:

- P>=1 [ F ... ] or P>0 [ F ... ]

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:

- Rmin=? [ F ... ] or Rmax=? [ F ... ]

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