# PRISM Benchmark Suite - Properties (PTAs)

### PTA time-bounded reachability

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

### PTA quantitative reachability

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

### PTA qualitative reachability

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