CTMC: Filter (avg, max, min).

[Valdivino Santiago]

Hello all,

My model is a CTMC and I have the following .props file (a piece of it):

const double T;

// Label: 1 - 0

label "a_1" = (o = 1) & (g = 0);

label "b_1" = (o = 1) & (g = 1);

...

// Label: 12 - 11

label "a_12" = (o = 12) & (g = 11);

label "b_12" = (o = 12) & (g = 12);

...

And I have these properties:

filter(avg, P=? [ "a_1" U<=T "b_1"], o=1&g=0 )

filter(avg, P=? [ "a_12" U<=T "b_12"], o=12&g=11)

filter(max, P=? [ "a_1" U<=T "b_1"], o=1&g=0 )

filter(max, P=? [ "a_12" U<=T "b_12"], o=12&g=11)

filter(min, P=? [ "a_1" U<=T "b_1"], o=1&g=0 )

filter(min, P=? [ "a_12" U<=T "b_12"], o=12&g=11)

We see that I want to verify these properties from a state that it is not the initial one. My question is whether these properties (avg, max, min) "make" sense since my model is a CTMC and not a MDP or PTA. I ran and I got the values of probabilities when I selected several values of T (time) but I am just wondering if this approach is conceptually valid.

Thank you again for your help.

Best,

Valdivino.

[Dave Parker]

Hi Valdivino,

It's hard to day whether these "make sense" - it depends what property
of your model you are trying to analyse. However, for MDP/PTA models,
you will be checking a Pmin or Pmax property, so it probably makes more
sense to use a corresponding "min" or "max" filter, rather than an "avg"

Best wishes,

Dave.

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

[Valdivino Santiago]

  Hi Dave,

  After analyzing several logs of PRISM when Model Checking my system, I believe that these properties DO make sense, specially the "avg" filter for my CTMC model. The fact that I am starting the analysis not from the initial state, in my point of view, helps these filters to "make sense".

   Yes, I could realize about Pmin/Pmax for MDP/PTAs.

    Thank you again.

     Best,

     Valdivino. 

> <mailto:prismmodelchecker+unsub...@googlegroups.com>.