Discrepancies in LRA results (exact vs non-exact and in Docker vs outside Docker)

[marisgg]

Hello!

In the attached box.drn (attached as box.txt as .drn is not allowed) describing a DTMC, we observe a significant difference between the results for R=? [ LRA ] obtained from Storm with and without --exact mode. Furthermore, for normal mode, we notice a difference between running inside Docker with the official Storm image for 1.11.1 (movesrwth/storm:1.11.1) and outside Docker (with a local Storm 1.11.1 installation).

The result from the exact mode (~4.7) is the result we would expect from the given model.

With non-exact (normal), we get warnings such as Iterative solver did not converge within 650 iteration(s). See below.

The commands used are:

• storm -drn box.drn -prop 'R=? [ LRA ]' for normal mode
• storm -drn box.drn -prop 'R=? [ LRA ]' --exact for exact mode

This may be a bug. Still, we're curious about how the LRA solver works internally in Storm and what properties DTMCs need to satisfy for accurate LRA (e.g., ergodicity), so we're happy to receive any pointers on that as well.

Outside Docker

Normal mode (unexpected result, different from inside Docker)

Storm 1.11.1

Date: REDACTED
Command line arguments: -drn box.drn -prop 'R=? [ LRA ]'
Current working directory: REDACTED

Time for model construction: 0.031s.

-------------------------------------------------------------- 
Model type:     DTMC (sparse)
States:         692
Transitions:    1988
Reward Models:  state_rewards
State Labels:   2 labels
   * others -> 691 item(s)
   * init -> 1 item(s)
Choice Labels:  none
-------------------------------------------------------------- 

Model checking property "1": R=? [LRA] ...
WARN  (GmmxxLinearEquationSolver.cpp:133): Iterative solver did not converge within 650 iteration(s).
Result (for initial states): 0.1621230201
Time for model checking: 0.013s.

Exact mode (provides expected result)

Storm 1.11.1

Date: REDACTED
Command line arguments: -drn box.drn -prop 'R=? [ LRA ]' --exact
Current working directory: REDACTED

Time for model construction: 0.034s.

-------------------------------------------------------------- 
Model type:     DTMC (sparse)
States:         692
Transitions:    1988
Reward Models:  state_rewards
State Labels:   2 labels
   * others -> 691 item(s)
   * init -> 1 item(s)
Choice Labels:  none
-------------------------------------------------------------- 

Model checking property "1": R=? [LRA] ...
Result (for initial states): 7162421502770909416536148542922100806422506642794095715805852820934134364848710405660011125025088579168541687133508650680212735099753117159848395190338331671530598443584400918056130110499589858387269847081838468574328918654072199585532922053709762114076110160528088374410107757895543405784028949749322403837269019711753146836058745585535645606045064554341311232772642290176712784932234144871720425971088407069191334047841255927044328679317136/1524160011107888041327815318385702144027890236968364998220827485670179543719738543535189444324780549945132276168165433947941275733831296484895374315237970149228420262351625551129637420792708024812917643893757379710057428158793780346975663842459183882442235084739662981503612147390477408810108596856813982800012486544685276883140521893768268949434715895548115755054004829165212867851389115207032958363308723696669205626457223156070031668961647 (approx. 4.699258248)
Time for model checking: 0.295s.

Inside Docker

Normal mode (unexpected result, and different from outside Docker)

Storm 1.11.1

Date: REDACTED
Command line arguments: -drn box.drn -prop 'R=? [ LRA ]'
Current working directory: REDACTED

Time for model construction: 0.030s.

-------------------------------------------------------------- 
Model type:     DTMC (sparse)
States:         692
Transitions:    1988
Reward Models:  state_rewards
State Labels:   2 labels
   * others -> 691 item(s)
   * init -> 1 item(s)
Choice Labels:  none
-------------------------------------------------------------- 

Model checking property "1": R=? [LRA] ...
WARN  (GmmxxLinearEquationSolver.cpp:133): Iterative solver did not converge within 1400 iteration(s).
Result (for initial states): 78.83970964
Time for model checking: 0.022s.

Exact mode (with expected result)

Storm 1.11.1

Date: REDACTED
Command line arguments: -drn box.drn -prop 'R=? [ LRA ]' --exact
Current working directory: REDACTED

Time for model construction: 0.033s.

-------------------------------------------------------------- 
Model type:     DTMC (sparse)
States:         692
Transitions:    1988
Reward Models:  state_rewards
State Labels:   2 labels
   * others -> 691 item(s)
   * init -> 1 item(s)
Choice Labels:  none
-------------------------------------------------------------- 

Model checking property "1": R=? [LRA] ...
Result (for initial states): 7162421502770909416536148542922100806422506642794095715805852820934134364848710405660011125025088579168541687133508650680212735099753117159848395190338331671530598443584400918056130110499589858387269847081838468574328918654072199585532922053709762114076110160528088374410107757895543405784028949749322403837269019711753146836058745585535645606045064554341311232772642290176712784932234144871720425971088407069191334047841255927044328679317136/1524160011107888041327815318385702144027890236968364998220827485670179543719738543535189444324780549945132276168165433947941275733831296484895374315237970149228420262351625551129637420792708024812917643893757379710057428158793780346975663842459183882442235084739662981503612147390477408810108596856813982800012486544685276883140521893768268949434715895548115755054004829165212867851389115207032958363308723696669205626457223156070031668961647 (approx. 4.699258248)
Time for model checking: 0.287s.

box.txt

[tquatmann]

Hi!

There is no hard structural requirement on the DTMC. However, some Markov chains (like this one apparently) are numerically challenging.

For DTMCs, there are essentially three methods (which you can pick with the --lra:detmethod command line switch

• gain-bias-equations (default) constructs and solves a linear equation system following this paper
• lra-distribution-equations constructs and solves a different linear equation system that encodes the steady-state (or stationary) distribution of the Markov chain.
• value-iteration which roughly follows this approach

Now the first two methods use a solver for linear equation systems (GMM++ by default). And because this is using iterative numerical methods, the approach can suffer from badly conditioned matrices. That is why we see the warning message, which essentially says: "don't trust the result!". In fact, I get -8.727522666 on my machine.
For similar reasons, Value iteration is also not helpful.

You seem to have a numerically challenging model. We often have this, e.g., when there are many high-probability cycles. I would recommend the --exact switch, which solves the linear equation systems using exact (arbitrary precision) rational number arithmethic (no floating points) and direct methods (LU Decomposition in the EIgen library).

By the way: you can also compute the entire steady state distribution, if that is interesting for your usecase:
storm -drn box.txt --steadystate --exportresult res.json --exact produces a file res.json. What we observer here is that most states are visited with rather rare probability (like 10^-20)

[marisgg]

Hi Tim,

Thanks for your response and for sharing your insights. I do not yet know the answer to your question as to what exactly makes this Markov chain challenging, I'll investigate in the new year.

If we can detect that the result has not converged, running these models in exact mode in these specific challenging cases should be fine. Is there a way to do this programmatically? We're building on top of the Storm C++ API and I did not find an easy way to check that.

If there is no existing solution, would it be possible to provide this kind of information in the checkresult?

[volkm]

Detection of non-convergence would actually be good in my view. We currently only warn but still continue. We could for example use the NoConvergenceException in these cases (which exists but is never used).

[sjunges]

With lack of convergence, does one want to get the actual result still? For some solvers, this may be a safe lower bound?

[volkm]

It would at least be good to have dedicated handling for these cases. At the moment, we return false for solveEquations in case of non-convergence but this return value seems to not be checked for most function calls.

[marisgg]

I think it would be great to have something to handle these cases, especially programmatically. A use-case for us in the C++ API is to, e.g., detect lack of convergence and switch to exact analysis only when necessary.

In another light of this issue, is there a paper or reference around which the analysis of the R=? [ LRA ] property for DTMCs in Storm is based that I can read?

[tquatmann]

I reference two papers in my previous post. They focus on MDPs, but the results carry over to DTMCs.
In particular, we compute the LRA values for each BSCC individually. Details should be in this paper, iirc.

The lra-distribution-equation approach computes the steady state (or stationary) distribution by constructing and solving an equation system. You should find some details in any textbook on DTMC.

Towards the convergence detection: Yes, we should somehow pass that to the CheckResult so that CLI users get a more explicit error message and API users can react on that.

To do this properly, I fear that this would require changes all over the place.

@marisgg if a quick and hacky solution is fine for your use case, you could e.g. throw a custom exception iff one of the solveEquations invocations in the file SparseDeterministicInfiniteHorizonHelper.cpp return false. Your API invocation can then catch that and restart solving with exact mode.

[marisgg]

@tquatmann, thanks for your quick response and suggestion. I'm sorry; for some reason, I looked over those papers you mentioned when revisiting the issue.

I'll look into your suggested hacky solution.