Model checking a CTMC usually means asking a question like P(X(t) = n) — the transient probability of being in a particular state at a particular time. The standard way to compute it exactly is uniformization: all exit rates are rescaled to a single uniform rate q, the chain becomes a discrete-time walk paced by a Poisson clock, and the transient distribution is the Poisson-weighted sum of matrix steps. PRISM and Storm use this same core algorithm; Stamina’s reachability machinery is built around it too.

Set the start state and time of interest. The bars show the exact full distribution P(X(t) = n) — no simulation involved.