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