Specification of properties of the form P1 implies P2

[Muhammad Usama Sardar]

Hi everyone. 

I went through the property specification section in the manual. But I didn't come across the specification of properties of the form: 

P1 implies P=? [P2];

where P1 is some pre-condition 

I did find the relevant property mentioned in KNP08a: 

(kkpp=N ^ kpp=0) implies  P >0:12[ (kkpp>0) U (kpp>0) ]

But when I go to the relevant case study on PRISM website [MAPK Cascade Case study], I do not find any such property. Can someone please elaborate how it can be formalized in PRISM. 

Thank you. 

[Joachim Klein]

Hi,

> I went through the property specification section in the manual. But I
> didn't come across the specification of properties of the form:
>

> *P1 implies P=? [P2];*
> *where P1 is some pre-condition *
>
> I did find the relevant property mentioned in *KNP08a*:
> *(kkpp=N ^ kpp=0) implies P >0:12[ (kkpp>0) U (kpp>0) ]*

>
> But when I go to the relevant case study on PRISM website [MAPK Cascade
> Case study], I do not find any such property. Can someone please
> elaborate how it can be formalized in PRISM.

You can use something like this:

filter(forall, P>0.5[ something ], s<7)

which evaluates to TRUE if, for all states with s<7, the probability
from that state is larger than 0.5.

Equivalently, you can use the boolean implication operator:

filter(forall, s<7 => P>0.5[ something ], true)

Note that here the filter ranges over all states because of the 'true'
at the end.


Cheers,
Joachim Klein

[Muhammad Usama Sardar]

Thanks very much for the quick response. Is it possible somehow without using filters? (Because filters are not supported in Statistical Model Checking) 

[Gethin Norman]

If you are using statistical model checking then you are only checking the result for the initial state (the approach samples paths starting from the initial state). You can of course change the initial state to analyse the property for different states, but clearly this has limitations if you want to check a large number of states.

thanks

Gethin

> --
> 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.
> To post to this group, send email to prismmod...@googlegroups.com.
> Visit this group at https://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.

[Marcin Copik]

We have discussed supporting multiple initial states in my GSoC'14 project with Dave and Vojtech but it has not become a part of the project; it requires a little bit of work. If you need to obtain SMC results for multiple initial states, you could easily make the initial state dependent on constants and write a script running simulation on all constants values which are interesting for you.

I have been working on an OpenCL simulator engine in the past and now I'm quite close to do an official release. The simulator should support the same type of models, properties and language features as the original simulator engine, but it is significantly faster due to more efficient implementation, parallelization and a possibility to use a GPU for sampling. Would you be interested in trying it out for your models? I'd be grateful for the ability to extend my set of regression tests.

Best regards,

Marcin Copik

To post to this group, send an email to prismmod...@googlegroups.com.

[Muhammad Usama Sardar]

Thanks everyone for the responses. 

Dear Marcin,

Sure. Please share the details and I would try it out. 

Best Regards,

Muhammad Usama Sardar

http://save.seecs.nust.edu.pk/musama/

--
You received this message because you are subscribed to a topic in the Google Groups "PRISM model checker" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/prismmodelchecker/Z3o1Y8AygE8/unsubscribe.
To unsubscribe from this group and all its topics, send an email to prismmodelchec...@googlegroups.com.