pith. sign in

arxiv: 2504.04132 · v3 · submitted 2025-04-05 · 💻 cs.LO

Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification

Satoshi Kura , Hiroshi Unno , Takeshi Tsukada This is my paper

Pith reviewed 2026-05-22 21:35 UTC · model grok-4.3

classification 💻 cs.LO
keywords ranking supermartingalesfixed pointsprobabilistic programslower bound verificationtermination probabilityexpected runtimeweakest preexpectation
0
0 comments X

The pith

Generalized ranking supermartingales witness uniqueness of fixed points and certify lower bounds on quantitative properties of probabilistic programs.

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

The paper establishes that a generalization of ranking supermartingales can serve as witnesses for the uniqueness of fixed points in the semantics of probabilistic programs. This connection allows a unified approach to verifying lower bounds for several quantitative properties that are defined as least fixed points. The properties include termination probability, weakest preexpectation, expected runtime, higher moments of runtime, and conditional weakest preexpectation. The approach comes with a template-based algorithm for automated verification, shown effective in experiments.

Core claim

A generalization of ranking supermartingales serves as witnesses of the uniqueness of fixed points and thereby provides a simple and unified reasoning principle applicable to a wide range of quantitative properties, including termination probability, the weakest preexpectation, expected runtime, higher moments of runtime, and conditional weakest preexpectation.

What carries the argument

Generalized ranking supermartingales that serve as witnesses of the uniqueness of fixed points.

If this is right

  • Lower bounds on termination probability can be verified using the same generalized supermartingale principle.
  • The method directly yields lower bounds for expected runtime and its higher moments.
  • Conditional weakest preexpectation admits the same uniform verification approach.
  • A template-based synthesis algorithm automates the search for suitable supermartingales.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The technique may extend to quantitative properties outside the five explicitly listed.
  • It could reduce the need for separate proof techniques across different program analyses.
  • Practical tools might combine the templates with existing solvers for broader automation.

Load-bearing premise

The connection between uniqueness of fixed points and program termination can be exploited by generalized ranking supermartingales to certify lower bounds on the listed quantitative properties.

What would settle it

A probabilistic program and property where a generalized ranking supermartingale exists yet the claimed lower bound on expected runtime fails to hold under actual executions.

read the original abstract

Many quantitative properties of probabilistic programs can be characterized as least fixed points, but verifying their lower bounds remains a challenging problem. We present a new approach to lower-bound verification that exploits and extends the connection between the uniqueness of fixed points and program termination. The core technical tool is a generalization of ranking supermartingales, which serves as witnesses of the uniqueness of fixed points. Our method provides a simple and unified reasoning principle applicable to a wide range of quantitative properties, including termination probability, the weakest preexpectation, expected runtime, higher moments of runtime, and conditional weakest preexpectation. We provide a template-based algorithm for automated verification of lower bounds and demonstrate the effectiveness of the proposed method via experiments.

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

0 major / 2 minor

Summary. The paper claims that a generalization of ranking supermartingales serves as witnesses of the uniqueness of fixed points, thereby providing a simple and unified reasoning principle for lower-bound verification of quantitative properties of probabilistic programs. The properties covered include termination probability, weakest preexpectation, expected runtime, higher moments of runtime, and conditional weakest preexpectation. The approach is supported by a template-based algorithm for automated verification together with experimental results.

Significance. If the central claim holds, the work offers a meaningful unification by extending the standard supermartingale argument for almost-sure termination to quantitative lower bounds via uniqueness witnesses. Each construction reduces uniqueness to an expectation-decrease condition that aligns with existing supermartingale techniques. The template-based algorithm follows directly from the uniqueness witnesses, and the experimental demonstration adds practical value. The absence of free parameters or ad-hoc axioms in the core development is a strength.

minor comments (2)
  1. [§3] §3 (or the section defining the generalized supermartingale): clarify whether the decrease condition is required to hold for all states or only outside a zero set, as this affects the uniqueness argument for conditional weakest preexpectation.
  2. [Experiments] The experimental section should report the number of benchmarks on which the template synthesis succeeded versus timed out, to allow assessment of the algorithm's effectiveness beyond the abstract claim.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive evaluation, the recognition of the unification achieved by generalized ranking supermartingales, and the recommendation for minor revision. No specific major comments were raised in the report.

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained

full rationale

The paper generalizes ranking supermartingales to serve as witnesses of uniqueness of fixed points, reducing uniqueness to an expectation-decrease condition that extends the standard supermartingale argument for almost-sure termination to quantitative properties (termination probability, weakest preexpectation, expected runtime, higher moments, conditional weakest preexpectation). Each construction follows directly from this extension without self-definitional reductions, fitted inputs renamed as predictions, or load-bearing self-citations. The template-based algorithm is derived from the uniqueness witnesses. The central claim has independent content grounded in the cited connection between uniqueness and termination, which is not shown to reduce to the paper's own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review; no explicit free parameters, axioms, or invented entities are stated in the provided text.

pith-pipeline@v0.9.0 · 5648 in / 1160 out tokens · 51196 ms · 2026-05-22T21:35:12.158929+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

36 extracted references · 36 canonical work pages

  1. [1]

    Alessandro Abate, Mirco Giacobbe, and Diptarko Roy. 2025. Quantitative Supermartingale Certificates. InComputer Aided Verification. Springer Nature Switzerland, Cham, 3–28

    work page 2025

  2. [2]

    Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotný. 2018. Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs.Proceedings of the ACM on Programming Languages2, POPL (Jan. 2018), 1–32

    work page 2018

  3. [3]

    Alejandro Aguirre, Shin-ya Katsumata, and Satoshi Kura. 2022. Weakest Preconditions in Fibrations.Mathematical Structures in Computer Science32, 4 (Oct. 2022), 472–510

    work page 2022

  4. [4]

    Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja

    work page

  5. [5]

    InTools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science, Vol

    Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants. InTools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science, Vol. 13994). Springer Nature Switzerland, Cham, 410–429

    work page

  6. [6]

    Raven Beutner and Luke Ong. 2021. On Probabilistic Termination of Functional Programs with Continuous Distri- butions. InProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. ACM, Virtual Canada, 1312–1326

    work page 2021

  7. [7]

    Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In Computer Aided Verification (Lecture Notes in Computer Science, Vol. 8044). Springer Berlin Heidelberg, Saint Petersburg, Russia, 511–526

    work page 2013

  8. [8]

    Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. 2016. Termination Analysis of Probabilistic Programs Through Positivstellensatz’s. InComputer Aided Verification (Lecture Notes in Computer Science, Vol. 9779). Springer International Publishing, Cham, 3–22

    work page 2016

  9. [9]

    Krishnendu Chatterjee, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, Milad Saadat, Maximilian Seeliger, and Ðorđe Žikelić. 2026. PolyQEnt: A Polynomial Quantified Entailment Solver. InAutomated Technology for Verification and Analysis (Lecture Notes in Computer Science, Vol. 16145). Springer Nature Switzerland, Cham, 411–424

    work page 2026

  10. [10]

    Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, and Ðorđe Žikelić. 2022. Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs. InComputer Aided Verification (Lecture Notes in Computer Science, Vol. 13371). Springer International Publishing, Cham, 55–78

    work page 2022

  11. [11]

    Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2005. Abstraction Refinement for Termination. InSAS ’05 (LNCS, Vol. 3672). Springer, 87–101

    work page 2005

  12. [12]

    Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2006. Termination proofs for systems code. InPLDI ’06. ACM, 415–426

    work page 2006

  13. [13]

    Dijkstra

    Edsger W. Dijkstra. 1975. Guarded Commands, Nondeterminacy and Formal Derivation of Programs.Commun. ACM 18, 8 (Aug. 1975), 453–457

    work page 1975

  14. [14]

    Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Naijun Zhan. 2023. Lower Bounds for Possibly Divergent Probabilistic Programs.Proceedings of the ACM on Programming Languages7, OOPSLA1 (April 2023), 696–726

    work page 2023

  15. [15]

    Luis María Ferrer Fioriti and Holger Hermanns. 2015. Probabilistic Termination: Soundness, Completeness, and Compositionality. InProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL ’15. ACM Press, Mumbai, India, 489–501

    work page 2015

  16. [16]

    Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl, and Joost-Pieter Katoen. 2020. Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification.Proceedings of the ACM on Programming Languages4, POPL (Jan. 2020), 1–28

    work page 2020

  17. [17]

    Henzinger, Kaushik Mallik, Pouya Sadeghi, and Ðorđe Žikelić

    Thomas A. Henzinger, Kaushik Mallik, Pouya Sadeghi, and Ðorđe Žikelić. 2025. Supermartingale Certificates for Quantitative Omega-Regular Verification and Control. InComputer Aided Verification. Springer Nature Switzerland, Cham, 29–55

    work page 2025

  18. [18]

    Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. 2018. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms.J. ACM65, 5 (Aug. 2018), 1–68

    work page 2018

  19. [19]

    Luke Ong

    Andrew Kenyon-Roberts and C.-H. Luke Ong. 2021. Supermartingales, Ranking Functions and Probabilistic Lambda Calculus. In2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, Rome, Italy, 1–13

    work page 2021

  20. [20]

    Dexter Kozen. 1979. Semantics of probabilistic programs. In20th Annual Symposium on Foundations of Computer Science (sfcs 1979). IEEE, 101–114. doi:10.1109/sfcs.1979.38

    work page doi:10.1109/sfcs.1979.38 1979

  21. [21]

    Satoshi Kura and Hiroshi Unno. 2024. Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System.Proceedings of the ACM on Programming Languages8, ICFP, Article 269 (Aug. 2024), 30 pages

    work page 2024

  22. [22]

    Satoshi Kura, Natsuki Urabe, and Ichiro Hasuo. 2019. Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments. InTools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science, Vol. 11428). Springer, Prague, Czech Republic, 135–153. 22 Satoshi Kura, Hiroshi Unno, and Takeshi Tsukada

    work page 2019

  23. [23]

    Sathiyanarayana

    Rupak Majumdar and V.R. Sathiyanarayana. 2025. Sound and Complete Proof Rules for Probabilistic Termination. Proceedings of the ACM on Programming Languages9, POPL (Jan. 2025), 1871–1902

    work page 2025

  24. [24]

    2005.Abstraction, Refinement and Proof for Probabilistic Systems

    Annabelle McIver and Carroll Morgan. 2005.Abstraction, Refinement and Proof for Probabilistic Systems. Springer, New York

    work page 2005

  25. [25]

    Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen. 2018. A New Proof Rule for Almost-Sure Termination.Proceedings of the ACM on Programming Languages2, POPL (Jan. 2018), 1–28

    work page 2018

  26. [26]

    Federico Olmedo, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Annabelle Mciver

    work page

  27. [27]

    Conditioning in Probabilistic Programming.ACM Transactions on Programming Languages and Systems40, 1 (March 2018), 1–50

    work page 2018

  28. [28]

    Marcin Szymczak and Joost-Pieter Katoen. 2020. Weakest Preexpectation Semantics for Bayesian Inference: Con- ditioning, Continuous Distributions and Divergence. InEngineering Trustworthy Software Systems (Lecture Notes in Computer Science, Vol. 12154). Springer International Publishing, Cham, 44–121

    work page 2020

  29. [29]

    Toru Takisaka, Yuichiro Oyabu, Natsuki Urabe, and Ichiro Hasuo. 2018. Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs. InAutomated Technology for Verification and Analysis (Lecture Notes in Computer Science, Vol. 11138). Springer International Publishing, Cham, 476–493

    work page 2018

  30. [30]

    Toru Takisaka, Libo Zhang, Changjiang Wang, and Jiamou Liu. 2024. Lexicographic Ranking Supermartingales with Lazy Lower Bounds. InComputer Aided Verification (Lecture Notes in Computer Science, Vol. 14683). Springer Nature Switzerland, Cham, 420–442

    work page 2024

  31. [31]

    Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen. 2023. Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification.Proceedings of the ACM on Programming Languages7, POPL, Article 72 (Jan. 2023), 30 pages

    work page 2023

  32. [32]

    Natsuki Urabe, Masaki Hara, and Ichiro Hasuo. 2017. Categorical Liveness Checking by Corecursive Algebras. In2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, Reykjavik, Iceland, 1–12

    work page 2017

  33. [33]

    Di Wang, Jan Hoffmann, and Thomas Reps. 2021. Central Moment Analysis for Cost Accumulators in Probabilistic Programs. InProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. ACM, Virtual Canada, 559–573

    work page 2021

  34. [34]

    Jinyi Wang, Yican Sun, Hongfei Fu, Krishnendu Chatterjee, and Amir Kafshdar Goharshady. 2021. Quantitative Analysis of Assertion Violations in Probabilistic Programs. InProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. ACM, Virtual Canada, 1171–1186

    work page 2021

  35. [35]

    Peixin Wang, Hongfei Fu, Amir Kafshdar Goharshady, Krishnendu Chatterjee, Xudong Qin, and Wenjun Shi. 2019. Cost analysis of nondeterministic probabilistic programs. InProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’19). ACM, 204–220. doi:10.1145/3314221.3314581

    work page doi:10.1145/3314221.3314581 2019

  36. [36]

    Peixin Wang, Hongfei Fu, Amir Kafshdar Goharshady, Krishnendu Chatterjee, Xudong Qin, and Wenjun Shi. 2019. Cost Analysis of Nondeterministic Probabilistic Programs. InProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, Phoenix AZ USA, 204–220. Supermartingales for Unique Fixed Points: A Unified Approach ...

    work page 2019