Time for model checking

[maro...@gmail.com]

I am working on a CTMC model. When I try to perform model checking, PRISM does it really quickly for some properties (transient probabilities) but for the others(steady state probabilities )  it seems like taking forever. I left it for few hours and finally the property was verified but it just took hours. I just want to ask if it is a normal behavior? Or are there any alternate options to make the process fast? 

[Joachim Klein]

Hi Maroua,

> I am working on a CTMC model. When I try to perform model checking,
> PRISM does it really quickly for some properties (transient

> probabilities) but for the others(steady state probabilities) it

> seems like taking forever. I left it for few hours and finally the
> property was verified but it just took hours. I just want to ask if
> it is a normal behavior? Or are there any alternate options to make
> the process fast?

Generally, if you run into performance problems during computations, it
makes sense to play around trying the performance of the different
engines
(http://www.prismmodelchecker.org/manual/ConfiguringPRISM/ComputationEngines).
Likewise, it makes sense to try e.g. Gauss-Seidel or Jacobi as the
solution method for linear equation systems
(http://www.prismmodelchecker.org/manual/ConfiguringPRISM/SolutionMethodsAndOptions),
if those are available for the chosen engine.

One issue that can result in long computation times is a large number of
states (or large size of the symbolic representation when using one of
the (semi-)symbolic engines), the other might be slow convergence of the
iterative solution method.


Cheers,
Joachim Klein