system verification engineers

Abstract: Decisiveness is central to reachability algorithms for infinite Markov chains, but is a qualitative notion: it guarantees that path-enumeration algorithms terminate, without an a priori bound on the horizon. We study decisiveness quantitatively of Markov chains, and apply our results to the approximate quantitative coverability problem for effective probabilistic well-structured transition systems (pWSTS). We introduce truncation sets, which represent the horizons sufficient to approximate the reachability probability within a precision $\varepsilon$. These sets reformulate decisiveness quantitatively, and their elements can be computed when it is decisive. To obtain such horizons, before any exploration, we introduce geometrically reachable sets, for which the probability of not reaching them within n steps decreases exponentially in n, up to a prefactor depending on the initial state. Horizons valid for all initial states exist iff this prefactor can be chosen uniformly for boundedly coarse chains. For such pWSTS, including probabilistic vector addition systems and Galton-Watson processes, we obtain a priori global horizons growing at most logarithmically in $1/\varepsilon$. In the non-uniform case, we give a drift condition ensuring the existence of a finite geometrically reachable set. Under this condition, we derive a priori horizons growing at most logarithmically in $1/\varepsilon$ and in the weight w(x) measuring the size of the initial state x. In both cases, we compute a horizon function whose evaluation on any initial state and precision requires only a constant number of elementary operations $(+, -, \times, / \text{ and } \log)$. For probabilistic lossy channel systems, this yields, to our knowledge, the first explicit a priori horizons from arbitrary initial states, and it extends to $ν$-pLCS, a new infinitely branching variant with probabilistic emissions.

Abstract: Safety verification of a Markov decision process (MDP) asks whether the probabilities of reaching several failure states jointly lie in a convex safe region under every scheduler. Watanabe and Unno (2026) prove safety by refining an outer approximation of the failure probabilities, where each query bounds a nonnegative weighted sum of the probabilities. Their rule selects weights by the largest Euclidean violation. We present a unified framework to measure violation in an explicitly chosen error unit: directions are scored by the support-function gap between the outer approximation and the safe region, normalized by the support function of the unit. We show that the maximal score, when positive, equals the smallest enlargement of the safe region in multiples of that unit that contains the outer approximation. The Euclidean unit recovers the earlier rule; two new rules are generated by the unit cube and the safe region itself. We experimentally evaluate how the choice of measurement rule affects the performance of safety verification for MDPs.