Add CVaR model checking for sparse MDP rewards - #983
Draft
pjtimm wants to merge 67 commits into
Draft
Conversation
Bucket terminal rewards, cache transposes and prefix sets, prune impossible thresholds via reachability checks, and extract schedulers only for the winning LP.
Cache choice-cost offsets and reachable state lists, reserve action-front storage, use binary-search frontier lookup, and avoid vector erase during hull pruning.
Remove a redundant target-state check and add a fused scaled Minkowski operation so SSP action-front computation avoids creating temporary scaled frontiers.
Merge sorted action frontiers, canonicalize already-sorted point sets without resorting, and compact duplicate, dominated, and convex-redundant points in place.
Use convex-chain Minkowski sums, reuse frontier-layer scratch storage, and switch sorted Pareto-front union merging to a heap-based merge.
Move SSP Pareto layer application into a dedicated operator with backend-style action reduction, keeping the CVaR helper focused on frontier-window initialization, cost-bound iteration, and candidate extraction.
# Conflicts: # src/storm/environment/SubEnvironment.cpp # src/storm/environment/modelchecker/AllModelCheckerEnvironments.h # src/storm/environment/modelchecker/ModelCheckerEnvironment.cpp # src/storm/environment/modelchecker/ModelCheckerEnvironment.h
tquatmann
marked this pull request as draft
August 18, 2026 08:35
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This PR adds scalar CVaR model checking for reward-reachability queries on sparse MDPs. It allows users to analyze the tail of a reward or cost distribution.
The weighted-reachability backend uses an LP for terminal-reward models. SSP minimum-cost and maximum-reward queries use Pareto front value iteration.
Scope
Queries have the form
R{"reward"}min/max=? [ F "target" ]together with
--cvar <alpha>, where0 < alpha < 1.The current implementation supports sparse MDPs with one initial state. Each backend checks its own assumptions on rewards, target states, and SSP structure and rejects unsupported models.
Testing
Created tests in
CvarQueryTestpass. They cover query parsing and validation, the weighted-reachability and SSP backends, cost and reward interpretations, preprocessing, exact rational inputs, and rejection of unsupported models.