发表机构
Université Paris-Saclay; CNRS; ENS Paris-Saclay; CentraleSupélec（巴黎萨克雷大学; 法国国家科学研究中心; 巴黎萨克雷高等师范学院; ）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出概率良构转移系统（pWSTS）框架，统一解决无限状态概率系统的定量覆盖性问题，并证明随机单调pWSTS具有决定性，进而为多类型Galton-Watson过程提供可计算的近似覆盖性算法。
AI 中文摘要
良构转移系统（WSTS）为无限状态系统的验证提供了经典框架，但其概率扩展缺乏对定量覆盖性的统一处理：路径枚举算法假设分支度有限，而替代的近似方案则将某些计算（如有界范围内的概率）推迟到具体模型中处理。我们引入了概率良构转移系统（pWSTS），即底层转移系统为WSTS的可数状态集上的马尔可夫链，且不预先假设分支度。该类涵盖了任何配备马尔可夫核的WSTS，例如概率向量加法系统（pVAS）和概率有损信道系统（pLCS）。对于有效的子类，我们解决了有界范围内的近似定量覆盖性问题，并在决定性条件下解决了无限范围内的该问题，所需概率信息仅包括单个转移概率。随后，我们识别出决定性的一般来源：每个随机单调的pWSTS相对于每个向上闭集合都是决定性的。最后，我们将该框架应用于多类型Galton--Watson过程，这是一种经典的种群动态模型，其后代分布可能具有无限支撑。在对繁殖规律的温和假设下，这些过程是有效的pWSTS，并且是随机单调的，因此是决定性的。因此，对于这些过程，近似定量覆盖性在两个范围内都是可计算的，其证明不使用任何传统工具：既不用生成函数，也不对情形进行区分。
英文摘要
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.
Comments25 pages
