用于Ω正则验证的弱非负上鞅
Weakly Non-Negative Supermartingales for Omega-Regular Verification
AI总结：
研究概率程序验证中基于鞅方法的弱非负性应用，引入惰性斯特雷特上鞅及其扩展，可在多种采样分布下用多项式模板验证Ω正则属性，扩展了相关验证范围，实验显示验证成功率显著提升。
AI中文摘要：
基于鞅的方法是概率程序验证的核心，但严格的全局非负性要求会将简单证书排除在易处理的模板类之外。放宽此要求会扩大自动合成的搜索空间，但简单的放宽在概率设置中是不合理的。我们引入了惰性斯特雷特上鞅及其字典序扩展，表明在包括所有有界支持分布在内的广泛采样分布下，弱非负性仍可合理地用于用多项式模板验证几乎必然满足Ω正则属性。这将先前的弱非负方法从终止扩展到一般的Ω正则验证。我们还根据一维证书对字典序证书进行了组合说明。在170个多项式概率程序基准上的实验表明，与强非负基线相比，验证成功率提高了20.0 - 23.5个百分点。
英文摘要：
Martingale-based methods are central to probabilistic program verification, but strong global non-negativity requirements can exclude simple certificates from tractable template classes. Relaxing this requirement enlarges the search space for automated synthesis, but naive relaxations are unsound in the probabilistic setting. We introduce lazy Streett supermartingales and their lexicographic extension, showing that weak non-negativity can nevertheless be used soundly to certify almost-sure satisfaction of $ω$-regular properties with polynomial templates under a broad class of sampling distributions, including all bounded-support distributions. This extends prior weakly non-negative methods from termination to general $ω$-regular verification. We further give a compositional account of lexicographic certificates in terms of one-dimensional ones. Experiments on 170 polynomial probabilistic-program benchmarks show increases of 20.0-23.5 percentage points in verification success over the strongly non-negative baseline.
