Error: Constructing a strategy for Rmin in the presence of zero-reward ECs is currently not supported.

[kl...@vt.edu]

Can anyone tell me what this error means?

"Error: Constructing a strategy for Rmin in the presence of zero-reward ECs is currently not supported."

Not sure what an EC is and can't seem to find why the mdp model isn't able to complete.

[Joachim Klein]

Hi,

EC is short hand for end component; it might make sense not to use the
short hand for the error message.


So, from the error message it looks like you are using the explicit
engine with an MDP, trying to check an Rmin[ F goal ] property and to
extract the corresponding strategy, right?

For Rmin computations, zero-reward end components in the MDP pose some
challenges. A zero-reward end component is a set of states where a
scheduler/adversary could stay indefinitely without accumulating any
reward and without reaching the goal. Those are "attractive" for a
minimizing scheduler as it seems it would get zero reward. However,
these schedulers are improper, as the goal is not reached, so one needs
special treatment for those, or you could get results that are lower
than the real value.

We have recently added some mechanism to deal with zero-reward ECs via a
quotienting mechanism (collapsing the zero-reward ECs to single states),
but currently strategy generation (lifting the strategy from the
quotient model to the original model) is not yet available.


Cheers,
Joachim

[kl...@vt.edu]

Thank you for the help. This completely answers my question!