Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918453469773824 |
|---|---|
| author | Kura, Satoshi Unno, Hiroshi Tsukada, Takeshi |
| author_facet | Kura, Satoshi Unno, Hiroshi Tsukada, Takeshi |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_04132 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification Kura, Satoshi Unno, Hiroshi Tsukada, Takeshi Logic in Computer Science 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. |
| title | Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2504.04132 |