Computing the probability of reaching some set of states in a DTMC, i.e. PRISM properties of the form:
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 |
Checking whether the probability of reaching some set of states in an MDP is 0 or 1, e.g. PRISM properties of the form:
| Model | Property | PRISM property & description |
Extra parameters |
Notes |
| leader_sync | eventually_elected |
P>=1 [ F "elected" ] Probability that a leader is eventually elected |
Computing the expected accumulated reward/cost to reach some set of states in a DTMC, i.e. PRISM properties of the form:
| 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 |
||
| 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 |