Enable arbitrary precision for Rmax=?

Mohammad Abdulaziz

unread,

Apr 14, 2022, 10:48:02 AM4/14/22

to PRISM model checker

Hello everyone,

Is it possible to enable arbitrary precision for Rmax properties?

best,

Mohammad

Dave Parker

unread,

Apr 14, 2022, 12:03:02 PM4/14/22

to prismmod...@googlegroups.com, Mohammad Abdulaziz

Hi Mohammad,

We support arbitrary precision for expected reward to reach a target on
MDPs. Here's an example:

prism ../prism-tests/functionality/verify/mdps/rewards/robot.nm -pf
'Rmin=? [ F "goal2" ]' -exact

Currently, that's done by reducing it to PRISM's parametric model
checking functionality, so it's done in a different part of the code.

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/dfcda9a2-b85f-444b-a6ed-7c3e565492b7n%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker/dfcda9a2-b85f-444b-a6ed-7c3e565492b7n%40googlegroups.com?utm_medium=email&utm_source=footer>.

Mohammad Abdulaziz

unread,

Apr 14, 2022, 2:06:43 PM4/14/22

to PRISM model checker

Hi Dave,

Many thanks for your response. I cannot get it to work when checking a cumulative reward property (e.g. Rmax=? [ C<= k]). Is there a way to get that to work?

best,

Mohammad

Dave Parker

unread,

Apr 26, 2022, 11:45:52 AM4/26/22

to prismmod...@googlegroups.com, Mohammad Abdulaziz

No, we only have the exact method implemented for R[F], in terms of
reward properties, I'm afraid.

Best wishes,

Dave

> <https://groups.google.com/d/msgid/prismmodelchecker/dfcda9a2-b85f-444b-a6ed-7c3e565492b7n%40googlegroups.com?utm_medium=email&utm_source=footer
> <https://groups.google.com/d/msgid/prismmodelchecker/dfcda9a2-b85f-444b-a6ed-7c3e565492b7n%40googlegroups.com?utm_medium=email&utm_source=footer>>.

>
>
> --
> 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/c78964d2-bdc0-4ca5-b7bc-973baeca4763n%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker/c78964d2-bdc0-4ca5-b7bc-973baeca4763n%40googlegroups.com?utm_medium=email&utm_source=footer>.

Reply all

Reply to author

Forward