Fix incorrect exit rates in DD-based Markov automaton bisimulation quotients

[tquatmann]

Summary

Fixes #498: bisimulation minimization changed model checking results for Markov automata.

Root cause: DD-based bisimulation quotient extraction (the Dd quotient format, used e.g. by the hybrid engine) built the quotient's transition matrix directly from the model's already-normalized transition matrix. For Markov automata, this matrix stores normalized probabilities for Markovian choices — the actual rates live separately in the exit-rate vector. Passing this normalized matrix into the quotient's MarkovAutomaton constructor made it re-derive the exit rate from the (already-summing-to-1) matrix, collapsing every Markovian state's exit rate to 1. This silently corrupted all time- and reward-based properties (e.g. Tmin/Tmax) after --bisimulation, while probability properties stayed correct — matching the exact symptom reported in the issue.

Fix: scale Markovian choices back to their original (unnormalized) rates before building the quotient's transition matrix, so the quotient's re-derived exit rates come out correct. Adjusted the affected sanity-check assertions accordingly (they assumed a fully-normalized matrix, which is no longer the case for Markovian rows).

Test plan

• Added a regression test (MarkovAutomatonExitRates) with a small MA model (resources/examples/testfiles/ma/bisimulation_exit_rates.ma) whose bisimilar states get merged; verified it fails without the fix (wrong result 1 instead of 0.25) and passes with it.
• Manually re-verified against the model from the issue: hybrid --bisimulation, hybrid --bisimulation --bisimulation:origvars, and dd-to-sparse --bisimulation:quot dd all now agree with the unminimized result.
• Full test-storage and test-modelchecker-csl suites pass.

🤖 Generated with Claude Code

[Copilot]

🟡 Changes recommended

The original-variable path can still lose Markovian exit rates, and its regression coverage is missing.

Get a fresh assessment by requesting another Copilot review.

Pull request overview

This PR fixes incorrect Markovian exit rates in DD-based bisimulation quotients and adds regression coverage.

Changes:

• Restores rate-weighted Markovian transitions.
• Updates related sanity checks.
• Adds a regression model and Tmin test.

File summaries

File	Reviewed change
src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp	Adds exit-rate regression coverage; original-variable mode remains untested.
src/storm/storage/dd/bisimulation/QuotientExtractor.cpp	Restores rates during quotient extraction; the original-variable conversion path still requires preserving exit rates.
resources/examples/testfiles/ma/bisimulation_exit_rates.ma	Adds the regression Markov automaton model.

Review details

Suppressed comments (2)

src/storm/storage/dd/bisimulation/QuotientExtractor.cpp:1287

• The new regression test only uses the default BisimulationOptions::useOriginalVariables = false, so it exercises extractQuotientUsingBlockVariables but never this extractQuotientUsingOriginalVariables path. A future regression in the explicitly supported --bisimulation:origvars mode would therefore remain undetected even though this fix duplicates the rate-scaling logic here. Please parameterize the regression over both extraction modes or add a second run with useOriginalVariables = true.

        storm::dd::Add<DdType, ValueType> transitionMatrix = model.getTransitionMatrix();
        if (modelType == storm::models::ModelType::MarkovAutomaton) {
            auto const& markovAutomaton = *model.template as<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>();
            transitionMatrix = transitionMatrix * markovAutomaton.getMarkovianMarker().ite(markovAutomaton.getExitRateVector(),
                                                                                           model.getManager().template getAddOne<ValueType>());

src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp:313

• This regression test uses the default BisimulationOptions, so it exercises only extractQuotientUsingBlockVariables. The PR also changes extractQuotientUsingOriginalVariables, used by --bisimulation:origvars, but there is no test coverage for useOriginalVariables; add the same time assertion with that option enabled so the second extraction path cannot regress independently.

        std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient(storm::dd::bisimulation::QuotientFormat::Dd);

• Files reviewed: 3/3 changed files
• Comments generated: 1
• Review effort level: Lite

---

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

[Copilot]

🔵 Needs a closer look

Expression conversion can reintroduce reserved init/deadlock labels and reject valid models in five files.

Review details

Suppressed comments (5)

src/storm/models/symbolic/Ctmc.cpp:105

• This re-adds reserved labels after they were intentionally erased above. A model may legally have an expression label named deadlock; getStates("deadlock") resolves to the special deadlock BDD, and the BDD-label constructor then rejects the resulting deadlock entry as an illegal custom label and throws. Skip init/deadlock entries when materializing expression labels.

    for (auto const& labelExpressionPair : this->getLabelToExpressionMap()) {
        newLabelToBddMap.emplace(labelExpressionPair.first, this->getStates(labelExpressionPair.first));
    }

src/storm/models/symbolic/Dtmc.cpp:61

• This re-adds reserved labels after they were intentionally erased above. A model may legally have an expression label named deadlock; getStates("deadlock") resolves to the special deadlock BDD, and the BDD-label constructor then rejects the resulting deadlock entry as an illegal custom label and throws. Skip init/deadlock entries when materializing expression labels.

    for (auto const& labelExpressionPair : this->getLabelToExpressionMap()) {
        newLabelToBddMap.emplace(labelExpressionPair.first, this->getStates(labelExpressionPair.first));
    }

src/storm/models/symbolic/MarkovAutomaton.cpp:145

• This re-adds reserved labels after they were intentionally erased above. A model may legally have an expression label named deadlock; getStates("deadlock") resolves to the special deadlock BDD, and the BDD-label constructor then rejects the resulting deadlock entry as an illegal custom label and throws. Skip init/deadlock entries when materializing expression labels.

    for (auto const& labelExpressionPair : this->getLabelToExpressionMap()) {
        newLabelToBddMap.emplace(labelExpressionPair.first, this->getStates(labelExpressionPair.first));
    }

src/storm/models/symbolic/Mdp.cpp:57

• This re-adds reserved labels after they were intentionally erased above. A model may legally have an expression label named deadlock; getStates("deadlock") resolves to the special deadlock BDD, and the BDD-label constructor then rejects the resulting deadlock entry as an illegal custom label and throws. Skip init/deadlock entries when materializing expression labels.

    for (auto const& labelExpressionPair : this->getLabelToExpressionMap()) {
        newLabelToBddMap.emplace(labelExpressionPair.first, this->getStates(labelExpressionPair.first));
    }

src/storm/models/symbolic/StochasticTwoPlayerGame.cpp:94

• This re-adds reserved labels after they were intentionally erased above. A model may legally have an expression label named deadlock; getStates("deadlock") resolves to the special deadlock BDD, and the BDD-label constructor then rejects the resulting deadlock entry as an illegal custom label and throws. Skip init/deadlock entries when materializing expression labels.

    for (auto const& labelExpressionPair : this->getLabelToExpressionMap()) {
        newLabelToBddMap.emplace(labelExpressionPair.first, this->getStates(labelExpressionPair.first));
    }

• Files reviewed: 9/9 changed files
• Comments generated: 0 new
• Review effort level: Lite

[volkm]

LGTM. Thanks for fixing this important issue.

[volkm]

Could we also check the same for exact?

[volkm]

The handling of rate matrix vs probability matrix reminded me of #826. If we have a CTMC representation as probability matrix + exit rate we need to be careful of this issue as well. I think for now it is considered a rate matrix.
I noticed that there is also no CTMC bisimulation test. Might also be good to add it at some point.