Quantitative methods improve reachability estimates in probabilistic infinite systems
Quantitative Reachability Properties Beyond Decisiveness
Logic in Computer ScienceFormal Languages and Automata Theory
Summary
Figuring out the chance of reaching a specific state in some infinite random systems can be very hard, especially when you don't know how far to look ahead. The authors study ways to estimate these chances more precisely by introducing new tools called truncation sets and geometrically reachable sets, which help decide a sufficient horizon to approximate probabilities within a certain precision. Their approach gives a way to calculate how far you need to explore in these systems to get good numeric estimates, even before starting the computation. They also provide formulas for this horizon that only require simple calculations and apply it to various probabilistic infinite models.
What this means in practice
- •For system verification engineers: Compute explicit bounds on how far to analyze probabilistic infinite-state models to estimate reachability accurately, improving verification workflows.
- •For network protocol developers: Determine safe and efficient message loss models in probabilistic lossy channel systems using new finite horizons from arbitrary initial states.
Authors
Raphaël Faure, Alain Finkel, Lina Ye
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.