Feature Request: Scheduler extraction in step-bounded reachability analysis

[MaximeBouton]

Given an MDP in the explicit format, for reachability formulas involving G , F{op}k or U{op}k, the model checking result returns a vector with the maximum probability of satisfying the formulas but not the associated scheduler.

It would be nice to support scheduler extraction for reachability analysis in MDP.

See also this issue: moves-rwth/stormpy#3

[cdehnert]

Dear Maxime,

thanks for your request, we will add it to our long wish list. This is just to tell you that we will most likely not address this in the foreseeable future, simply because we are lacking resources and the list is very long. Sorry about that.

As Storm is open source, you might want to think about implementing this yourself to get it done more quickly.

Best wishes, Chris

[sjunges]

Storm now supports extraction of schedulers for the unbounded case, i.e., for finally and until, but not for the step-bounded variants. The issue remains thus open, but I think a changed title is adequate.