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

Skip to first unread message

Jan 17, 2024, 8:20:02 PMJan 17
to PRISM model checker
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?


Dave Parker

Jan 18, 2024, 3:50:18 AMJan 18
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,

> --
> 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
> <>.
> To view this discussion on the web, visit
> <>.
Reply all
Reply to author
0 new messages