Weakly Non-Negative Supermartingales for Omega-Regular Verification
2026-07-20 • Programming Languages
Programming Languages
AI summaryⓘ
The authors study a method to verify that probabilistic programs behave correctly almost all the time. Traditional methods require certain mathematical functions to always be non-negative, which can be too strict and limit the automated discovery of these functions. They introduce a relaxed approach called lazy Streett supermartingales, which allow some negativity but still ensure correctness for a wide range of cases. Their approach works for more general properties and types of randomness than before, and experiments show it improves verification success significantly compared to older strict methods.
probabilistic programsmartingalessupermartingalesω-regular propertiestermination verificationpolynomial templatessampling distributionscompositional reasoning
Authors
Toru Takisaka, Hongjie Qing, Libo Zhang
Abstract
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.