Deterministic time delays to a CTMC

[Khaza Anuarul Hoque]

The following code is from the PRISM site:
http://www.prismmodelchecker.org/manual/FrequentlyAskedQuestions/PRISMModelling


===

ctmc

const int k;
const double mean = 10;

module trigger

i : [1..k+1];

[]   i < k -> k/mean : (i'=i+1);
[go] i = k -> k/mean : (i'=i+1);

endmodule

module main

x : [0..1];

[go] x=0 -> (x'=1);


===

I am confused coz when I check the mentioned property:   P=? [ F<=T x=1 ], i get a different graph as i was expecting a probability of very close to 1 at point T = 10 for k = 1000.

Can someone please explain me the reason ? Thanks a lot in advance.

[Dave Parker]

Hi Khaza,

You are only varying T in steps of 5 for your experiment. Use a smaller
step value, and you will see a sharper jump in the curve (and thus a the
increase to probability 1 will be much closer to T=10).

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

[Khaza Anuarul Hoque]

Hi Dave,

According to PRISM site, I am expecting that for k=1000,T=10 the probability will be something like 0.9995 or very close to 1. But When i do the experiment , the result I get is 0.504. I am wondering why is that ?

[Dave Parker]

Why do you expect this? The graph on the website shows that the
probability is very close to 0 for T just less than 10 and very close to
1 for T just higher than 10. The curve jumps up from 0 to 1 at
approximately T=10 and the probability is thus in the middle of the
range (approx, 0.5) at T=10.

Best wishes,

Dave.

On 22/11/2013 00:05, Khaza Anuarul Hoque wrote:
> Hi Dave,
>
> According to PRISM site, I am expecting that for k=1000,T=10 the
> probability will be something like 0.9995 or very close to 1. But When i
> do the experiment , the result I get is 0.504. I am wondering why is that ?
>
>
>
> On Thursday, November 21, 2013 7:00:32 PM UTC-5, Dave Parker wrote:
>
> Hi Khaza,
>
> You are only varying T in steps of 5 for your experiment. Use a smaller
> step value, and you will see a sharper jump in the curve (and thus a
> the
> increase to probability 1 will be much closer to T=10).
>
> Best wishes,
>
> Dave.
>
> On 21/11/2013 23:48, Khaza Anuarul Hoque wrote:
> > The following code is from the PRISM site:
> >
> http://www.prismmodelchecker.org/manual/FrequentlyAskedQuestions/PRISMModelling

> <http://www.google.com/url?q=http%3A%2F%2Fwww.prismmodelchecker.org%2Fmanual%2FFrequentlyAskedQuestions%2FPRISMModelling&sa=D&sntz=1&usg=AFQjCNFOt5NTjumxC_I-jwjTAl-x_P_Ekw>

>
> >
> >
> > ===
> >
> > ctmc
> >
> > const int k;
> > const double mean = 10;
> >
> > module trigger
> >
> > i : [1..k+1];
> >
> > [] i < k -> k/mean : (i'=i+1);
> > [go] i = k -> k/mean : (i'=i+1);
> >
> > endmodule
> >
> > module main
> >
> > x : [0..1];
> >
> > [go] x=0 -> (x'=1);
> >
> >
> > ===
> >
> > I am confused coz when I check the mentioned property: |P=? [
> F<=T x=1
> > ], i get a different graph as i was expecting a probability of very
> > close to 1 at point T = 10 for k = 1000.
> >
> > Can someone please explain me the reason ? Thanks a lot in
> advance. |
> >
> > --
> > 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 <javascript:>.

> > To post to this group, send an email to

> prismmod...@googlegroups.com <javascript:>.

> > Visit this group at
> http://groups.google.com/group/prismmodelchecker

> <http://groups.google.com/group/prismmodelchecker>.

> > For more options, visit https://groups.google.com/groups/opt_out

> <https://groups.google.com/groups/opt_out>.

[Khaza Anuarul Hoque]

Hi Dave,

thanks for the answer, Got it now. i was wondering is it possible to model exact time delays with such erlang distribution. Lets say we have 2 states A and B. Also lets say we have a global clock, and exactly in every 1 hour transition from A to B (or B to A if already in B after first transition) takes place, is it possible to express such scenario ?

Regards

[Dave Parker]

Hi Khaza,

I'm not sure what you are asking. If you want to adapt the example model
so that it oscillates between two states A and B after a deterministic
delay (say, every 1 hour), this is easy to do.

But the whole point of that example is that it *approximates* a
deterministic delay for a CTMC model. It is not possible to have an
event occurring after *exactly* 1 hour, if you need to model the rest of
your system as a CTMC.

Best wishes,

Dave.

> <http://www.google.com/url?q=http%3A%2F%2Fwww.prismmodelchecker.org%2Fmanual%2FFrequentlyAskedQuestions%2FPRISMModelling&sa=D&sntz=1&usg=AFQjCNFOt5NTjumxC_I-jwjTAl-x_P_Ekw
> <http://www.google.com/url?q=http%3A%2F%2Fwww.prismmodelchecker.org%2Fmanual%2FFrequentlyAskedQuestions%2FPRISMModelling&amp;sa=D&amp;sntz=1&amp;usg=AFQjCNFOt5NTjumxC_I-jwjTAl-x_P_Ekw>>

[Khaza Anuarul Hoque]

Hi Dave,

Yes, u r right, the exact delay is not possible but for now the approximate delay would work I guess. Actually I am trying to model failure and repair. So failure transitions follow exponential delay but repair is periodic, so lets say every hour the system is checked and faulty module is replaced, that's why i am trying to model  the periodic transition. 

As you just mentioned its easy to adopt that example and make it oscillate between the states, can you give a short example code ? thanks a lot in advance.

[Dave Parker]

> As you just mentioned its easy to adopt that example and make it
> oscillate between the states, can you give a short example code ? thanks
> a lot in advance.

You just need to change an update in the "trigger" module, and add a new
command to the "main" module. Here is the updated model:

------

ctmc

const int k;
const double mean = 10;

module trigger

i : [1..k+1];

[] i < k -> k/mean : (i'=i+1);

[go] i = k -> k/mean : (i'=1);

endmodule

module main

x : [0..1];

[go] x=0 -> (x'=1);

[go] x=1 -> (x'=0);

endmodule
------

You can then check the property P=? [ F=T x=1 ] for a range of T to see
the oscillating behaviour.

Best wishes,

Dave.

[K. Anuarul Hoque]

thanks dave, just tried the code with the property P=? [ F=T x=1 ] for a range of T (k = 100 and mean = 10).  Probability of (x=1) becomes 1 at time step T = 14 and goes on, seems like it never comes back to x=0 and hence fails to oscillate periodically

[Dave Parker]

> thanks dave, just tried the code with the property P=? [ F=T x=1 ] for a
> range of T (k = 100 and mean = 10). Probability of (x=1) becomes 1 at
> time step T = 14 and goes on, seems like it never comes back to x=0 and
> hence fails to oscillate periodically

T=14 sounds about right, based on the attached graph showing the values
for various values of k.

If you do not see oscillation, perhaps you are using the property, e.g.
P=? [ F<=T x=1 ] instead of P=? [ F=T x=1 ].

Dave.

[K. Anuarul Hoque]

Hi Dave,

yes, I used P=? [ F<=T x=1 ],  because if i use P=? [ F=T x=1 ], it shows an syntax error !

[Dave Parker]

> yes, I used P=? [ F<=T x=1 ], because if i use P=? [ F=T x=1 ], it
> shows an syntax error !

I guess you are using an old version of PRISM. The F=T notation was
added in version 4.1. In older versions, you can use the equivalent F[T,T].

Dave.

[Khaza]

Hi Dave,

I tried to implement the oscillation between 2 states with deterministic delay and it works as we discussed. the graph is attached. However i need some help for more accurate modeling.


As you can see in the graph, its goes to x=1 at 11th time unit with a probability of 0.985. it waits for 10 more time unit and comes back to x=0 with a probability. again it waits for 10 more time unit and the probability of being at x=1 at 31th time unit is 0.90. So its decreased and keep deceasing with time. I was wondering if there is any way so that i can keep this probability same. that mean after every 10 time unit it will come back to x=0 with the same probability every time.

This is just an exercise that i am doing, so that i can implement the concept in the real problem, which is periodic repair of components in reliability problems.