www.prismmodelchecker.org

PRISM Benchmark Suite - Properties (DTMCs)

DTMC quantitative reachability

Computing the probability of reaching some set of states in a DTMC, i.e. PRISM properties of the form:

  • P=? [ F ... ]
  • P=? [ ... U ... ]

Quantitative properties only (i.e. the probability is not 0/1 for at least some states).

Model Property PRISM property
& description
Extra
parameters
Notes
brp p1 P=? [ F s=5 ]
Probability that the sender does not report a successful transmission (property 1 from [DJJL01])
brp p2 P=? [ F s=5 & srep=2 ]
Probability that the sender reports an uncertainty on the success of the transmission (property 2 from [DJJL01])
brp p4 P=? [ F !(srep=0) & !recv ]
Probability that the receiver does not receive any chunk when the sender did try to send a chunk (property 4 from [DJJL01])
crowds positive P=? [ F observe0>1 ]
Probability that the adversary observes the real sender more than once
egl unfairA P=? [ F !"knowA" & "knowB" ]
Probability that party A is unfairly disadvantaged
egl unfairB P=? [ F !"knowB" & "knowA" ]
Probability that party B is unfairly disadvantaged
nand reliable P=? [ F s=4 & z/N<0.1 ]
Probability that less than 10 percent of outputs are erroneous

DTMC qualitative reachability

Checking whether the 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 ... ]
Model Property PRISM property
& description
Extra
parameters
Notes
leader_sync eventually_elected P>=1 [ F "elected" ]
Probability that a leader is eventually elected

DTMC expected reachability

Computing the expected accumulated reward/cost to reach some set of states in a DTMC, i.e. PRISM properties of the form:

  • R=? [ F ... ]
Model Property PRISM property
& description
Extra
parameters
Notes
bluetooth time R=? [ F rec=mrec {"init"}{max} ]
Expected time to complete the inquiry phase
Note the use of a filter since there are muliple initial states.
egl messagesA R{"messages_A_needs"}=? [ F phase=4 ]
Expected number of messages A needs to knows a pair once B knows a pair
egl messagesB R{"messages_B_needs"}=? [ F phase=4 ]
Expected number of messages B needs to knows a pair once A knows a pair
herman steps R=? [ F "stable" {"init"}{max} ]
Expected number of steps until termination
Note the use of a filter since there are muliple initial states.
leader_sync time R{"num_rounds"}=? [ F "elected" ]
Expected time (number of rounds) to elect a leader

Benchmarks