www.prismmodelchecker.org

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

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

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

Benchmarks