Presenter: Mingqi Yang
Author: Satoshi Kura (Waseda University); Hiroshi Unno (Tohoku University); Takeshi Tsukada (Chiba University)
Abstract: Verifying lower bounds for quantitative properties of probabilistic programs is notoriously difficult. We propose a unified approach based on fixed-point uniqueness. By extending ranking supermartingales, we prove that the existence of such supermartingales ensures the coincidence of least and greatest fixed points, allowing lower bounds to be established via simple inductive assertions. This method uniformly handles termination probability, expected runtime, higher moments, and even non-terminating programs. We also developed an automated template-based verifier, which successfully derives precise lower bounds for various benchmarks.