Problem using parametric PRISM on MDPs

[Shalini Ghosh]

I have a simple mdp model in PRISM for modeling lane changes in a car controller (model file lanechange_mdp_simple.prism attached). The property we're trying to evaluate is the ratio of the min. reward for changing lanes to abandoning the lane change (properties file lanechange_mdp.props attached).

When I set the value of the variable p to 0.626 and run: 'prism lanechange_mdp_simple.prism lanechange_mdp.props', the PRISM output is:

--> Result: 2.004274843687604 (value in the initial state)

When I set p to 0.1 and run the same command, the PRISM output is:

--> Result: 1.0666666 (value in the initial state)

We see that the property changes with p, as expected -- hence, if we parameterize the model and use parametric model checking in PRISM, we would expect the output to be a polynomial in p.

So, we considered a parametric form of the mdp (model file lanechange_mdp_simple_parametric.prism attached) and ran parametric model checking using the command: 'prism lanechange_mdp_simple.prism lanechange_mdp.props --param p=0:0.9'. However, instead of getting a polynomial in p in the output, the output is degenerate:

--> Result: ([0.0,0.9]): { 1  }

I also tried a couple of variants of this mdp, but the same problem happened -- any idea why this could be happening?

Thanks,
Shalini.

[Joachim Klein]

Hi Shalini,

> I have a simple mdp model in PRISM for modeling lane changes in a car
> controller (model file lanechange_mdp_simple.prism attached). The
> property we're trying to evaluate is the ratio of the min. reward for
> changing lanes to abandoning the lane change (properties file
> lanechange_mdp.props attached).

Thanks for the report, indeed the results look strange. The
Rmin=?[ F "abandoned" ] (1/2) looks fine, but the results for
Rmin=?[ F "changed" ] (also 1/2) is wrong.

I've opened a bug report in the PRISM issue tracker at
https://github.com/prismmodelchecker/prism/issues/15

It looks like there is some problem with the precomputation of the
zero/infinity states in the parametric/exact engine for Rmin in this
model. This will require a bit of debugging.


Cheers,
Joachim

[Shalini Ghosh]

[Shalini Ghosh]

Hi Joachim,

Thanks for your prompt response!

Good to know that you've filed a bug report in the PRISM issue tracker -- it would be very helpful if you can let me know once you've debugged the problem.

Best,
Shalini.