MDP support

[ochipara]

Hi,

I am interested in checking time-bounded reachability for an mdp model. An example is shown below:

mdp const double ps; module active s : [0 .. 3] init 0; [] s = 0 -> ps : (s'=1) + (1 - ps) : (s'=0); [] s = 0 -> ps : (s'=2) + (1 - ps) : (s'=0); [] s = 1 -> ps : (s'=3) + (1 - ps) : (s'=1); [] s = 2 -> ps : (s'=3) + (1 - ps) : (s'=1); endmodule

rewards "progress" s = 0: 0; s = 1: 1; s = 2: 1; s = 3: 2; endrewards

I want to check system properties of the form: P=? [true U<=5 (s = 3)]. Is there support in storm built for evaluating such properties?

[volkm]

Yes, step-bounded reachability properties are supported in Storm. As your model is an MDP you need to specify whether you want to compute the minimal or maximal probability: Pmin=? [F<=5 (s = 3)]. Other than that, the property should work. Please also note that the variable ps needs to be initialized either directly in the Prism file or from the command line with --constants "ps=0.4".

[ochipara]

Thank you for the quick reply. I really want to use ps as a parameter rather than a constant. So, in fact, I want to compute the minimal reachability of a state for PMDPs.

[cdehnert]

Thanks for your interest in Storm!

For a pMDP, there is not the minimal/maximal reachability probability, since the optimal resolution of nondeterminism (potentially) depends on the values of the parameters. For DTMCs, reachability probabilities also depend on the parameter values, but can be represented as a rational function in a "compact" closed form. However, this is not true anymore for MDPs: here, every possible resolution of nondeterminism corresponds to a rational function and the min/max over all these functions is not necessarily representable as a rational function. Could you be more specific what kind of result you would like to obtain in your scenario?

[ochipara]

Agreed. What I want to compute is solve the following problem: given every possible resolution of non-determinism, what is a lower bound on the likelihood of reaching a state after k steps. It would also be nice to have various types of adversaries, but that's a bonus.

[tquatmann]

I'm sorry, we are still not a 100% sure what result you expect exactly.

• Should the provided lower bound be a real number, representing the minimum (or maximum) over all possible parameter values? In this case, something like

  ~/storm/build/bin/storm-pars --prism model.prism --prop 'Pmin=? [F<=5 (s=3)]' --region '0.01<=ps<=0.99' --extremum min 0.05 

  should do the trick.

• If the provided lower bound should be a function over the parameter ps, Storm only supports this for DTMCs and not for MDPs (what @cdehnert said).

[ochipara]

Thank you both. The first option should be good enough. I have a couple of further questions:

• I assume that we could also check properties based on rewards such as Rmin=? [F<=4 (s=3)]. For this query, Storm reports the following error:

ERROR (SparseMdpParameterLiftingModelChecker.cpp:67): Simplifying the model was not successfull. ERROR (storm-pars.cpp:642): An exception caused Storm-pars to terminate. The message of the exception is: UnexpectedException: Simplifying the model was not successfull.

• What algorithm (or combination of algorightms) does Storm use to check bounded reachability properties?

[tquatmann]

Step-bounded expected rewards can be checked via cumulative reward properties, e.g.:

./storm-pars --prism test.pm --prop 'Rmin=? [C<=4]' --region '0.01<=ps<=0.99' --extremum min 0.05

This refers to the reward collected within 4 steps However, you can not specify any kind of goal states here.

Towards your second question: Storm uses Parameter lifting as described here and (more recently) here in Section VI and VII. While these paper discuss unbounded properties, the results can be lifted to step-bounded properties, as well.