Expess property in PRISM(PCTL)

[Anuroop Kuppam]

Hello,

I have a PRISM model and I want to check for its properties. Specifically the property { phi = true U state=3 }

where U is the strongest until operation.

The definition of U :

The expression s[i] |= (p U q) holds when:

  1. s[i] |= (p U q) where U is weak until operation

  2. there exists some j>=i for which s[ j ] |=q.

Thanks,

Anuroop Kuppam

[Gethin Norman]

Anuroop,

the operator “U” in PRISM is the strong until operator, so you can just use this.

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 http://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.

[Anuroop Kuppam]

Thanks Gethin.