Add upper and lowerbounds to check results.

[lukovdm]

This PR adds upper and lower bounds to ExplicitQuantitativeCheckResults and implements this for OVI and II. Further algorithms are implemented it #1048.

Upper and lower bounds are stored in a class SolutionBounds. It has an optional vector of lower bounds and an optional vector of upper bounds. No bound mean the algorithm did not try to give any bounds, infinity as a value in the bound means the algorithm tried and that is the best it came up with.

The ExplicitQuantitativeCheckResults and ExplicitQualitativeCheckResults have had there map option removed and instead get an optional bitvector states holding the states for which the values and bounds hold. This was done such that the vectors in the SolutionBounds can be used easily in conjuction with any values stored in the check results. ExplicitQualitativeCheckResults was update to be consistent with ExplicitQuantitativeCheckResults.

Solution bounds are passed around from helper to PRCTLmodel checker using (MDP/DTMC)SparseModelCheckingHelperReturnType, the dtmc variant is new.

Solution bounds in this PR have been implemented for OVI and II.

Printing of bounds has been implemented where no bound is reported with a - if no bound is present. This was done to differentiate it from infinities.

So far I have the convention that any non-maybe states get bounds that exist from the algorithm. So if only lower bounds are produced, the maybe states get 1 [1, -] where - is no bound. This could be changed.

[lukovdm]

I will do a pass over the code and clean up any weird AI smells, this draft is mostly so I can have early feedback on the architecture.

[sjunges]

What if we dont have upper bounds? We could of course then have a vector of infinities, but is that better than not having the vector?

…

On 24 Aug 2026, at 16:25, Matthias Volk ***@***.***> wrote: @volkm commented on this pull request. In src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h <#1031 (comment)>: > @@ -85,9 +115,26 @@ class ExplicitQuantitativeCheckResult : public QuantitativeCheckResult<ValueType return t == typeid(ValueType); } - // The values of the quantitative check result. + /*! + * Asserts that the given bounds have the same shape as the values. + */ + void assertBoundsShape(boost::variant<vector_type, map_type> const& bounds) const; + + /*! + * Writes the value of the given state, followed by its bounds if any are known. + */ + void printValue(std::ostream& out, storm::storage::sparse::state_type state) const; + + // The values of the quantitative check result. These are estimates of the actual values, which lie within + // the bounds below but carry no further guarantee. boost::variant<vector_type, map_type> values; I would keep the pair of vectors. I agree that this is more performant. In the current version using SolutionBounds = std::optional<std::pair<std::vector<ValueType>, std::vector<ValueType>>>; so it would should already fit. I would just use these new type to make sure we have a consistent handling of the bounds. — Reply to this email directly, view it on GitHub <#1031?email_source=notifications&email_token=ADH67DEJPZ5B7V6MZSHU3K35LRF4HA5CNFSNUABKM5UWIORPF5TWS5BNNB2WEL2QOVWGYUTFOF2WK43UKJSXM2LFO4XTKMBQHA4TAMBTG4ZKM4TFMFZW63VHMNXW23LFNZ2KKZLWMVXHJLDGN5XXIZLSL5RWY2LDNM#discussion_r3844377461>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ADH67DGPWG5TA7POLSFVIID5LRF4HAVCNFSNUABEKJSXA33TNF2G64TZHM3TCMZZGU2TANB3JFZXG5LFHM2TEMBTGQ4DMMRXG2QXMAQ>. Triage notifications, keep track of coding agent tasks and review pull requests on the go with GitHub Mobile for iOS <https://github.com/notifications/mobile/ios/ADH67DFXCQZQYPAHHOSEK6L5LRF4HA5CNFSNUABKM5UWIORPF5TWS5BNNB2WEL2QOVWGYUTFOF2WK43UKJSXM2LFO4XTKMBQHA4TAMBTG4ZKM4TFMFZW63VHMNXW23LFNZ2KKZLWMVXHJKTGN5XXIZLSL5UW64Y> and Android <https://github.com/notifications/mobile/android/ADH67DBQMNA44YIDJS6UDFT5LRF4HA5CNFSNUABKM5UWIORPF5TWS5BNNB2WEL2QOVWGYUTFOF2WK43UKJSXM2LFO4XTKMBQHA4TAMBTG4ZKM4TFMFZW63VHMNXW23LFNZ2KKZLWMVXHJLTGN5XXIZLSL5QW4ZDSN5UWI>. Download it today! You are receiving this because you commented.

[volkm]

Is there a difference between infinity and undefined or can they be considered the same?
For example, a conditional probability should throw an exception if the condition is not reachable but one could also set the result to undefined. There could also be a difference between not calculating the upper bound (undefined) and calculating it but getting infinity (for example in reward queries)? But I am not sure whether there is actually a distinction to be made.

[lukovdm]

I guess there is a difference between I tied to find an upperbound as this is the best I came up with and I did not even try to find one. That would be the difference between infinite and undefined. But not trying is usually for all states while infinite could be for some states.

[lukovdm]

This PR now includes moving away from a map in the ExplicitQua(nt/l)itativeCheckResults. This allows for using the SolutionBounds as the upper and lower bounds in the CheckResults

[lukovdm]

I have split of most algorithms to an new PR #1048. I think this PR should be ready for a more thorough review now. I have nothing more I want to add here.

[Copilot]

🟡 Changes recommended

Unresolved moderate findings remain in bounds propagation and result handling.

Get a fresh assessment by requesting another Copilot review.

Pull request overview

This pull request adds optional lower and upper solution bounds to explicit model-checking results and propagates bounds from OVI and interval iteration.

Changes:

• Introduces SolutionBounds and solver bound lifecycle support.
• Updates result APIs and bounds propagation across model-checking helpers.
• Adds bounds tests and registers them.

File summaries

File	Summary
src/test/storm/modelchecker/bounds/SolutionBoundsTest.cpp	Adds DTMC and MDP bounds tests.
src/test/storm/CMakeLists.txt	Registers bounds tests.
src/storm/solver/SolutionBounds.h	Defines optional lower and upper bounds.
src/storm/solver/NativeLinearEquationSolver.cpp	Integrates solver-bound handling.
src/storm/solver/MinMaxLinearEquationSolver.cpp	Integrates solver-bound handling.
src/storm/solver/LinearEquationSolver.cpp	Integrates solver-bound handling.
src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp	Integrates solver-bound handling.
src/storm/solver/helper/OptimisticValueIterationHelper.h	Exposes OVI bound outputs.
src/storm/solver/helper/OptimisticValueIterationHelper.cpp	Reused outputs can retain a stale upper bound before verification.
src/storm/solver/helper/IntervalterationHelper.h	Convenience II overload cannot request or forward bounds.
src/storm/solver/helper/IntervalterationHelper.cpp	Extracts interval-iteration bounds.
src/storm/solver/AbstractEquationSolver.h	Stores solver-produced bounds.
src/storm/solver/AbstractEquationSolver.cpp	Manages stored solver bounds.
src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h	Adds bound-aware result storage and access.
src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp	Bounds can be omitted from compact output, retained stale, or mishandled at endpoints.
src/storm/modelchecker/results/ExplicitQualitativeCheckResult.h	Refactors optional state subsets.
src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp	Updates qualitative result filtering and access.
src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp	Updates explicit result construction.
src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp	Attaches helper bounds to MDP results.
src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp	Attaches helper bounds to DTMC results.
src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h	Carries bounds through the MDP helper API.
src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp	Interval and end-component paths drop or fail to transform bounds.
src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h	Carries bounds through the DTMC helper API.
src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp	Robust interval-DTMC path does not populate returned bounds.
src/storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h	Adds bounds to the helper return type.
src/storm/modelchecker/prctl/helper/DTMCModelCheckingHelperReturnType.h	Adds bounds to the helper return type.
src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp	Product-DTMC path drops bounds before the final result.
src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp	Global CTMC path drops helper bounds.
src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp	CTMC wrapper drops DTMC helper bounds.
src/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.cpp	Updates qualitative state access.
src/storm-dft/modelchecker/DFTModelChecker.cpp	Updates result filtering.
src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h	Adapts helper result access.
src/storm-counterexamples/api/counterexamples.cpp	Adapts helper result access.
.gitignore	Adds ignored local metadata.

Review details

Suppressed comments (7)

src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp:320

• The product DTMC result now carries solutionBounds, but this path moves only .values into prodNumericResult. Any OVI/II enclosure is discarded before LTL model-checking returns its quantitative values; project the lower/upper vectors alongside the values and propagate them to the final result.

                                          .values);

src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp:298

• For interval DTMCs, the robust solver path above fills result but never fills solutionBounds; this newly returned field is therefore always empty for that branch even when the min-max solver computed an enclosure. Propagate and embed the robust solver's lower/upper vectors before returning the result.

    returnValue.solutionBounds = std::move(solutionBounds);

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp:794

• The interval-model branch reaches this assertion after computeValuesForMaybeStates has produced a result object, but the following assignment copies only its values. Any lower/upper vectors returned by the solver are dropped, so interval checks report no bounds despite the non-interval branch propagating them. Copy resultForMaybeStates.solutionBounds into resultBounds here.

                    STORM_LOG_ASSERT(resultForMaybeStates.getValues().size() == transitionMatrix.getColumnCount(), "Dimensions do not match.");

src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp:187

• SolutionBounds uses an unset side to mean that no bound was produced, but this setter only updates sides that are present and leaves any previously stored side untouched. Reusing a result and calling setBounds with only a lower (or only an upper) bound therefore exposes a stale bound that is not guaranteed for the new values. Clear this->bounds before applying the incoming sides.

void ExplicitQuantitativeCheckResult<ValueType>::setBounds(storm::solver::SolutionBounds<ExtendedValueType> bounds) {
    if (bounds.hasLower()) {
        this->setLowerBounds(std::move(*bounds.lower));
    }
    if (bounds.hasUpper()) {
        this->setUpperBounds(std::move(*bounds.upper));

src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp:410

• The strict interior test misses thresholds equal to either reported endpoint, even though those comparisons can still be undecided. For example, with an enclosure [0, 0.5], comparing an approximate value against value < 0.5 can return true while the exact value is 0.5, but this condition emits no warning. Account for endpoint cases (and the comparison operator) when deciding whether the result is sound.

            STORM_LOG_WARN_COND(!((*bounds.lower)[offset] < bound && bound < (*bounds.upper)[offset]),
                                "The bound " << bound << " lies between the lower bound " << (*bounds.lower)[offset] << " and the upper bound "
                                             << (*bounds.upper)[offset] << ", so the comparison against it is not decided at state " << offset << ".");

src/storm/solver/helper/IntervalterationHelper.h:43

• The bounds output parameter was added to the overload that exposes numIterations, but the convenience overload immediately below still has no way for callers to request SolutionBounds and its implementation forwards no output reference. This makes the new bounds API unavailable through one of the two public II entry points (unlike the corresponding OVI overloads); add the optional reference to this overload and forward it.

                    storm::OptionalRef<SolutionBounds<ValueType>> solutionBounds = storm::NullRef) const;

src/storm/solver/helper/OptimisticValueIterationHelper.cpp:285

• If a caller reuses the output SolutionBounds object, an OVI run that terminates before verification leaves the previous upper vector intact because this branch only assigns upper on convergence. That stale upper vector is then reported as if it were sound for the new run; clear the supplied bounds before writing the new lower/conditional upper result.

• Files reviewed: 33/34 changed files
• Comments generated: 4
• Review effort level: Lite

---

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