pith. sign in

arxiv: 2512.00270 · v2 · submitted 2025-11-29 · 💻 cs.LO

A Hierarchy of Supermartingales for ω-Regular Verification

Satoshi Kura , Hiroshi Unno This is my paper

Pith reviewed 2026-05-17 04:02 UTC · model grok-4.3

classification 💻 cs.LO
keywords supermartingalesomega-regular propertiesMarkov chainsalmost sure satisfactionrecurrenceStreett conditionsprobabilistic verification
0
0 comments X

The pith

Distribution-valued Streett supermartingales can certify the almost-sure satisfaction of any ω-regular property for Markov chains that meet it.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a hierarchy of supermartingale certificates for checking whether Markov chains satisfy ω-regular properties almost surely. It derives generalised Streett supermartingales and distribution-valued ones from fixed-point views of recurrence under Streett conditions, and shows they are strictly stronger than prior Streett supermartingales. The authors prove that generalised versions are complete for positive recurrence and distribution-valued ones for null recurrence, making the latter theoretically the strongest certificates available.

Core claim

We introduce distribution-valued Streett supermartingales (DVSSMs) and prove that they are complete: for any Markov chain that almost surely satisfies a given ω-regular property, there exists a DVSSM that certifies it. We also establish that generalised Streett supermartingales (GSSMs) are complete for the positive recurrence case, and we present a hierarchy showing these new certificates are more powerful than existing Streett supermartingales.

What carries the argument

Distribution-valued Streett supermartingales (DVSSMs), which use distributions over rational numbers assigned to states to witness null recurrence with respect to a Streett condition.

Load-bearing premise

The least-fixed-point characterisations of positive and null recurrence with respect to Streett conditions correctly capture the almost-sure satisfaction semantics for the given ω-regular properties.

What would settle it

A concrete Markov chain and ω-regular property that the chain satisfies almost surely, yet no distribution-valued Streett supermartingale exists for it.

Figures

Figures reproduced from arXiv: 2512.00270 by Hiroshi Unno, Satoshi Kura.

Figure 1
Figure 1. Figure 1: The hierarchy of supermartingale certificates for almost sure satisfaction of [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Algorithm for synthesizing a LexPMSM map. [PITH_FULL_IMAGE:figures/full_fig_p017_2.png] view at source ↗
read the original abstract

We propose new supermartingale-based certificates for verifying almost sure satisfaction of $\omega$-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 $\omega$-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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper proposes generalised Streett supermartingales (GSSMs), distribution-valued Streett supermartingales (DVSSMs), progress-measure supermartingales (PMSMs) and their lexicographic extensions as certificates for almost-sure satisfaction of ω-regular properties on Markov chains. These are derived from least-fixed-point characterisations of positive and null recurrence with respect to Streett conditions (for GSSMs/DVSSMs) or as probabilistic extensions of parity progress measures (for PMSMs). The authors establish a strict hierarchy showing these certificates are more powerful than standard Streett supermartingales, prove completeness of GSSMs for positive recurrence and of DVSSMs for null recurrence (asserting DVSSMs are the most powerful), give a sound and relatively complete synthesis algorithm for LexPMSMs, and report a prototype implementation whose experiments succeed on examples beyond the reach of prior supermartingales.

Significance. If the completeness results hold, the work provides a theoretically grounded and practically useful extension of supermartingale techniques to full ω-regular verification, with a clear hierarchy and the first relatively complete synthesis procedure for a near-maximal class of certificates. Credit is given for the explicit derivation of the new certificates from recurrence operators, the relatively complete algorithm for LexPMSMs, and the experimental demonstration that the prototype handles instances not certifiable by existing methods.

major comments (1)
  1. [§4] §4 (completeness theorems for GSSMs and DVSSMs): the central completeness claims rest on the least-fixed-point characterisations of positive and null recurrence w.r.t. a Streett condition coinciding exactly with the sets of states satisfying the ω-regular property almost surely. The manuscript must supply an explicit argument (or reference to a prior result) showing that the operators are monotone, that their fixed points are neither over- nor under-approximations, and that this equivalence is preserved under the distribution-valued lifting; without it the assertion that DVSSMs are the most powerful certificates is not yet load-bearing.
minor comments (2)
  1. [§3.1] Clarify the precise relationship between the lexicographic order on LexGSSMs and the underlying Streett condition in the definition of the ranking function.
  2. [§6] The experimental section would benefit from a table listing the number of states, the specific ω-regular property, and the size of the synthesised certificate for each benchmark.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful and constructive review. We address the single major comment below and will incorporate the requested clarifications in the revised manuscript.

read point-by-point responses

  1. Referee: [§4] §4 (completeness theorems for GSSMs and DVSSMs): the central completeness claims rest on the least-fixed-point characterisations of positive and null recurrence w.r.t. a Streett condition coinciding exactly with the sets of states satisfying the ω-regular property almost surely. The manuscript must supply an explicit argument (or reference to a prior result) showing that the operators are monotone, that their fixed points are neither over- nor under-approximations, and that this equivalence is preserved under the distribution-valued lifting; without it the assertion that DVSSMs are the most powerful certificates is not yet load-bearing.

    Authors: We agree that the completeness claims for GSSMs and DVSSMs depend on the least-fixed-point operators for positive and null recurrence coinciding exactly with the almost-sure satisfaction sets. The current manuscript derives the certificates from these characterisations and states the completeness results, but we acknowledge that the monotonicity, exactness, and preservation under distribution-valued lifting are not spelled out in full detail. In the revision we will add a dedicated subsection (or lemmas) in §4 that supplies the missing arguments: (i) monotonicity follows directly from the inductive definition of the recurrence operators over the Streett pairs, as enlarging the candidate set cannot decrease the infimum probability of satisfying the recurrence condition; (ii) the least fixed point is shown to be exact (neither over- nor under-approximation) by proving it equals the greatest lower bound of all sets from which the ω-regular property holds with probability 1, using the standard probabilistic semantics of Streett automata on Markov chains; (iii) the distribution-valued lifting preserves the equivalence because the expectation operator commutes with the fixed-point construction while maintaining the almost-sure guarantees. We will either include a self-contained proof or cite the relevant fixed-point results from the literature on recurrence in Markov decision processes. This addition will make the claim that DVSSMs are the most powerful certificates fully rigorous. revision: yes

Circularity Check

0 steps flagged

No circularity: certificates derived from external LFP characterizations of Streett recurrence

full rationale

The paper defines GSSMs, LexGSSMs and DVSSMs directly from least-fixed-point operators for positive and null recurrence w.r.t. given Streett conditions; completeness statements then follow from the (assumed or prior) fact that those fixed points coincide with the almost-sure satisfaction sets. No equation or definition inside the paper reduces the target certificate or the completeness claim back to itself by construction, no parameters are fitted to the verification outcome, and no load-bearing self-citation chain is required for the central theorems. The derivation therefore remains self-contained against the external LFP semantics.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work rests on standard definitions from probability theory and automata theory; no new free parameters, ad-hoc axioms, or invented physical entities are introduced.

axioms (1)
  • domain assumption Least-fixed-point characterisations of positive and null recurrence for Markov chains with respect to Streett conditions correctly encode almost-sure satisfaction of the corresponding omega-regular properties.
    Invoked to derive the new supermartingales and prove completeness.

pith-pipeline@v0.9.0 · 5587 in / 1291 out tokens · 37694 ms · 2026-05-17T04:02:22.091217+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Zero-Knowledge Model Checking

    cs.CR 2026-05 unverdicted novelty 7.0

    Zero-knowledge protocols for model checking that certify linear temporal logic properties of hidden systems using ranking functions, polynomial commitments, and sigma protocols.

Reference graph

Works this paper leans on

11 extracted references · 11 canonical work pages · cited by 1 Pith paper

  1. [1]

    2018), 1–32

    Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs.Proceedings of the ACM on Programming Languages2, POPL (Jan. 2018), 1–32. Christel Baier and Joost-Pieter Katoen. 2008.Principles of Model Checking. MIT Press, Cambridge, Mass. Aleksandar Chakarov and Sriram Sankaranarayanan

    work page 2018

  2. [2]

    Krishnendu Chatterjee, Petr Novotný, and Ðorđe Žikelić

    On Lexicographic Proof Rules for Probabilistic Termination.Formal Aspects of Computing35, 2 (June 2023), 1–25. Krishnendu Chatterjee, Petr Novotný, and Ðorđe Žikelić

    work page 2023

  3. [3]

    (Leibniz International Proceedings in Informatics (Lipics), Vol. 72). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 7:1–7:18. Erich Grädel, Wolfgang Thomas, and Thomas Wilke. 2002.Automata Logics, and Infinite Games: A Guide to Current Research. Lecture Notes in Computer Science, Vol

    work page 2002

  4. [4]

    2019), 1–29

    Modular Verification for Almost-Sure Termination of Probabilistic Programs.Proceedings of the ACM on Programming Languages3, OOPSLA (Oct. 2019), 1–29. Marcin Jurdziński

    work page 2019

  5. [5]

    InSTACS 2000 (Lecture Notes in Computer Science, Vol

    Small Progress Measures for Solving Parity Games. InSTACS 2000 (Lecture Notes in Computer Science, Vol. 1770). Springer Berlin Heidelberg, Berlin, Heidelberg, 290–301. Andrew Kenyon-Roberts and C.-H. Luke Ong

    work page 2000

  6. [6]

    Results on the Quantitative𝜇-Calculus qM𝜇.ACM Transactions on Computational Logic8, 1 (Jan. 2007),

    work page 2007

  7. [7]

    2018), 1–28

    A New Proof Rule for Almost-Sure Termination.Proceedings of the ACM on Programming Languages2, POPL (Jan. 2018), 1–28. Toru Takisaka, Yuichiro Oyabu, Natsuki Urabe, and Ichiro Hasuo

    work page 2018

  8. [8]

    Ranking and Repulsing Supermartingales for Reachability in Randomized Programs.ACM Transactions on Programming Languages and Systems43, 2 (June 2021), 1–46. , Vol. 1, No. 1, Article . Publication date: December

    work page 2021

  9. [9]

    ,(X𝑟 𝑝(𝑥) ) (𝑥)), and lev(𝑥) is a level

    (𝑥), . . . ,(X𝑟 𝑝(𝑥) ) (𝑥)), and lev(𝑥) is a level. That is, for any 𝑖 such that1 ≤𝑖<lev(𝑥) , 𝑟𝑖 (𝑥) ≥ (X𝑟 𝑖 ) (𝑥), and if 𝑖=lev(𝑥), then𝑟 𝑖 (𝑥) ≥1+ (X𝑟 𝑖 ) (𝑥). The functionlevis defined as follows. •If𝑝(𝑥)=𝑖∉𝐼, then we have 𝑝 −1 ({𝑖}) ⊆ Ø 1≤𝑙≤𝑖 𝑅𝑙 where𝑅 𝑙 := Ù 1≤𝑗<𝑙 {𝑥|𝑟 𝑗 (𝑥) ≥ (X𝑟 𝑗 ) (𝑥)} ∩ {𝑥|𝑟 𝑙 (𝑥) ≥1+ (X𝑟 𝑙 ) (𝑥)}. Since 𝑝 −1 ({𝑖}) and each 𝑅𝑙 a...

    work page 2018

  10. [10]

    A Hierarchy of Supermartingales for𝜔-Regular Verification 29 •By definition of a parity progress measure, we have𝑟 𝑙 (𝑥𝑛′ ) ∈ [0,∞)= Ð 𝐵∈N [0, 𝐵]. {𝑥∈𝑆 𝜔 |minInf lev(𝑥)=𝑙∧ ∀𝑚≥𝑛 ′, 𝑝(𝑥 𝑚) ≥𝑘∧lev(𝑥 𝑚) ≥𝑙} = Ø 𝐵∈N {𝑥∈𝑆 𝜔 |minInf lev(𝑥)=𝑙∧ ∀𝑚≥𝑛 ′, 𝑝(𝑥 𝑚) ≥𝑘∧lev(𝑥 𝑚) ≥𝑙∧𝑟 𝑙 (𝑥𝑛′ ) ≤𝐵} There exists𝐵∈Nsuch that𝑟 𝑙 (𝑥𝑛′ )is at most𝐵with positive probability. P𝑥0 ...

    work page 2018

  11. [11]

    𝑙0 ↦→ 𝑙0 𝑙0,2 𝑙0,3 [𝑥=0] [𝑥>0] As for the Streett pair (𝐴, 𝐵)=({(𝑙 0, 𝑥) | ⌊𝑥⌋ ≥ 2},{(𝑙 0, 𝑥) | ⌊𝑥⌋= 1} ∪ {(𝑙 1, 𝑥) |𝑥∈R}) , we obtain the following equation system

    according to the priority partition. 𝑙0 ↦→ 𝑙0 𝑙0,2 𝑙0,3 [𝑥=0] [𝑥>0] As for the Streett pair (𝐴, 𝐵)=({(𝑙 0, 𝑥) | ⌊𝑥⌋ ≥ 2},{(𝑙 0, 𝑥) | ⌊𝑥⌋= 1} ∪ {(𝑙 1, 𝑥) |𝑥∈R}) , we obtain the following equation system. 𝑋𝑙0,2 (𝑥)= 𝜈 if𝑥≥1then𝑋 𝑙0 (𝑥−1)else𝑋 𝑙1 (2) 𝑋𝑙1,2 (𝑥)= 𝜈 1 2𝑋𝑙1 (2𝑥) + 1 2𝑋𝑙0 (𝑥) 𝑋𝑙0,3 (𝑥)= 𝜇 if𝑥≥1then𝑋 𝑙0 (𝑥−1)else𝑋 𝑙1 (2) 𝑋𝑙0,4 (𝑥)= 𝜇 if𝑥≥1then𝑋 𝑙0...

    work page 2025