Implemented support for verifying IDTMCs #808

plindnercs · 2025-11-12T17:20:20Z

This feature extension includes IDTMC support to verify the following properties:

Reachability Probabilities
Reach-Reward
Propositional

Note:

As discussed in issue Add support for explicit scheduler-nature optimization directions in uncertain (interval) models #807, the results for Pmin, Pmax, Rmin and Rmax are flipped compared to PRISM.
The expected results in the unit tests were double-checked with PRISM and manually verified by computing them by hand (except for the BRP-32-2 test case).
If the minmax:method is not manually set to vi, the current implementation prints a warning and defaults to robust value iteration. This is somewhat related to issue Default selected method not supported (dd's) #264. Note that the warning currently appears twice as the minmax:method is checked in two places.
The implementation heavily relies on the IMDP implementation (see Support for interval-based transitions in storm #409)
This pull request should solve the first item and second item, at least for IDTMCs, in Support for interval models #762

I'm happy to receive any kind of feedback!

…propositional model checking for interval DTMCs

…probabilities

tquatmann

Good progress! My comment regarding the interval optimization direction is related to #807 .

tquatmann · 2025-11-17T14:58:20Z

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

+    solver->setHasUniqueSolution(false);
+    solver->setHasNoEndComponents(false);
+    solver->setLowerBound(storm::utility::zero<SolutionType>());
+    solver->setUpperBound(storm::utility::one<SolutionType>());


The upper bound of 1 does not apply if we compute expected rewareds

tquatmann · 2025-11-17T16:28:08Z

src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

+    Environment const& env, CheckTask<storm::logic::UntilFormula, SolutionType> const& checkTask) {
    storm::logic::UntilFormula const& pathFormula = checkTask.getFormula();
+    if (storm::IsIntervalType<ValueType>) {
+        STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,


It's a bit odd that the optimization direction controls nature for IDTMCs (but not for IMDPs, it seems).
Suggestion: the interval optimization direction should be stored as an std::optional<storm::OptimizationDirection> in the Checktask (and then checked e.g. here). That forces an API user to set it explicitly.
When creating a checktask from a formula, the interval optimization direction can be derived automatically (following PRISM behaviour).

Of course, this also means that we have to read the IntervalOptimizationDirection from the SolveGoal (somewhere in the Helper).

tquatmann · 2025-11-17T16:28:38Z

src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

+    Environment const& env, CheckTask<storm::logic::EventuallyFormula, SolutionType> const& checkTask) {
    storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
+    if (storm::IsIntervalType<ValueType>) {
+        STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,


…probabilities

…uncertainty should be resolved by nature. This flag is required as soon as interval models are being checked.

src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp

volkm · 2025-12-29T14:55:53Z

src/storm/utility/ConstantsComparator.h

@@ -1,5 +1,7 @@
 #pragma once

+#include "storm/adapters/IntervalAdapter.h"


Is it possible to keep the include only in the cpp file? This avoids costly includes of carl in header files.

With the current design (ValueType precision; stored by value), this is not possible, because ValueType needs to be complete at the point where ConstantsComparator<ValueType> is instantiated. However, as an alternative, we could change it to std::shared_ptr<const ValueType> precision, and use the precision variable by dereferencing the pointer in the implementation (ConstantsComparator.cpp). This would avoid requiring ValueType to be complete in the header. If that is acceptable, then I can change the code accordingly.

let's change that to

Suggested change

#include "storm/adapters/IntervalAdapter.h"

#include "storm/adapters/IntervalForward"

The pointer solution would yield a runtime overhead

Incorporating this change results in the following error while executing the tests locally on my machine (same as before adding the include for IntervalAdapter.h):
error: ‘storm::utility::ConstantsComparator<ValueType>::precision’ has incomplete type.

…probabilities

tquatmann

Thanks for the contribution! Looks good, I just have some nitpicks :)

src/test/storm/modelchecker/prctl/mdp/RobustMdpPrctlModelCheckerTest.cpp

src/storm/solver/UncertaintyResolutionMode.h

src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h

tquatmann · 2026-01-02T13:02:39Z

src/storm/utility/ConstantsComparator.h

@@ -1,5 +1,7 @@
 #pragma once

+#include "storm/adapters/IntervalAdapter.h"


let's change that to

Suggested change

#include "storm/adapters/IntervalAdapter.h"

#include "storm/adapters/IntervalForward"

The pointer solution would yield a runtime overhead

src/storm/settings/modules/MinMaxEquationSolverSettings.cpp

src/storm/modelchecker/CheckTask.h

tquatmann · 2026-01-03T04:56:23Z

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

    }

-    return result;
+    // Solve the corresponding system of equations.


We actually need to check the requirements. Something like

auto req = solver->getRequirements(env); if (!computeReward) { req.clearbounds(); } STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");

Temporarily fixed in dee5cad. I hope this is okay for now.

I think we should throw already at this point. If the solver requires an upper bound and we ignore that requirement, it will fail or (even worse) terminate with a wrong result.

On another note: We should have negative rewards in mind. This means that 0 is not necessarily a lower bound. (I know there are still some parts that assume non-negative rewards).

Is there an issue with my suggestion?

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

sjunges · 2026-01-03T20:08:39Z

What does it even mean that we use an interval as precision in the constants comparator?

volkm · 2026-01-05T09:56:56Z

The following patch should handle the includes for ConstantsComparator.
patch.txt

volkm · 2026-01-05T09:57:49Z

I can also push the changes to this PR if you want.

plindnercs · 2026-01-05T23:02:14Z

What does it even mean that we use an interval as precision in the constants comparator?

Intuitively, I would have expected a behaviour like this, where we interpret the precision bounds as tolerances on the interval bounds:

storm::Interval precision(0.1, 0.15);
storm::Interval candidateA(0.3, 0.3);
storm::Interval candidateB(0.2, 0.4);
storm::Interval candidateC(0.1, 0.4);

storm::utility::ConstantsComparator<storm::Interval> constantsComparator(precision, false);

EXPECT_TRUE(constantsComparator.isEqual(candidateA, candidateB));
EXPECT_FALSE(constantsComparator.isEqual(candidateA, candidateC));
EXPECT_TRUE(constantsComparator.isEqual(candidateB, candidateC));

If this is not the intended semantics, then maybe we need to discuss this more thoroughly.

plindnercs · 2026-01-05T23:02:29Z

I can also push the changes to this PR if you want.

That would be great. Thank you!

About the failing build: is this due to an error in my implementation, or is it caused by the pipeline itself? I might be missing something, but I could not infer this from the error messages.

volkm · 2026-01-06T15:03:17Z

I have merged the recent changes from master. This should fix the build issue on Alpine.

sjunges · 2026-01-06T15:05:43Z

@plindnercs so you use two precisions, one for the lower bound and one for the upper bound? Is this a hypothetical use case, or a real one?

plindnercs · 2026-01-06T15:40:03Z

@plindnercs so you use two precisions, one for the lower bound and one for the upper bound? Is this a hypothetical use case, or a real one?

Yes, you can see it that way. Right now, it is only a hypothetical use case as far as I know. At least the implementation that I contributed does not make use of this directly.

tquatmann · 2026-01-09T08:50:07Z

@plindnercs so you use two precisions, one for the lower bound and one for the upper bound? Is this a hypothetical use case, or a real one?

Yes, you can see it that way. Right now, it is only a hypothetical use case as far as I know. At least the implementation that I contributed does not make use of this directly.

I'd be in favour of using the most obvious semantics for now, until something else is required. To me, "most obvious semantics" would be to have IntervalBaseType<ValueType> as type of precision and then apply that precision to both, lower and upper interval boundaries

Edit: I realise that this, again, requires the IntervalForward include in the ConstantsComparator.
I don't know how to prevent that. @volkm any idea?

…ainty resolution mode.

tquatmann

Thanks! Just some final remarks.

I also pushed a change to the storm::api::createTask interface. In my opinion, this should explicitly ask for an uncertainty resolution mode when dealing with interval models.

tquatmann · 2026-01-09T09:11:07Z

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

    }

-    return result;
+    // Solve the corresponding system of equations.


I think we should throw already at this point. If the solver requires an upper bound and we ignore that requirement, it will fail or (even worse) terminate with a wrong result.

On another note: We should have negative rewards in mind. This means that 0 is not necessarily a lower bound. (I know there are still some parts that assume non-negative rewards).

Is there an issue with my suggestion?

tquatmann · 2026-01-09T09:16:26Z

src/storm/settings/modules/IOSettings.cpp

+    } else if (uncertaintyResolutionModeString == "cooperative") {
+        return UncertaintyResolutionModeSetting::Cooperative;
+    } else if (uncertaintyResolutionModeString == "both") {
+        STORM_LOG_ERROR("Uncertainty resolution mode 'both' not yet supported.");


STORM_LOG_ASSERT(false ...

with the validator above, this should not be reachable. It's better to just fail for now.

tquatmann · 2026-01-09T09:26:09Z

src/storm/solver/helper/ValueIterationHelper.cpp

+                                                                                   uint64_t& numIterations, SolutionType const& precision,
+                                                                                   const std::function<SolverStatus(const SolverStatus&)>& iterationCallback,
+                                                                                   MultiplicationStyle mult,
+                                                                                   const UncertaintyResolutionMode& uncertaintyResolutionMode) const {


For consistency: UncertaintyResolutionMode const&

tquatmann · 2026-01-09T09:33:03Z

src/storm/solver/UncertaintyResolutionMode.cpp

            return false;
-        }
+        case UncertaintyResolutionMode::Unset:
+            STORM_LOG_WARN("Uncertainty resolution mode not set properly, assuming to resolve uncertainty in a robust fashion.");


STORM_LOG_THROW(false, ...

sjunges · 2026-01-09T10:36:27Z

@plindnercs so you use two precisions, one for the lower bound and one for the upper bound? Is this a hypothetical use case, or a real one?

Yes, you can see it that way. Right now, it is only a hypothetical use case as far as I know. At least the implementation that I contributed does not make use of this directly.

I'd be in favour of using the most obvious semantics for now, until something else is required. To me, "most obvious semantics" would be to have IntervalBaseType<ValueType> as type of precision and then apply that precision to both, lower and upper interval boundaries

I fully second this. In particular, I would not even allow instantiating the constants comparator with intervals...

volkm · 2026-01-09T15:55:35Z

Edit: I realise that this, again, requires the IntervalForward include in the ConstantsComparator.
I don't know how to prevent that. @volkm any idea?

I think the IntervalForward is okay to include. Up until now, I managed to avoid including it, because ValueType is only later instantiated in the cpp and it was somehow okay to delay the actual include to the class which later uses it, for example in the tests. Maybe that is still possible.

plindnercs added 4 commits November 12, 2025 18:02

Implemented support for reachability probabilities, reach-reward and …

6922fea

…propositional model checking for interval DTMCs

Applied code formatting

13d40bc

Check for Z3 being available on certain tests

71705ff

Merge remote-tracking branch 'upstream/master' into imc-reachability-…

8acb6f7

…probabilities

tquatmann reviewed Nov 18, 2025

View reviewed changes

plindnercs added 4 commits November 18, 2025 17:44

Merge remote-tracking branch 'upstream/master' into imc-reachability-…

6d37341

…probabilities

Merge remote-tracking branch 'upstream/master' into imc-reachability-…

2b76334

…probabilities

Merge remote-tracking branch 'upstream/master' into imc-reachability-…

6765a8a

…probabilities

Implemented explicit flag 'uncertainty-resolution' to decide how the …

072f87a

…uncertainty should be resolved by nature. This flag is required as soon as interval models are being checked.

plindnercs mentioned this pull request Dec 10, 2025

Add support for explicit scheduler-nature optimization directions in uncertain (interval) models #807

Open

plindnercs commented Dec 10, 2025

View reviewed changes

src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp Show resolved Hide resolved

plindnercs requested a review from tquatmann December 12, 2025 19:45

plindnercs added 2 commits December 16, 2025 12:58

fixed warnings

eddd5be

merged incoming changes

c2cff21

volkm reviewed Dec 29, 2025

View reviewed changes

Merge remote-tracking branch 'upstream/master' into imc-reachability-…

5858817

…probabilities

tquatmann requested changes Jan 3, 2026

View reviewed changes

plindnercs added 2 commits January 3, 2026 19:58

incorporated feedback of @tquatmann

dee5cad

added optimization direction handling for IDTMCs

4e0ccd8

plindnercs requested a review from tquatmann January 3, 2026 19:46

Avoid include of IntervalAdapter.h in ConstantsComparator.h

94f95c5

Merge from branch 'master'

fcb6a03

API: createTask for interval models now explicitly requires an uncert…

3e5bd6b

…ainty resolution mode.

tquatmann requested changes Jan 9, 2026

View reviewed changes

tquatmann mentioned this pull request Jan 9, 2026

IMDPs: Improved support for reachability rewards and reachability probabilities #853

Draft

Suppress unused lambda capture warning.

f3d75e1

		@@ -1,5 +1,7 @@
		#pragma once

		#include "storm/adapters/IntervalAdapter.h"

	#include "storm/adapters/IntervalAdapter.h"
	#include "storm/adapters/IntervalForward"

Implemented support for verifying IDTMCs #808

Are you sure you want to change the base?

Implemented support for verifying IDTMCs #808

Uh oh!

Conversation

plindnercs commented Nov 12, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tquatmann left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tquatmann left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

sjunges commented Jan 3, 2026

Uh oh!

volkm commented Jan 5, 2026

Uh oh!

volkm commented Jan 5, 2026

Uh oh!

plindnercs commented Jan 5, 2026

Uh oh!

plindnercs commented Jan 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

volkm commented Jan 6, 2026

Uh oh!

sjunges commented Jan 6, 2026

Uh oh!

plindnercs commented Jan 6, 2026

Uh oh!

tquatmann commented Jan 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tquatmann left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

sjunges commented Jan 9, 2026

Uh oh!

plindnercs commented Nov 12, 2025 •

edited

Loading

plindnercs commented Jan 5, 2026 •

edited

Loading

tquatmann commented Jan 9, 2026 •

edited

Loading

volkm commented Jan 9, 2026 •

edited

Loading