Question about properties

[Anastasia Mavridou]

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]

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

> --
> 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
> an email to prismmodelchec...@googlegroups.com
> <mailto:prismmodelchec...@googlegroups.com>.
> To view this discussion on the web, visit
> https://groups.google.com/d/msgid/prismmodelchecker/57afe6bb-4d8a-4b6d-8fae-5e785430f2cen%40googlegroups.com <https://groups.google.com/d/msgid/prismmodelchecker/57afe6bb-4d8a-4b6d-8fae-5e785430f2cen%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Chris Kloukinas]

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]

Thank you both for your answers! 

Indeed, in this property: P>=1 [G (r => P>0.2 [q])] the internal probability is meaningless. 

I tried using rewards and it seems to give me the result I would expect. I need to investigate more.

Thank you,

Anastasia