Absolute vs relative convergence test

509 views
Skip to first unread message

Prasenjit Karmakar

unread,
May 12, 2011, 3:11:26 AM5/12/11
to PRISM model checker
I have a 3-state CTMC model with transition matrix as follows:

0 -> 1 : 2*lambda
1 -> 0 : mu
1 -> 2 : lambda

where lambda=1/MTTF and mu=1/MTTR. The input I have taken is
MTTF=200000 hr and MTTR=0.5 hr

Now when calculating the mean time to reach state 2 by expected reward
calculation I am getting the answer as 2.6E10(My termination epsilon
is 1E-06 and I am using SOR method with termination criteria
"relative").
But analytically solving the CTMC gives the result as 4E10.
Also changing the termination criteria as "absolute" gives me the
correct answer. So, when calulating expected reward should I go for
termination criteria as "absolute" always(especially for slowly
converging models) i.e absolute test is more strict?

Prasenjit

Gethin Norman

unread,
May 12, 2011, 3:28:52 AM5/12/11
to prismmod...@googlegroups.com, Gethin Norman

Prasenjit,

if you look at the definitions of absolute and relative difference, you see

- the absolute is based on the actual difference between values e.g. | x - y |
- the relative is based on the difference compared to their actual size, e.g. | x - y |/max(x,y)

So if the values are less than 1 (i.e. probabilities) then using relative difference convergence test is stricter (since in this case | x - y | is smaller than | x - y |/max(x,y)). However, the reverse is true when the values are greater than 1 (the absolute test is stricter). Therefore to obtain the most precise results you should use relative when the values are less than or equal to 1 and absolute otherwise.

In your case the reward values are very large indeed and as a result using the relative convergence criteria PRISM thinks that the iterative method has converged too early leading to imprecise results.

Gethin

> --
> You received this message because you are subscribed to the Google Groups "PRISM model checker" group.
> To post to this group, send email to prismmod...@googlegroups.com.
> To unsubscribe from this group, send email to prismmodelchec...@googlegroups.com.
> For more options, visit this group at http://groups.google.com/group/prismmodelchecker?hl=en.
>


The University of Glasgow, charity number SC004401

Reply all
Reply to author
Forward
0 new messages