iMDP Error: Transition probability has lower bound of 0 in state ...

[mcl...@seas.upenn.edu]

Dear All,

I have been trying to analyze interval MDPs using the newest version of PRISM (4.8.1). When I try to verify my model, PRISM returns an error saying "Error: Transition probability has lower bound of 0 in state ..."

I've attached a simple hello world example that throws the error. In this example, you can change the value of p_min on line 3 to any value below 0.5 to get PRISM to verify the model without issue.

Any ideas why this is the case?

Thanks,

Matthew

[Dave Parker]

Hi Matthew,

Interval models need to have a consistent transition graph structure,
across all the transition probabilities within the intervals, which
means you can only have intervals with a lower bound strictly greater
than zero. This is because the behaviour of a model can be qualitatively
different if transitions are added/removed. So, in your attached model,
p_min can be anything in the range (0,0.5], but not 0.

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
> <mailto:prismmodelchec...@googlegroups.com>.
> To view this discussion on the web, visit
> https://groups.google.com/d/msgid/prismmodelchecker/a7d237a2-caec-48f9-bb23-39dfa8311bfcn%40googlegroups.com <https://groups.google.com/d/msgid/prismmodelchecker/a7d237a2-caec-48f9-bb23-39dfa8311bfcn%40googlegroups.com?utm_medium=email&utm_source=footer>.