Computing the minimum or maximum probability of reaching some set of states in a PTA within a time-bound, i.e. PRISM properties of the form:

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

Model | Property | PRISM property & description |
Extra parameters |
Min/max | Notes |

csma_abst |
deadline_max |
Pmax=? [ F<=T "done" ] Maximum probability that both stations have sent their packets within time T |
T (time bound: e.g. 1000,1750,1800,...) |
max | |

csma_abst |
deadline_min |
Pmin=? [ F<=T "done" ] Minimum probability that both stations have sent their packets within time T |
T (time bound: e.g. 1000,1750,1800,...) |
min | |

firewire |
deadline |
Pmin=? [ F<=T "done" ] Minimum probability that a leader has been elected by time T |
T (time bound: e.g. 2500,5000,...) |
min | |

firewire_abst |
deadline_max |
Pmax=? [ F<=T "done" ] Maximum probability that a leader has been elected by time T |
T (time bound: e.g. 50,500,5000,...) |
max | |

firewire_abst |
deadline_min |
Pmin=? [ F<=T "done" ] Minimum probability that a leader has been elected by time T |
T (time bound: e.g. 5000,10000,15000,...) |
min | |

repudiation_honest |
deadline |
Pmin=? [ F<T "terminated_successfully" ] Minimum probability that the protocol terminates successfully before time T |
T (time bound: e.g. 40,80,100,...) |
min | |

repudiation_malicious |
deadline |
Pmax=? [ F<T "gains_information" ] Maximum probability that the malicious recipient gains information before time T |
T (time bound: e.g. 5,10,20,...) |
max | |

zeroconf |
deadline |
Pmax=? [ F<=T s=2 & ip=2 ] Maximum probability of configuring IP address incorrectly by time T |
T (time bound: e.g. 100,150,200,...) |
max |

Computing the minimum or maximum probability of reaching some set of states in a PTA, 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).

Note that time-bounded reachability queries (see below) are reduced to reachability queries for PTAs so this as an additional source of benchmarks for this property class.

Model | Property | PRISM property & description |
Extra parameters |
Min/max | Notes |

csma |
collisions |
Pmax=? [ F "cmax" ] Maximum probability that transmissions from stations collide COL times |
- | max | |

repudiation_malicious |
eventually |
Pmax=? [ F "gains_information" ] Maximum probability that the malicious recipient eventually gains information |
- | max | |

zeroconf |
incorrect |
Pmax=? [ F s=2 & ip=2 ] Maximum probability of configuring IP address incorrectly |
- | max |

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

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

where the probability is 0/1 for all states.

Model | Property | PRISM property & description |
Extra parameters |
Min/max | Notes |

csma_abst |
eventually |
Pmin=? [ F "done" ] Minimum probability that both stations eventually send their packets |
- | min | |

firewire |
eventually |
Pmin=? [ F "done" ] Minimum probability that a leader is eventually elected |
- | min | |

firewire_abst |
eventually |
Pmin=? [ F "done" ] Minimum probability that a leader is eventually elected |
- | min | |

repudiation_honest |
eventually |
Pmin=? [ F "terminated_successfully" ] Minimum probability that the protocol eventually terminates successfully |
- | min |