Weakly Non-Negative Supermartingales for Omega-Regular Verification

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.