Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Satoshi Kura, Hiroshi Unno, Takeshi Tsukada

TL;DR

The paper introduces a unified, fixed-point-based framework for lower-bound verification of probabilistic program properties by leveraging a generalized ranking supermartingale to enforce uniqueness of fixed points within an upper bound. This U-ranking approach applies across diverse transformers, including weakest preexpectation, expected runtime, higher moments, and conditional variants, and even supports non-terminating or unbounded settings. A template-driven automation pipeline (MuVal) reduces the problem to polynomial quantified entailments solvable by dedicated solvers, enabling exact lower bounds in many benchmarks and extending prior methods. The work also provides formal correctness results, a discussion of completeness in bounded settings via gamma-scaling, and practical experimental results, highlighting both strengths and limitations. Overall, the approach offers a principled, broadly applicable mechanism for lower-bound verification in probabilistic programs with a unifying theoretical and automated toolkit.

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.

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

TL;DR

The paper introduces a unified, fixed-point-based framework for lower-bound verification of probabilistic program properties by leveraging a generalized ranking supermartingale to enforce uniqueness of fixed points within an upper bound. This U-ranking approach applies across diverse transformers, including weakest preexpectation, expected runtime, higher moments, and conditional variants, and even supports non-terminating or unbounded settings. A template-driven automation pipeline (MuVal) reduces the problem to polynomial quantified entailments solvable by dedicated solvers, enabling exact lower bounds in many benchmarks and extending prior methods. The work also provides formal correctness results, a discussion of completeness in bounded settings via gamma-scaling, and practical experimental results, highlighting both strengths and limitations. Overall, the approach offers a principled, broadly applicable mechanism for lower-bound verification in probabilistic programs with a unifying theoretical and automated toolkit.

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.

Paper Structure

This paper contains 47 sections, 18 theorems, 95 equations, 5 tables.

Table of Contents

  1. Introduction
  2. Our Approach
  3. Ranking Supermartingales for Unique Fixed Points
  4. Implementation
  5. Contributions.
  6. Outline.
  7. Program Analysis via Fixed-Point Equations
  8. Preliminaries on Fixed Points
  9. Fixed-Point Equation System
  10. Semantics.
  11. A Probabilistic Programming Language and its Verification via Equation System
  12. Weakest Precondition Transformer
  13. Expected Cost Analysis
  14. Cost Moment Analysis
  15. Soft/Hard Conditioning
  16. ...and 32 more sections

Key Result

theorem 2

If $(X, {\le})$ is an $\omega$cpo with a bottom element $\bot$ and $K : X \to X$ is a Scott continuous function, then $K$ has the least fixed point given by $\mu K = \sup_n K^n(\bot)$. Here $K^n$ is defined by $K^0(x) = x$ and $K^{n+1}(x) = K(K^n(x))$. ∎

Theorems & Definitions (30)

  • theorem 2: Kleene's fixed-point theorem
  • Remark 3
  • theorem 4: Knaster--Tarski theorem
  • definition 1
  • Remark 5
  • definition 2
  • Remark 6
  • lemma 1
  • corollary 1
  • definition 3: Affineness
  • ...and 20 more