46 views

Skip to first unread message

Jan 31, 2023, 8:01:55 PM1/31/23

to PRISM model checker

Hi,

We would like to express the following properties in PRISM:

- Every time r holds, then q holds at the same time point with probability > 0.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

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

to prismmod...@googlegroups.com, Anastasia Mavridou

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

> o P=? [(q & r)] / P=? [r], however, this formula will only return

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

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:

>

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

> We have tried several formulas:

>

> 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
> nested (P>0.2) probability?

> 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:
> r is false and thus [r => q] is trivially true. However we only want

> to consider the non-trivially true case.

> 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

>

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

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

to prismmod...@googlegroups.com

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

#Experiment 1rewards

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

Jul 25, 2023, 8:31:38 PM7/25/23

to PRISM model checker

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

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu