www.prismmodelchecker.org

PRISM Benchmark Suite - Properties (MDPs)

MDP quantitative reachability

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

MDP qualitative reachability

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

MDP expected reachability

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

Benchmarks