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

10 views
Skip to first unread message

mcl...@seas.upenn.edu

unread,
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?

Thanks,
Matthew
prismHelloWorld.prism
prismHelloWorldProps.props

Dave Parker

unread,
Jan 18, 2024, 3:50:18 AMJan 18
to prismmod...@googlegroups.com, mcl...@seas.upenn.edu
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>.
Reply all
Reply to author
Forward
0 new messages