Interpreting total reward property

9 views
Skip to first unread message

Mridu Nanda

unread,
Apr 3, 2022, 11:53:52 PMApr 3
to PRISM model checker
Hi,

I understand that R=? [C] means the expected reward if every path is run to infinity. In an mdp, what does the property Rmax=? [C] mean? In other words, how does the "max" qualifier relate to the expected reward?

Thanks,
Mridu 

Gethin Norman

unread,
Apr 5, 2022, 10:22:19 AMApr 5
to prismmod...@googlegroups.com, Gethin Norman
Mridu,

similar to my reply to your other message, for Rmax=?[C] it would return the maximum expected total cumulative reward when considering all possible resolutions of the non-determinism (for any resolution of the non-determism we get a DTMC and then can compute the expected total cumulative reward for that DTMC).

thanks

Gethin
> --
> 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.
> To view this discussion on the web, visit https://groups.google.com/d/msgid/prismmodelchecker/572b9d08-909b-4e23-a43d-ae17edafeb53n%40googlegroups.com.

Reply all
Reply to author
Forward
0 new messages