发表机构
Aalto University; TU Wien; Nanyang Technological University（阿尔托大学; 维也纳工业大学; 南洋理工大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究基于鞅理论，提出可处理方法验证概率转移系统（PTS）的多项式不变量，通过可选停定理（OST）的前提条件dui，可综合允许无界支撑采样分布的多项式循环不变量。
AI 中文摘要
我们基于鞅理论研究概率转移系统（PTS）的多项式不变量的综合问题。我们提出了可处理的方法来验证这些多项式确实是不变量，其含义是它们终止时的期望值与计算开始时的值相同。我们通过将可选停定理（OST）应用于特定前提条件来实现这一点。该前提条件要求鞅表达式存在一个可积的支配函数，这意味着一致可积性；我们将此条件称为dui。对于线性概率转移系统，我们将dui属性简化为证明取决于更新矩阵、鞅表达式的次数和停止时间的表达式的期望值有限。具体而言，如果所有随机样本都具有有限矩，并且我们可以验证线性循环运行时间的矩界，那么我们可以自动综合满足可选停定理的多项式循环不变量。值得注意的是，dui允许采样分布具有无界支撑，这是该领域的一项新贡献。
英文摘要
We study the synthesis of polynomial invariants for probabilistic transition systems (PTS) based on martingale theory. We present tractable methods to verify that such polynomials are indeed invariants, in the sense that their expected value upon termination is the same as their value at the start of the computation. We do this by applying the Optional Stopping Theorem (OST) in the form of a specific precondition. This precondition requires the existence of an integrable dominating function for the martingale expression, which implies uniform integrability; we refer to this condition as dui. For linear PTS we simplify the dui property to proving finiteness of the expected value of an expression depending on the update matrix, the degree of the martingale expression, and the stopping time. Specifically, if all random samples have finite moments and we can verify a moment bound on the runtime of a linear loop, then we can automatically synthesise polynomial loop invariants that satisfy the OST. Notably, dui allows for the sampled distributions to have unbounded support, which is a novel contribution to the field.
Comments16 pages + 19 pages appendix, extended version of submission accepted at LPAR'26
