Skip to content

Sound Solution bounds for CTMC model checking methods - #1067

Draft
lukovdm wants to merge 21 commits into
stormchecker:masterfrom
lukovdm:soundresults-timed
Draft

Sound Solution bounds for CTMC model checking methods#1067
lukovdm wants to merge 21 commits into
stormchecker:masterfrom
lukovdm:soundresults-timed

Conversation

@lukovdm

@lukovdm lukovdm commented Sep 22, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Builds on #1066 and contains some algorithms from #1048.

  • CTMC until probabilities — csl/helper/SparseCtmcCslHelper.cpp (computeUntilProbabilities). Reduces to the embedded DTMC, so the linear equation solver's bounds are handed through instead of dropped.
  • CTMC globally probabilities — csl/SparseCtmcCslModelChecker.cpp. The until bounds, inverted through SolutionBounds::invertProbabilityBounds().
  • CTMC reachability rewards — SparseCtmcCslHelper.cpp (computeReachabilityRewards). Same reduction to the embedded DTMC.
  • CTMC total rewards — SparseCtmcCslHelper.cpp (computeTotalRewards).
  • CTMC reachability times — SparseCtmcCslHelper.cpp (computeReachabilityTimes), via reachability rewards with exit rates as state rewards.
  • CTMC next probabilities — csl/SparseCtmcCslModelChecker.cpp. A single multiplication on the embedded probability matrix, so the values are reported as exact.
  • Markov automaton until probabilities — csl/SparseMarkovAutomatonCslModelChecker.cpp. Reduces to the embedded MDP; the helper already returned bounds and the model checker was discarding them.
  • Markov automaton globally probabilities — same file, straight through SparseMdpPrctlHelper.
  • Markov automaton reachability rewards — same file.
  • Markov automaton total rewards — same file.
  • Markov automaton reachability times — same file.
  • Markov automaton next probabilities — same file. One multiplyAndReduce, reported as exact.

@lukovdm
lukovdm marked this pull request as draft September 22, 2026 13:14
@lukovdm lukovdm mentioned this pull request Sep 22, 2026
Closed
@lukovdm lukovdm changed the title Sound Solution bounds for CTMC model checking methods - #1066 Sound Solution bounds for CTMC model checking methods Sep 24, 2026
lukovdm and others added 16 commits September 28, 2026 14:28
@lukovdm @claude
Report solution bounds from value iteration and the topological solvers
028ce43 
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)
@lukovdm @claude
Claim a value iteration bound only for an in-place iteration
448975e 
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)
@lukovdm @claude
Report both bounds for an iteration that moved nothing
2013f72 
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)
@lukovdm @claude
Report the enclosures that sound and guessing value iteration maintain
dbad7d4 
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)
@lukovdm @claude
Report a solution as exact where the procedure ends at it
a0a5354 
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)
@lukovdm @claude
Pass the value iteration bounds by OptionalRef as well
149123b 
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)
@lukovdm @claude
Report the solution bounds that MDP reward queries already produce
6a48f15 
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)
@lukovdm @claude
Give the DTMC reward paths a channel for the solution bounds
7f03693 
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)
@lukovdm @claude
Carry the bounds through the aggregating filters
f48ed79 
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)
@lukovdm @claude
Write an unknown aggregate bound as a dash as well
8352e61 
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)
@lukovdm @claude
Report values the graph analysis settles as exact
3d86b6f 
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)
@lukovdm @claude
Report the bounds the robust interval solve produces
4fd6d4a 
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)
@lukovdm @claude
Trim the comments added for the solution bounds
bd95f90 
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
Add more algs
912543d
@lukovdm
Fix comments, add tests and small things
033cbfc
@lukovdm
Solve CI and add better widening of bounds after modelchecking
f5d640e
lukovdm and others added 3 commits September 29, 2026 13:38
@lukovdm @claude
Report solution bounds for CTMC reachability queries
490ab4e 
Until probabilities, reachability times, reachability rewards and total rewards
on a CTMC are all reductions to the corresponding query on the embedded DTMC,
so the linear equation solver was producing bounds on them already and the CTMC
helper was dropping them on the floor. The four now return the same type the
DTMC helper does and hand what they get straight through.

That return type is no longer DTMC-specific, so it is renamed to
DeterministicSparseModelCheckingHelperReturnType: it fits both models exactly,
as neither has nondeterminism for a scheduler to resolve. It stays next to the
MDP one, which is likewise used from the CSL helpers.

Bounded until keeps taking only the values. It reduces to unbounded reachability
only for the interval [0, inf] and otherwise goes through uniformization, which
produces no bounds, so reporting them for the one case would be inconsistent.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01TfkAUfVqCKnSCRm3fAwJzL
(cherry picked from commit d07454ff76093d8b1c9572fa0515c785afb2bb11)
(cherry picked from commit 746cbd764d0e63bcd84c852f5aefde4701367ec7)
@lukovdm @claude
Report solution bounds for CTMC globally probabilities
cad6aa4 
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_017n6Z1D3qCc4kFkU1moVg5L
(cherry picked from commit 97fe3562f52675a20243ff48993baf344083e86e)
@lukovdm @claude
Trim the comments added for the CTMC solution bounds
6410d43 
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_017n6Z1D3qCc4kFkU1moVg5L

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@lukovdm