Filters in PRISM

[diner]

Hi

I am wondering if someone can help me with a PRISM related query.

Let's say I have a CTMC model. Starting from the initial states, there exists different paths to reach an "error" state. Since the assumption is there exists multiple paths to reach the error state, what I want is to know the minimum, maximum and avg time required to reach the "error" state. Is there any way to do that in PRISM? 

My first impression was 'filters' will be able to help me with this while using with a reward structure in this format: filter(min,R{"total_time"}=? [F error], requirement: (let's say "ready") , but after reading some discussions in this forum I am more confused.

[Gethin Norman]

You can find the average or expected time if the state is reached with probability 1. This is achieved by using the reward operation R=?[F error ] where error is a predicate representing the error state and you assign a reward of 1 to all states.

If the error state can be reached then the minimum time to reach it is 0 and the maximum time is infinity. This is because each delay is exponential distribution and therefore can take any positive value. Paths for CTMCs include the time delay on each transition, and hence there will be an infinite number of paths that pass through the same sequence of states as opposed to the single path. For more details see:

http://www.prismmodelchecker.org/bibitem.php?key=KNP07a

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.

[K. Anuarul Hoque]

Thank you very much Gethin for your illustrative answer.  It is very clear from your answer that what i want is not possible in ctmc. However I am wondering if the model is given as a dtmc then is it possible to find the maximum/minimum time unit required to reach the error state via different paths , assuming that multiple path exists to reach an error state ?

Also can filters help in such cases to reason about paths ?

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/5Y34Wq2jxRs/unsubscribe.
To unsubscribe from this group and all its topics, send an email to prismmodelchec...@googlegroups.com.
To post to this group, send an email to prismmod...@googlegroups.com.

[Gethin Norman]

Filters will not help to reason about paths: filters are for analysing results for multiple states.

One way of finding the minimum and maximum number of steps for a DTMC (the maximum will only work if there are no loops, i.e. paths that return to a state they have already visited), is to consider the bounded operator P=?[F<=k error].

Just increase k from 0 and the first time the probability returned is greater than 0 gives the minimum number of steps. On the other hand, the first time the probability returned equals P=?[F error] will give the maximum number steps. You can do this by running an experiment and setting k to be an undefined constant, see:

http://www.prismmodelchecker.org/manual/RunningPRISM/Experiments

The approach for computing minimum will work even if there are loops, while if there are loops then the maximum can be infinity.

thanks

Gethin

[K. Anuarul Hoque]

Thanks for the explanation,  i will try this with my model.  As you said max will not work for models with loop, so does it also mean that there is no way to find the  avg time steps to reach the error state? If possible then how ?

Thanks again for your illustrative answers.

[Gethin Norman]

For the expected number of steps you can calculate this in the same manner that I explained for CTMCs (assuming the error state is reached with probability 1), however here the reward structure assigns 1 to all commands.

thanks

Gethin

[K. Anuarul Hoque]

Hi Gethin,

by "assigning the reward of one to all the commands" - do you mean the reward structure for the total time (as following)?  

rewards "total_time"

    true : 1;

endrewards

[Gethin Norman]

This will work, but as you are counting steps it would make sense to assign rewards to steps, e.g.

rewards
[] true : 1
[a] true : 1;
..
endrewards

if “a” is an action of the model and the dots correspond to adding a reward 1 to all other actions that appear in the model (if there are any).

thanks

Gethin

[K. Anuarul Hoque]

Thanks Gethin, really appreciate your time for answering the questions !