PRISM Model Optimal Policy Not Generated

16 views
Skip to first unread message

Wendy

unread,
Mar 6, 2025, 12:18:22 PMMar 6
to PRISM model checker

Hello,

I have successfully built a PRISM MDP model, and the property I want to check is Rmax=? [ C<=40 ], which calculates the maximum rewards at the end of the horizon/steps. I am able to obtain the expected rewards but cannot see the optimal policy. Could you guide me on the possible causes?

Since this is a clinical-related model and assuming that not all patients are dead at the end of the horizon, I added a filter to exclude patients who died by using:
filter(max, Rmax=? [ C<=40 ], death_cancer=0 & death_other_causes=0).

However, while I am still able to obtain the expected rewards, the policy is not generated.

Interestingly, I can see the policy for the following property, even though the rewards are infinite:
Rmax=? [ F (death_other_causes = 0 & death_cancer=0) ].

Could you please shed some light on what might be causing this issue and preventing me from seeing the policy? 


Thank you,

Wendy

Reply all
Reply to author
Forward
0 new messages