Computing steady-state probability vector

[temunds]

Hello everyone,

thank you for this tool, we use it on version 1.7.0, and it has been great for our purpose, computing the steady-state probability for a set of states in a ctmc. However, working on some more complex models recently, we expect to run into computation time issues when checking the desired property directly. Hence searching for ways to reduce the size of the state space, we came across the technique of lumping. Although we are still in the process of determining our detailed approach, we are considering a solution that requires more 'manual' handling of steady-state probabilities to modify transition rates in sequentially solved ctmcs. Since we would love to start the sequential solving utilizing stormpy, we are searching for a way to obtain the steady-state probabilities for all states in a considered ctmc.

Unfortunately, we have not been able to find an example describing how to obtain the desired results. Is there a method that does provide access to all steady-state probabilites of the considered state space?

Thanks in advance :)

[tquatmann]

Thanks for the kind words!
I just added the required bindings in PR #133.
See the test_modelchecking.py for example usage.

This should also work with Storm version 1.7.0 in case you have a good reason not to upgrade.

I'm closing the issue, feel free to re-open in case there are follow-up questions or if this is not what you need.

[temunds]

Awesome, thanks a lot :)