A Hierarchy of Supermartingales for $ω$-Regular Verification
Satoshi Kura, Hiroshi Unno
TL;DR
The paper tackles the challenge of certifying almost-sure satisfaction of ω-regular properties in Markov chains by introducing a hierarchy of supermartingale-based certificates. It extends Streett-based approaches with Generalised Streett Supermartingales (GSSMs), Distribution-valued Streett SSMs (DVSSMs), and parity-oriented Progress-Measure SSMs (PMSMs), including lexicographic extensions (LexGSSMs, LexPMSMs) to enhance automation. The authors prove completeness results (GSSMs for positive recurrence, DVSSMs for null recurrence) and establish equivalences and translations between extended forms, culminating in a sound and relatively complete algorithm for LexPMSM synthesis and a prototype tool with favorable experimental results. This work significantly broadens the class of ω-regular verification problems that can be certified automatically, offering practical techniques beyond the traditional Streett supermartingales. The approach provides a structured framework for automated verification of infinite-state probabilistic programs and lays the groundwork for future extensions to MDPs and stochastic games.
Abstract
We propose new supermartingale-based certificates for verifying almost sure satisfaction of $ω$-regular properties: (1) generalised Streett supermartingales (GSSMs) and their lexicographic extension (LexGSSMs), (2) distribution-valued Streett supermartingales (DVSSMs), and (3) progress-measure supermartingales (PMSMs) and their lexicographic extension (LexPMSMs). GSSMs, LexGSSMs, and DVSSMs are derived from least-fixed point characterisations of positive recurrence and null recurrence of Markov chains with respect to given Streett conditions; and PMSMs and LexPMSMs are probabilistic extensions of parity progress measures. We study the hierarchy among these certificates and existing certificates, namely Streett supermartingales, by comparing the classes of problems that can be verified by each type of certificates. Notably, we show that our certificates are strictly more powerful than Streett supermartingales. We also prove completeness of GSSMs for positive recurrence and of DVSSMs for null recurrence: DVSSMs are, in theory, the most powerful certificates in the sense that for any Markov chain that almost surely satisfies a given $ω$-regular property, there exists a DVSSM certifying it. We provide a sound and relatively complete algorithm for synthesising LexPMSMs, the second most powerful certificates in the hierarchy. We have implemented a prototype tool based on this algorithm, and our experiments show that our tool can successfully synthesise certificates for various examples including those that cannot be certified by existing supermartingales.