search

moves-rwth / stormpy

Python Bindings for the Probabilistic Model Checker Storm
https://moves-rwth.github.io/stormpy/
GNU General Public License v3.0
30 stars 16 forks source link

Getting DTMC from given MDP and policy #118

Closed MrBly closed 1 year ago

MrBly commented 1 year ago

Hi, I have an MDP that I have successfully built into a stormpy model and model checked. I have a policy giving an action for each state. How can I best get a DTMC from the MDP as it acts by the policy?

I've tried to modify the MDP before building it into a stormpy model, but I've gotten errors both ways I've tried. Removing all sub-optimal actions and continuing to treat it as an MDP causes an error: empty row group in the MinMax equation system. (Though, having checked, all the MDP's row groups have at least one entry).

Model type: MDP (sparse) States: 50000 Transitions: 188419 Choices: 50000 Reward Models: none State Labels: 21 labels

Removing all transitions belonging to sub-optimal actions and building it as a DTMC causes an error: the equation system has no solution. This approach also warns me Level 2 Warning in storm/resources/3rdparty/gmm-5.2/include/gmm/gmm_precond_ilu.h, line 182: pivot 1832 is too small (among other pivots).

Model type: DTMC (sparse) States: 50000 Transitions: 188419 Reward Models: none State Labels: 21 labels

Basically, I'm confused by these errors and warnings, and want to know how to fix my model, or how I can impose my policy on the MDP in a more stormpythonic way.

Thanks!

volkm commented 1 year ago

Hi, stormpy provides explicit support for getting the DTMC from an MDP as induced by a scheduler. Please see this test for an example. Does this provide you the desired functionality?

MrBly commented 1 year ago

I saw this, but it's not clear to me how to provide my own scheduler. What format does the scheduler take? How can I initialize my own schedule object to apply to the MDP?

Thanks!

I can confirm that the test example works for my model in a simple example, but need to be able to specify the scheduler myself.

On Tue, May 2, 2023, 00:23 Matthias Volk @.***> wrote:

Hi, stormpy provides explicit support for getting the DTMC from an MDP as induced by a scheduler. Please see this test https://github.com/moves-rwth/stormpy/blob/master/tests/storage/test_scheduler.py#L69 for an example. Does this provide you the desired functionality?

— Reply to this email directly, view it on GitHub https://github.com/moves-rwth/stormpy/issues/118#issuecomment-1531004659, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAUN2ON5UYHN64PYB67TYBDXECY7FANCNFSM6AAAAAAXSO4U3E . You are receiving this because you authored the thread.Message ID: @.***>

MrBly commented 1 year ago

When I use the formula 'Pmax = ? [ (G "aq2") ]' on the MDP to extract a scheduler, a valid scheduler is retrieved. But when applied to my MDP to induce a DTMC, the resulting DTMC causes model checking to return "RuntimeError: InvalidOperationException: The equation system has no solution."

MrBly commented 1 year ago

It seems my MDP had some actions that included transitions with probability 0, and that was causing this error. I'd still like a method to create a scheduler from scratch to induce a DTMC.

EDIT: I then tried to check a different property, and was told that "The equation system has no solution."

volkm commented 1 year ago

stormpy currently has no methods to create a scheduler from scratch. You can only extract a scheduler from a model checking query. In principle we could add support for manually creating schedulers.

For a better understanding, could you give us a bit more context why you want to create your own schedulers? And what type of schedulers do you want to use? Are memoryless deterministic schedulers sufficient for your purpose? Feel free to contact us via email if you do not want to share these details publicly.

MrBly commented 1 year ago

Hi, and thanks for your attention to this.

Memoryless deterministic schedulers are sufficient, as I'm trying to check approximate policies found for MDPs. That is, empirically, what properties of the induced MC are different under different approximation schemes? For that I have number of policy approximation algorithms, which return a policy. So I'd like to create my own scheduler for each and check the induced MC.

MrBly commented 1 year ago

Hi, and thanks for your attention to this.

Memoryless deterministic schedulers are sufficient, as I'm trying to check approximate policies found for MDPs. That is, empirically, what properties of the induced MC are different under different approximation schemes? For that I have number of policy approximation algorithms, which return a policy. So I'd like to create my own scheduler for each and check the induced MC.

I'm also OK with simply applying the scheduler myself and producing a new storm DTMC model, but many properties that I am trying to check are successfully checked on the MDP, but when I check on the re-built DTMC I get the error: WARN (GmmxxLinearEquationSolver.cpp:123): Iterative solver did not converge within 1 iteration(s). ERROR (TopologicalLinearEquationSolver.cpp:157): The equation system has no solution.

tquatmann commented 1 year ago

Is it possible for you to create a small example that would help us to reproduce this error?

MrBly commented 1 year ago

I'm actually concerned that this problem might be one of scale. The models that I get this kind of error on are fairly large. I could potentially share a model with you, and the code that produces such an error, if that would be helpful. Otherwise, I will have to search for a smaller component of my model that produces the error.

tquatmann commented 1 year ago

Maybe we can find the issue on the large model already. You can send it potentially via email and/or using a file sharing service.

MrBly commented 1 year ago

How should I export my models to you? (pickle.dump doesn't work, for example)

volkm commented 1 year ago

You can use the function stormpy.export_to_drn(model, file) (see here) which exports the model in our custom DRN format. Note that this export uses an explicit text format and depending on your model size the resulting file might be quite large.

MrBly commented 1 year ago

storm_dtmc.tar.gz storm_mdp.tar.gz

The first file is the DTMC in DRN format that was elicited from the second file - the MDP in DRN format.

Both models satisfy 'P <= 0.2 [ G "aq0" ]' at state 0, but when I check 'P <= 0.2 [ F "aq0" ]', I get "False" for the MDP, but many warnings like Level 2 Warning in /home/.../storm/resources/3rdparty/gmm-5.2/include/gmm/gmm_precond_ilu.h, line 182: pivot 1715 is too small, and a couple warnings like WARN (GmmxxLinearEquationSolver.cpp:123): Iterative solver did not converge within 1 iteration(s)., and then the error ERROR (TopologicalLinearEquationSolver.cpp:157): The equation system has no solution. for the DTMC.

tquatmann commented 1 year ago

Thanks for providing these. I think I figured out the problem:

Your model contains many very low transition probabilities, like 10^{-20} or even 10^{-40}. I noticed that there are quite a few states where several successors have a probability close to 0 and one successor has probability 1 (I assume this is actually something very close to 1 but got rounded up to 1, at least in the .drn files). This causes numerical issues. The warning you see is gmm (the linear equation system solving library we use) complaining about that.

This is not an issue for the MDP since we detect that the maximal probability to reach an aq0 state is 1 using graph-based algorithms, so no equation system solving is needed.

Is it intended that your model has such low probabilities? If not, you should delete such transitions (i.e. round them down to 0 and make sure that the remaining transitions sum up to 1).

If your application requires working with these numerically challenging values, I recommend to not use finite precision floats. Storm offers support for exact (arbitrary precision) rational numbers, see e.g. here.

MrBly commented 1 year ago

Thanks for catching that! I had written code to fix those probabilities, but I had my condition backwards, and missed that it didn't work. With that code fixed, the DTMC solver works, so I'm closing the issue. But do you know what the minimum precision in probabilities should be, so I can make sure my code respects that?

tquatmann commented 1 year ago

Great to hear that things work now :)

I don't think there is a definite answer to your last question. Small transition values can theoretically make a big difference: think of a 2-state DTMC where we go from initial state A to the target state B with probability $\varepsilon$ and from A to A with probability $1-\varepsilon$. Then, the probability to reach B from A is 1 for all $\varepsilon > 0$ but the probability drops to 0 if $\varepsilon = 0$.

If possible for your application, you should avoid such transitions, e.g., by adding program logic that determines if a transition should have value 0. One could also use arbitrary precision arithmetic as I mentioned before.

Finally, if you want an unscientific answer that "probably kind of works in practice", I would try putting $10^{-6}$ there. This is also our default precision parameter for numerical methods.