Sound Solution bounds for DTMC/MDP model checking methods by lukovdm · Pull Request #1066 · stormchecker/storm

lukovdm · 2026-09-22T13:11:57Z

Subsumes #1048

Builds on top of #1031.

This PR adds bounds for the following algorithms:

Value iteration (power method) — solver/NativeLinearEquationSolver.cpp (solveEquationsPower), solver/helper/ValueIterationHelper.cpp. A sweep that moved every entry one way proves the operand is a post- or pre-fixpoint, giving that side of the enclosure. Only for in-place (Gauss-Seidel) multiplication.
Value iteration (MinMax) — solver/IterativeMinMaxLinearEquationSolver.cpp (solveEquationsValueIteration). The same sweep certificate, claimed only when the caller has set hasUniqueSolution().
Sound value iteration — solver/helper/SoundValueIterationHelper.cpp, plus solveEquationsSoundValueIteration in both solvers. The enclosure SVI maintains, read out before the final averaging step collapses it. Needs both scaling factors to be known.
Guessing value iteration — solveEquationsGuessingValueIteration in both solvers. The two vectors GVI keeps, which hold verified guesses and so enclose the solution throughout.
Rational search — solveEquationsRationalSearch in both solvers. The solution as both bounds, once sharpening has verified an exact fixpoint.
Policy iteration — solver/IterativeMinMaxLinearEquationSolver.cpp (performPolicyIteration). Whatever the inner linear solver established. Optimality of the scheduler says nothing about the accuracy of the values.
State elimination — solver/EliminationLinearEquationSolver.cpp. The solution as both bounds; the method is direct.
Eigen SparseLU — solver/EigenLinearEquationSolver.cpp. The solution as both bounds. The iterative Eigen methods are left out.
Acyclic solving — solver/AcyclicLinearEquationSolver.cpp, solver/AcyclicMinMaxLinearEquationSolver.cpp. The solution as both bounds; values are substituted in topological order and final when written.
Topological solving — solver/TopologicalLinearEquationSolver.cpp, solver/TopologicalMinMaxLinearEquationSolver.cpp. An interval of ±precision around the result, under --sound only. The per-SCC deviations add to at most the configured precision along any chain.
Robust value iteration (interval models) — modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp (computeRobustValuesForMaybeStates). Whatever the MinMax solver produced. Now that is the sweep certificate, so rewards report and probabilities do not.

This is the ones I have tackled so far, I am not entirely certain these bounds are correct, but they all seem logical to me and when possible I tried to read the papers to find if they claim a bound. Please suggest other algorithms I can report bounds for.

lukovdm · 2026-09-24T07:51:49Z

Are there any algorithms that should be added. If not I will do another pass over the PR and then it should be ready for review.

tquatmann · 2026-09-24T08:39:31Z

Are there any algorithms that should be added. If not I will do another pass over the PR and then it should be ready for review.

I think this is a good list for now. My thoughts:

Topological: if all SCCs are singleton, we can set the exact bound (same as acyclic)
Step-bounded until, cumulative rewards, and Nest probabilities can get exact bounds
If some preprocessing bounds are provided to the solver, we may take those
If value iteration is started at a lower bound (like zero), it will always give a lower bound for the solution. Not sure if we can make use of this easily. The "A sweep that moved every entry one way"-approach sounds like it will affect runtime?

There might be some more algorithms, but we can always add them on demand.

Value iteration now certifies its own solution bound: while iterating it tracks whether the sequence is monotonically approaching the solution from one side and, if so, reports the final iterate as a sound bound in that direction. NativeLinearEquationSolver::solveEquationsPower and IterativeMinMaxLinearEquationSolver::solveEquationsValueIteration pass that through to the solution bounds of the solver. The topological solvers instead derive bounds from the precision they were asked to achieve. A sound topological solve hands every SCC a precision of eps divided by the length of the longest SCC chain, and the deviation an SCC inherits from its predecessors enters its own solution as a convex combination of the values at the exits, i.e. without amplification. The per-SCC deviations therefore add up to at most eps along any chain, so eps bounds the error of the overall solution and [x - d, x + d] is sound. The shared conversion from a precision to such an interval, including the relative criterion and the tightening with any a priori bounds, lives in the new AbstractEquationSolver::setSolutionBoundsFromPrecision. Nothing is claimed when soundness was not requested: an unsound solver only reports that its iteration stopped moving, which is no statement about the distance to the solution. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011oamBujHwK891QqnAYZ6Wr (cherry picked from commit c7bb8a4) (cherry picked from commit cb1eba635c9f36b086d1fa536ac957f7589c60a1)

The direction of an iteration is learned by comparing the new value of an entry against the one it overwrites. That is the previous iterate only when the operand is updated in place: with a regular multiplication the two operands alternate, so the entry being overwritten holds the iterate from two steps ago, and in the first iteration it holds whatever the auxiliary vector was left with by an earlier solve. Neither says anything about the direction of the step that was just taken, so an iteration that in fact decreased some entries could be reported as a lower bound, which is not merely loose but inverted. The convergence criterion reads the same entry and is unaffected, since across two steps of a monotone sequence it is a stricter test that stops later rather than earlier. A direction is not a distance, so it gets no such reprieve, and nothing is claimed unless the iteration ran in place. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BZPHMTb2xEncinYBJX3sjh (cherry picked from commit 4ab503b) (cherry picked from commit d831a7716bff0c3f78021cf0cab5a8a9d6037126)

The two directions were tested as alternatives, so an iteration in which the operator reproduced its operand reported only that the operand lies below the solution. Such an iteration establishes both sides at once: the operand is the fixed point, and the equation systems handed to this helper have only one, so it bounds itself from either side. Testing the two directions independently reports that as the point interval it is. Whether the iterates stopped moving because the system was solved outright or because the arithmetic ran out of precision is not distinguished, in keeping with the bounds being sound up to floating point throughout. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BZPHMTb2xEncinYBJX3sjh (cherry picked from commit c29ce70) (cherry picked from commit 8ac0bef2b32671818bc229bbb039232713cb03d2)

Both procedures keep the solution enclosed between two vectors in every iteration, which is the property they are named for, and both then collapse that enclosure into a single point estimate before returning. The enclosure is now read out first and reported as the bounds on the solution, as interval iteration already did. Neither needs to have converged for this: sound value iteration bounds the solution by its two scaling factors as soon as both are known, and guessing value iteration only ever writes a guess back once it has verified it, so the vectors it hands out enclose the solution throughout. An aborted run therefore reports a wider enclosure rather than none. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BZPHMTb2xEncinYBJX3sjh (cherry picked from commit 03f5d08) (cherry picked from commit 0248cd4967348335e18ba1897adfafc502bfc621)

Some procedures do not approach the solution but arrive at it: state elimination, an LU factorization, a single topologically ordered sweep over an acyclic system, and rational search once it has verified a sharpened candidate to be a fixed point. Each of those now reports its result as both the lower and the upper bound through the new AbstractEquationSolver::setSolutionBoundsExact, which is the strongest statement a solver can make about what it computed. Policy iteration is not among them. Its own termination says that the scheduler is optimal, not how accurately the values under that scheduler were computed, so it forwards whatever the last solve of the induced equation system established instead of claiming anything itself. That makes it exact when the inner solver is and silent when the inner solver is silent. Left out are the iterative Eigen methods, which stop at a tolerance like any other iteration, and the LP-based solver, whose backend may be an inexact one with a simplex tolerance that is a different thing from rounding. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BZPHMTb2xEncinYBJX3sjh (cherry picked from commit a932f8a) (cherry picked from commit 680b3a40a8be978176dfaf108e9523d41ccaafa7)

The value iteration and sound value iteration helpers gained their bounds out-parameter as a raw pointer, matching what interval and optimistic value iteration had before those were converted. This brings them into line, so that every helper in this directory hands the bounds back the same way. One site needed more than a mechanical edit: the MinMax value iteration builds the reference conditionally, since the direction certificate is only sound for a unique fixpoint, and OptionalRef deliberately has no assignment operator. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TfkAUfVqCKnSCRm3fAwJzL (cherry picked from commit fa3e93623ce8d12fb829e26741836d76119d94d7)

computeValuesForMaybeStates is shared between the probability and the reward paths and has been collecting the solver's bounds for both all along, but computeReachabilityRewardsHelper read only the values out of it, so every R=? query on an MDP dropped them. Embed them over the qualitative state sets the same way the until-probabilities path does: outside the maybe states the reward is exactly zero or exactly infinity, so the entries the result vector already holds bound those states from either side. computeTotalRewards may solve on an end component quotient and map the values back afterwards; the bounds get the same treatment, which is sound because all states of an eliminated end component share the value of their quotient state. Note that this is only claimed where the solver claims it: minimizing expected rewards does not give a unique solution unless the maybe states are free of end components, so plain value iteration keeps quiet there, while it does report for the maximizing direction. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BZPHMTb2xEncinYBJX3sjh (cherry picked from commit a3d6dc4) (cherry picked from commit c2eb32c68173987cd647432d52256eee1f3a5ad5)

Unlike the probability paths, which return a DTMCSparseModelCheckingHelperReturnType, the reward paths returned a bare vector and so had nowhere to put the bounds the linear equation solver produces; they never asked for them. Return the same type from computeReachabilityRewards, computeReachabilityTimes and computeTotalRewards, and read the bounds out where the values are read, embedding them over the states whose reward is qualitatively zero or infinity. Two callers only take the values, both because the bounds would need work that this commit does not do: - computeConditionalRewards solves on the Baier-transformed model, so the bounds it gets back are indexed by transformed states. - SparseCtmcCslHelper returns plain vectors of its own, so carrying the bounds further would mean changing the CSL helpers and their model checker too. That is the natural next step for CTMC reward queries. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BZPHMTb2xEncinYBJX3sjh (cherry picked from commit a656808) (cherry picked from commit a5f26aa0f2e3ee1ee89bbc421ed0a0b059a20f77)

filter(min, ...) and its siblings collapsed a result to a single number and threw the enclosure away, so the one place where a property asks a question of several states at once reported less than the per-state output right next to it. QuantitativeCheckResult gains an aggregate(FilterType), which reports the aggregate of the values together with the aggregate of each bound that is known. Every aggregation on offer is monotone in each individual value, so applying it to the lower resp. upper bounds bounds the aggregate of the values. The default implementation reports no bounds, which is right for the results that cannot carry any, so the symbolic and hybrid results need no change. The explicit result aggregates a bound by wrapping it in a result of its own and calling the very methods that aggregate the values, so the two kinds of aggregate cannot drift apart. average() is now defined through sum() rather than repeating its loop. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TfkAUfVqCKnSCRm3fAwJzL (cherry picked from commit d0d4c002e590aedb1e29fe8be71adaa9e25e023b) (cherry picked from commit 3574889b40d03067983b39a375478367a6fd3324)

The aggregating filters print the aggregate of each bound next to the aggregate of the values, so they follow the same convention the per-state output already uses: a side that was never proven prints as "-", and "inf" is kept for a bound that really is infinite. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TfkAUfVqCKnSCRm3fAwJzL (cherry picked from commit d35b237f12498f4a62ea74f46e79b3a4124abf8e)

A property whose every state is decided by the qualitative preprocessing never reaches an equation solver, so nothing set any bounds and a result that is known exactly was reported with no bound at all. P=? [F "a"] on a model where the target is reached almost surely is the plain case: the answer is 1 and it was being reported as though nothing were known about it. Where the maybe states come out empty there is no equation system, no placeholder is written anywhere, and every entry of the result comes from the graph analysis, so the values bound themselves from either side. All four helpers that build a result out of qualitative state sets now say so. Reward infinity is included: a state that cannot reach the target reports [inf, inf]. Nothing changes where maybe states remain. In particular no attempt is made to report the qualitative entries when the solver bounds the maybe states but the solver reports nothing, since bounds are held per result rather than per state and the maybe entries would have to be filled with something meaningless. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TfkAUfVqCKnSCRm3fAwJzL (cherry picked from commit cf526abc37bc5dfc508b40d2eb28a793a6847699) (cherry picked from commit b381d5c) (cherry picked from commit 8afe1da1f77b4a9b00ca42e37a4ff610585a3351)

Reachability on an interval DTMC is handed to the very MinMax solvers the MDP helper uses, so those solvers were producing bounds and computeRobustValuesForMaybeStates was returning only the values. It now hands the bounds back as well, and the two callers place them the same way they place the values: the probability path takes them over whole, since for interval models the result for the maybe states covers every state, while the reward path embeds them over the maybe states into the qualitative entries the result already holds. Only the reward path reports today, and that is the gate working rather than a gap. For interval models every method falls back to robust value iteration, whose bound is the direction certificate, and that is claimed only where the caller asserts a unique fixpoint -- which this helper does for rewards, on the strength of the graph-preservation check, and not for probabilities. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TfkAUfVqCKnSCRm3fAwJzL (cherry picked from commit 848679e991f073b8168d8c7a73ca3336f3539231) (cherry picked from commit 30ed498) (cherry picked from commit b692c9a9492ce8cd8d27e055ecde0593946387f6)

Same pass as on the first change: comments that restate the code or a member name are removed, as are notes about work that is not done, and the ones that remain say in one or two sentences what the code cannot. The value iteration argument, the topological precision argument and the policy iteration one are the three worth keeping at length, and each is now about half of what it was. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TfkAUfVqCKnSCRm3fAwJzL

lukovdm · 2026-09-29T09:40:33Z

@tquatmann This is ready for review. The VI path could take the most attention.

lukovdm · 2026-09-30T06:50:00Z

@volkm Could I get a copilot review here?

Copilot

Copilot review overview

🟡 Changes recommended

Three unresolved findings affect bound propagation, solver-status handling, and topological precision soundness.

Review effort: Lite
Findings: 1 · 1

Open (2)

Check solver status before publishing exact bounds · New
Preserve solution bounds in the interval-model branch · New

What changed in this PR

This PR adds sound lower and upper solution bounds across linear solvers and DTMC/MDP model-checking result pipelines.

Changes:

Adds exact, directional, interval, and precision-based solver bounds.
Propagates bounds through model-checking helpers and aggregate results.
Extends tests and CLI bound reporting.

Review findings:

Critical (4 votes): Eigen SparseLU publishes exact bounds without checking solver status.
Moderate (2 votes): Robust interval-model branches omit MinMax bounds at lines 792 and 1497.
Moderate (1 vote): Topological precision bounds use native-solver settings instead of delegated solver settings.

File	Reviewed change
`src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp`	Tests solver bounds.
`src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp`	Tests exact MDP results.
`src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp`	Tests exact DTMC results.
`src/storm/solver/TopologicalMinMaxLinearEquationSolver.h`	Declares topological MinMax bound handling.
`src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp`	Reports topological MinMax bounds.
`src/storm/solver/TopologicalLinearEquationSolver.h`	Declares topological linear bound handling.
`src/storm/solver/TopologicalLinearEquationSolver.cpp`	Reports topological linear bounds.
`src/storm/solver/SolutionBounds.h`	Adds bound transformations and exactness utilities.
`src/storm/solver/NativeLinearEquationSolver.cpp`	Tracks bounds for native methods.
`src/storm/solver/MinMaxLinearEquationSolver.cpp`	Finalizes MinMax bounds.
`src/storm/solver/LinearEquationSolver.cpp`	Finalizes linear-solver bounds.
`src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp`	Adds bounds to MinMax algorithms.
`src/storm/solver/helper/ValueIterationHelper.h`	Extends value-iteration APIs.
`src/storm/solver/helper/ValueIterationHelper.cpp`	Tracks value-iteration enclosures.
`src/storm/solver/helper/SoundValueIterationHelper.h`	Extends sound value-iteration APIs.
`src/storm/solver/helper/SoundValueIterationHelper.cpp`	Exposes sound iteration bounds.
`src/storm/solver/EliminationLinearEquationSolver.cpp`	Reports exact elimination results.
`src/storm/solver/EigenLinearEquationSolver.cpp`	Reports exact SparseLU results.
`src/storm/solver/AcyclicMinMaxLinearEquationSolver.cpp`	Reports exact acyclic MinMax results.
`src/storm/solver/AcyclicLinearEquationSolver.cpp`	Reports exact acyclic results.
`src/storm/solver/AbstractEquationSolver.h`	Adds bound-management APIs.
`src/storm/solver/AbstractEquationSolver.cpp`	Implements bound finalization and precision bounds.
`src/storm/modelchecker/results/QuantitativeCheckResult.h`	Adds aggregate-bound result types.
`src/storm/modelchecker/results/QuantitativeCheckResult.cpp`	Implements aggregation defaults.
`src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h`	Adds explicit bound aggregation APIs.
`src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp`	Implements explicit bound aggregation.
`src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp`	Propagates MDP bounds.
`src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp`	Propagates DTMC bounds.
`src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp`	Transforms and propagates MDP bounds.
`src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h`	Updates DTMC helper return types.
`src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp`	Computes and propagates DTMC bounds.
`src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp`	Adapts DTMC helper results.
`src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h`	Adapts changed helper results.
`src/storm-cli/model-handling-main-cli.h`	Prints aggregate bounds.

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

This was referenced Sep 22, 2026

Sound Solution bounds for CTMC model checking methods #1067

Draft

Sound solution bounds for conditional model checking of MDPs #1068

Draft

lukovdm marked this pull request as draft September 22, 2026 13:14

lukovdm mentioned this pull request Sep 22, 2026

Upper and lower bounds for more algorithms #1048

Closed

lukovdm requested a review from tquatmann September 24, 2026 07:50

lukovdm and others added 13 commits September 28, 2026 14:28

lukovdm force-pushed the soundresults-deterministic branch from 4f53705 to bd95f90 Compare September 28, 2026 12:47

Add more algs

912543d

volkm modified the milestones: 2.0, 1.15 Sep 29, 2026

Fix comments, add tests and small things

033cbfc

lukovdm marked this pull request as ready for review September 29, 2026 09:39

lukovdm added the ready for review label Sep 29, 2026

Solve CI and add better widening of bounds after modelchecking

f5d640e

volkm requested a lite review from Copilot September 30, 2026 07:21

Copilot started reviewing on behalf of volkm September 30, 2026 07:21 View session

Copilot AI reviewed Sep 30, 2026

View reviewed changes

Comment thread src/storm/solver/EigenLinearEquationSolver.cpp

Comment thread src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

Add test and fix LU bounds and add bounds for interval until probs

8eb3523

Navigation Menu

Sound Solution bounds for DTMC/MDP model checking methods - #1066

Sound Solution bounds for DTMC/MDP model checking methods#1066
lukovdm wants to merge 17 commits into
stormchecker:masterfrom
lukovdm:soundresults-deterministic

lukovdm commented Sep 22, 2026 •

edited

Loading

Uh oh!

lukovdm commented Sep 24, 2026

Uh oh!

tquatmann commented Sep 24, 2026

Uh oh!

lukovdm commented Sep 29, 2026

Uh oh!

lukovdm commented Sep 30, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

This branch has not been deployed

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

lukovdm commented Sep 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

lukovdm commented Sep 24, 2026

Uh oh!

tquatmann commented Sep 24, 2026

Uh oh!

lukovdm commented Sep 29, 2026

Uh oh!

lukovdm commented Sep 30, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Copilot review overview

🟡 Changes recommended

Uh oh!

Uh oh!

Uh oh!

This branch has not been deployed

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

lukovdm commented Sep 22, 2026 •

edited

Loading