Quantitative coverability for probabilistic well-structured transition systems

Abstract

Well-structured transition systems (WSTS) provide a classical framework for the verification of infinite-state systems, but their probabilistic extensions lack a unified treatment of quantitative coverability: path-enumeration algorithms assume a finite branching degree, while alternative approximation schemes defer some computations, such as probabilities over a bounded horizon, to the model at hand. We introduce probabilistic well-structured transition systems (pWSTS), Markov chains over countable state sets whose underlying transition systems are WSTS, with no a priori assumption on the branching degree. This class encompasses any WSTS equipped with a Markov kernel, such as probabilistic vector addition systems (pVAS) and probabilistic lossy channel systems (pLCS). For an effective subclass, we solve the approximate quantitative coverability problem over bounded horizons, and over infinite horizons under decisiveness, requiring no probabilistic information beyond individual transition probabilities. We then identify a general source of decisiveness: every stochastically monotone pWSTS is decisive with respect to every upward-closed set. We finally instantiate the framework on multi-type Galton--Watson processes, a classical model of population dynamics whose offspring distributions may have infinite support. Under mild assumptions on the reproduction laws, these processes are effective pWSTS, and they are stochastically monotone, hence decisive. Approximate quantitative coverability is therefore computable for them over both horizons, with a proof that uses none of the traditional tools: neither generating functions nor any case distinction between regimes.