complexity of algorithm

[steph...@gmail.com]

Hello everybody,

I would like to know the complexity of the algorithm used in MDP for the property specification Rmin=? [F target]. I cannot seem to find the right answer in the manual. Is it polynomial or exponential?!

Thanks,

Stephane.

[someusernam...@gmail.com]

Hello,
whether it is polynomial or exponential depends on how you measure it. Although I am not 100% sure (especially for symbolic models, since there it is not obvious to me how to measure the size), I think the algorithm uses in the worst case exponential time regarding the size of the LTL-formula in the squared-brackets and polynomial time regarding the size of the model, so the overall runtime is sometihng like O(poly(size of model) * exp(size of LTL-formula)).

[steph...@gmail.com]

In the MDP structure, there are no continuous time variables, that's why I was asking......

[Dave Parker]

Hi Stephane,

For the problem of checking Rmin=? [F target], the main part of the
computation can actually be done using linear programming, which makes
it polynomial (in the size of the state space). In practice, though,
PRISM usually uses iterative numerical methods, which do not have ths
complexity.

Hope that helps.

Dave

On 21/07/2016 08:02, steph...@gmail.com wrote:
> In the MDP structure, there are no continuous time variables, that's why
> I was asking......
>

> --
> 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 https://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.

[steph...@gmail.com]

Thank you very much for the answer. It indeed helps.