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 |

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 |

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

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 |