Parametric model checking for reward parameters

[xinwei2124]

Hi, there

It seems that the stormy 1.6.4 doesn't support the analysis of the DTMC models, whose state reward values are specified as parameters. Can you please confirm this.

Best Xinwei

[volkm]

Hi Xinwei,

stormpy does support the analysis of DTMCs with parametric rewards. Parametric models can be built similar to non-parametric ones, see this code for an example. The analysis approach then depends on what you want to compute. The simplest option is to compute the rational function representing the reward, see for example this code in the same file.

If you tell us a bit more what exactly you want to analyse, we can help in guiding you to the right approach.

Best, Matthias

[xinwei2124]

Hi, Matthias

Thanks for your prompt reply. I looked into a bit and it is probably a bug in the code.

I analysed a reachability reward property ( R{\"totalCost\"}=?[F s=5] ) of a simple pDTMC (attached in the email).

It contains three parameters, they are p1, p2 and e1.

The stormpy successfully returned the expression, which contains all three parameters, but the parameter e1 is missing from the returned variables. Please see the screenshot attached.

Best Xinwei

On 31 Aug 2022, at 15:17, Matthias Volk @.***> wrote:

Hi Xinwei,

stormpy does support the analysis of DTMCs with parametric rewards. Parametric models can be built similar to non-parametric ones, see this code https://github.com/moves-rwth/stormpy/blob/master/tests/pars/test_parametric.py#L64 for an example. The analysis approach then depends on what you want to compute. The simplest option is to compute the rational function representing the reward, see for example this code https://github.com/moves-rwth/stormpy/blob/master/tests/pars/test_parametric.py#L11 in the same file.

If you tell us a bit more what exactly you want to analyse, we can help in guiding you to the right approach.

Best, Matthias

— Reply to this email directly, view it on GitHub https://github.com/moves-rwth/stormpy/issues/87#issuecomment-1233000444, or unsubscribe https://github.com/notifications/unsubscribe-auth/AO36O2AHRQ36GPOFZST3TJDV35SQNANCNFSM6AAAAAAQBKYKT4. You are receiving this because you authored the thread.

[volkm]

It seems that Github removes attachment when you reply by email. Can you upload your file(s) directly on Github? Then I will take a look at the issue.

[xinwei2124]

The model: toy.txt The property: R{\"totalCost\"}=?[F s=5]

The screenshot:

[volkm]

How did you obtain the list of parameters? Did you obtain them from the rational function or from the model? In the latter case, be sure to use model.collect_all_parameters().

[xinwei2124]

Thanks for your help. I incorrectly used model.collect_probability_parameters() to obtain the parameters.

[volkm]

I am happy to hear that this solves your problem.

For future reference: collect_probability_parameters() only collects the parameters on transitions, collect_reward_parameters() collects the parameters occurring in rewards, and collect_all_parameters() subsumes both and lists all parameters occurring in the model.