46 views

### Anastasia Mavridou

Jan 31, 2023, 8:01:55 PM1/31/23
to PRISM model checker
Hi,

We would like to express the following properties in PRISM:

1. Every time r holds, then q holds at the same time point with probability > 0.2.
2. Every time r holds, then what is the probability that q also holds at the same time point?

We have tried several formulas:

• For the first property: P>=1 [G (r => P>0.2 [q])], however this does not return the correct result. Does PRISM take into account the nested (P>0.2) probability?
• For the second property: P=?[G(r => q)] , however this computes the probability by adding both cases where 1)  r is true (and q); and 2) r is false and thus [r => q] is trivially true. However we only want to consider the non-trivially true case.
• For the second property, we also tried conditional probabilities:
• P=? [(q & r)] / P=? [r], however, this formula will only return the result at the first time point.
• We also tried adding the eventually operator: P=? [F (q & r)] / P=? [F r] but it appears that PRISM will not count anything past the first occurrence of r in our model.

Could you please help us with expressing these properties in PRISM? We can make our model and properties files available if needed.

Thank you,

Anastasia

### Dave Parker

Feb 1, 2023, 3:58:36 PM2/1/23
Hi Anastasia,

This is a bit tricky to formulate. PRISM's P operator expresses
properties about the probability of events that happen along the
possible paths (executions) from some state(s). For the property,
P>0.2[q], path formula q asks whether q is true in the current state, so
the probability P=?[q] is either 0 or 1 in a state, depending on whether
q is true in that state. So your property P>=1 [G (r => P>0.2 [q])]
is just the same as saying P>=1 [G (r => q)].

A conditional probability formulation seems more promising. Your
suggeston of P=? [F (q & r)] / P=? [F r] doesn't quite work (as you
suggest) because F refers to the first occurrence. One option is to look
at the conditional long-run probability: S=?[q & r] / S=?[r].

Best wishes,

Dave

On 01/02/2023 01:01, Anastasia Mavridou wrote:
> Hi,
>
> We would like to express the following properties in PRISM:
>
> 1. Every time r holds, then q holds at the same time point with
> probability > 0.2.
> 2. Every time r holds, then what is the probability that q also holds
> at the same time point?
>
>  We have tried several formulas:
>
> * For the first property: P>=1 [G (r => P>0.2 [q])], however this does
> not return the correct result. Does PRISM take into account the
> nested (P>0.2) probability?
> * For the second property: P=?[G(r => q)] , however this computes the
> probability by adding both cases where 1)  r is true (and q); and 2)
> r is false and thus [r => q] is trivially true. However we only want
> to consider the non-trivially true case.
> * For the second property, we also tried conditional probabilities:
> o P=? [(q & r)] / P=? [r], however, this formula will only return
> the result at the first time point.
> o We also tried adding the eventually operator: P=? [F (q & r)] /
> P=? [F r] but it appears that PRISM will not count anything past
> the first occurrence of r in our model.
>
> can make our model and properties files available if needed.
>
> Thank you,
>
> Anastasia
>
> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send
> To view this discussion on the web, visit

### Chris Kloukinas

Feb 3, 2023, 8:40:55 AM2/3/23

I wonder if rewards can be used to figure out what the probabilities of r, r&q, r&~q are, as in:

#Experiment 1
rewards
[] r : 1;
endrewards

#Experiment 2
rewards
[] r&q : 1;
endrewards

Then, compare the reward values from Exp 1 & 2.
(maybe I've misunderstood the question...)

Christos

### Anastasia Mavridou

Jul 25, 2023, 8:31:38 PM7/25/23
to PRISM model checker