Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification
This work provides a novel theoretical framework for lower-bound verification in probabilistic programs, addressing a known bottleneck in automated reasoning about quantitative properties.
The paper presents a unified approach to verifying lower bounds of quantitative properties in probabilistic programs by generalizing ranking supermartingales to witness the uniqueness of fixed points. The method is applied to termination probability, expected runtime, and other properties, with experimental validation showing its effectiveness.
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.