{"id":1796,"date":"2015-03-13T14:50:02","date_gmt":"2015-03-13T13:50:02","guid":{"rendered":"https:\/\/project.inria.fr\/plasma-lab\/?page_id=1796"},"modified":"2015-03-19T10:41:50","modified_gmt":"2015-03-19T09:41:50","slug":"reward-estimation","status":"publish","type":"page","link":"https:\/\/project.inria.fr\/plasma-lab\/reward-estimation\/","title":{"rendered":"Reward estimation for MDPs"},"content":{"rendered":"

<\/p>\n

In addition to estimating minimum and maximum probabilities<\/a>, PLASMA Lab implements an algorithm to estimate minimum and maximum expected reward, as defined by the rewards properties described below. The algorithms are demonstrated on a number of standard case studies<\/a>.<\/p>\n

\n

Types of reward<\/h3>\n

Rewards or costs are additional variables assigned to states or transitions. The RML language uses a specific rewards<\/strong> construction described below and on the PRISM website<\/a>:<\/p>\n

Important!<\/strong><\/p>
\nrewards “rewardName<\/em>“<\/p>\n

guard1<\/em> : value1;<\/em>
\n[] guard2<\/em>: value2<\/em>;
\n[channel<\/em>] guard3<\/em> : value3<\/em>;<\/p>\n

endrewards
\n<\/div><\/p>\n

This construction associates the following values to the reward:<\/p>\n

    \n
  1. The first command defines a state reward<\/strong> that assigns the value1<\/em> to each state of the model that satisfies guard1.<\/em><\/li>\n
  2. The second command defines a transition reward<\/strong> that assigns the value2<\/em> to each non synchronized transition that satisfies guard2.<\/em><\/li>\n
  3. The third command also defines a transition reward<\/strong> but it assigns the value3<\/em> only to the transitions labeled with channel<\/em> and that satisfy guard3<\/em>.<\/li>\n<\/ol>\n

    Three types of reward properties<\/strong> define the value of the reward associated to a path that will be used by the algorithm:<\/p>\n