Weakly Non-Negative Supermartingales for Omega-Regular Verification

Toru Takisaka, Hongjie Qing, Libo Zhang

Martingale-based methods are central to probabilistic program verification, but strong global non-negativity requirements can exclude simple certificates from tractable template cl…