Add support for explicit scheduler-nature optimization directions in uncertain (interval) models

[plindnercs]

For checking uncertain (interval) models, the PRISM Property Specification allows explicitly specifying the optimization direction for both the scheduler and nature. In contrast, in STORM's current implementation for IMDPs, nature’s optimization direction is implicitly chosen as the adversarial one with respect to the scheduler’s direction. e.g., when checking Pmax=? [F "done"], nature acts in a worst-case fashion and minimizes the probability, resulting in Pmaxmin=? [F "done"].
At the moment, it is not possible in STORM to check properties where both optimization directions are explicity given, e.g., Pmaxmax=? [F "done"].

In my opinion, it would be nice if STORM supports properties like Pmaxmax=? [F "done"], as this is also possible in PRISM. Additionally, while working on my pull request adding support for IDTMCs, I noticed that checking Pmax=? [F "done"] yields the same result in STORM as checking Pmin=? [F "done"] in PRISM. This is due to the fact, that the optimization direction is interpreted as the one for the scheduler and not nature, and hence the robust value iteration minimizes the probability by a worst-case behaviour of nature.

In PRISM, if only one optimization direction is given for an IMDP, this optimization direction is chosen for both the scheduler and nature, e.g., Pmax=? is interpreted as Pmaxmax=?. However, when checking Pmaxmax=? on an IDTMC, PRISM currently returns an error.

[volkm]

Is this an issue with the parsing of the property? As far as I can see from this test Storm in principle already has support for specifying both optimization directions.

[plindnercs]

Yes, I think this is an issue with the parsing.

[tquatmann]

e.g., when checking Pmax=? [F "done"], nature acts in a worst-case fashion and minimizes the probability [for IDTMC]

I'd suggest to set the optimization direction (i.e. Minimize or Maximize for intervals explicitly in the CheckTask and SolveGoal. Right now it is a Boolean robust flag that defaults to true which I find confusing for IDTMC.

IMO, the behaviour should be like this (API users can overwrite by explicitly setting the interval optimization directions in the Checktask)

• IDTMC:
  • Pmax=? [ .. ] maximizes the described probability among all interval instantiations.
  • Pmin=? [ .. ] similarly minimizes.
  • P=? [ .. ] throws an exception as it doesn't specify how to resolve the intervals.
  • Pmaxmin=? [ .. ] and similar combinations should work (and consider the second direction for the intervals).
• IMDP:
  • Pmaxmin=? [ .. ] maximizes over MDP schedulers and minimizies over interval resolutions.
  • Pminmax=? [ ..] , Pminmin=? [ .. ], Pmaxmax=? [ .. ] are similar.
  • Pmax=? [ .. ] and Pmin=? [ .. ] throw an exception as they don't specify how to resolve the intervals. P=? [ .. ] should also throw ( I believe it does this already)

This mostly mimics the behaviour of PRISM (correct me if I'm wrong @plindnercs ) except

• we would allow Pmaxmin=? [ .. ] etc. for IDTMC (I would expect this as we also allow Pmax=? for (non-interval) DTMC
• we would not allow Pmax=? [ .. ] etc. for IMDP: We so-far defaulted to the robust interpretation which is reasonable in many contexts, but not in line with the PRISM behaviour.

For API users, one could also think about using (e.g. in the checktask):

enum class IntervalOptimizationMode { Minimize, Maximize, Robust, Cooperative };

Where Robust (or Cooperative) means that the intervals should do the inverse of (or the same as) the provided optimization direction.

Edit: Changed "Angelic" to "Cooperative"

[sjunges]

Hey!

I agree that robust should be replaced by natureOptimizationDirection, or so. Note however that setting the default is a bit more annoying. I therefore think the API should allow the options as given by Tim (I would use angelic (vs demonic) but rather cooperative).

I am not sure I am superhappy with the prism-style Pmaxmin style notation. I always have to look this up. In particular, I also think it is a bit dangerous that for Pmax has a different interpretation for the special case that an imdp is a idtmc and for the special case that an imdp is an mdp.

I would therefore like to propose that one can write --interval-resolution {min, max, robust, cooperative }. Maybe that should be a required flag with no default for MDPs.

We can also talk to Dave to get his 2 cents on the maxmax...

Sebastian

[tquatmann]

I edited to cooperative as it fits better, indeed.

I'm absolutely in favour of setting the interval resolution more explicitly.
Your suggestion also means that we don't have to tinker with the OperatorFormulas and the FormulaParser which is a nice side effect :)

I would then be in favour of saying (in CLI) --interval-resolution <val> must be present iff the input is an interval model. API users also have to set that explicitly (e.g. in the checktask).

Only downsides are that

• PRISM users can't use their properties out-of-the-box.
• Users that want the entire interval of possible values need either two CLI calls or stormpy.

[sjunges]

The latter point could be adressed by allowing --interval-resolution both.

[tquatmann]

Sounds good. both would just be a command line option (i.e. nothing you could specify in a CheckTask) and essentially doubles the properties to check.

Shall we go with that for now? We can always add Pmaxmin style properties if there ever is an actual need for them.

[plindnercs]

Hi @tquatmann , @sjunges!
I have now implemented the functionalities discussed here in my pull request (#808), except for the functionality of --uncertainty-resolution both.
To support this, I would have to make changes to multiple method signatures in, for example model-handling.h (e.g. adding another parameter to the verificationCallback function) and others. In my opinion, under the current structure, these changes would unnecessarily clutter the code and the interfaces for a use-case that only applies to uncertain models. Therefore, I would suggest leaving out the both option for now and maybe add it later if it gets requested.

Note that I chose the name uncertainty-resolution rather than interval-resolution to be more general, in case Storm might support other uncertain models in the future.