Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs

被引:15
|
作者
Chatterjee, Krishnendu [1 ]
Goharshady, Amir Kafshdar [2 ]
Meggendorfer, Tobias [1 ]
Zikelic, Dorde [1 ]
机构
[1] Inst Sci & Technol Austria ISTA, Klosterneuburg, Austria
[2] Hong Kong Univ Sci & Technol HKUST, Hong Kong, Peoples R China
来源
COMPUTER AIDED VERIFICATION (CAV 2022), PT I | 2022年 / 13371卷
关键词
LINEAR-INVARIANT GENERATION;
D O I
10.1007/978-3-031-13185-1_4
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
We consider the quantitative problem of obtaining lower-bounds on the probability of termination of a given non-deterministic probabilistic program. Specifically, given a non-termination threshold p is an element of [0, 1], we aim for certificates proving that the program terminates with probability at least 1-p. The basic idea of our approach is to find a terminating stochastic invariant, i.e. a subset SI of program states such that (i) the probability of the program ever leaving SI is no more than p, and (ii) almost-surely, the program either leaves SI or terminates. While stochastic invariants are already well-known, we provide the first proof that the idea above is not only sound, but also complete for quantitative termination analysis. We then introduce a novel sound and complete characterization of stochastic invariants that enables template-based approaches for easy synthesis of quantitative termination certificates, especially in affine or polynomial forms. Finally, by combining this idea with the existing martingale-based methods that are relatively complete for qualitative termination analysis, we obtain the first automated, sound, and relatively complete algorithm for quantitative termination analysis. Notably, our completeness guarantees for quantitative termination analysis are as strong as the best-known methods for the qualitative variant. Our prototype implementation demonstrates the effectiveness of our approach on various probabilistic programs. We also demonstrate that our algorithm certifies lower bounds on termination probability for probabilistic programs that are beyond the reach of previous methods.
引用
收藏
页码:55 / 78
页数:24
相关论文
共 50 条
  • [21] Modular Verification for Almost-Sure Termination of Probabilistic Programs
    Huang, Mingzhang
    Fu, Hongfei
    Chatterjee, Krishnendu
    Goharshady, Amir Kafshdar
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2019, 3 (OOPSLA):
  • [22] Quantitative Bounds on Resource Usage of Probabilistic Programs
    Chatterjee, Krishnendu
    Goharshady, Amir Kafshdar
    Meggendorfer, Tobias
    Zikelic, Dorde
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2024, 8 (OOPSLA):
  • [23] Sound and Complete Axiomatization of Trace Semantics for Probabilistic Systems
    Silva, Alexandra
    Sokolova, Ana
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2011, 276 : 291 - 311
  • [24] Agent independent probabilistic robustness certificates for robust optimization programs with uncertain quadratic cost
    Pantazis, George
    Fele, Filiberto
    Margellos, Kostas
    2020 59TH IEEE CONFERENCE ON DECISION AND CONTROL (CDC), 2020, : 554 - 559
  • [25] Termination Analysis of linear Loop Programs
    Yu, Wei
    Zhao, Xiaoyan
    ICICTA: 2009 SECOND INTERNATIONAL CONFERENCE ON INTELLIGENT COMPUTATION TECHNOLOGY AND AUTOMATION, VOL IV, PROCEEDINGS, 2009, : 677 - +
  • [26] Termination Analysis of Linear Programs with Conditionals
    Bi, Zhongqin
    Shan, Meijing
    2008 INTERNATIONAL CONFERENCE ON ADVANCED COMPUTER THEORY AND ENGINEERING, 2008, : 450 - 456
  • [27] Automatic termination analysis of logic programs
    Lindenstrauss, N
    Sagiv, Y
    LOGIC PROGRAMMING: PROCEEDINGS OF THE FOURTEENTH INTERNATIONAL CONFERENCE ON LOGIC PROGRAMMING, 1997, : 63 - 77
  • [28] Termination Analysis by Learning Terminating Programs
    Heizmann, Matthias
    Hoenicke, Jochen
    Podelski, Andreas
    COMPUTER AIDED VERIFICATION, CAV 2014, 2014, 8559 : 797 - 813
  • [29] A PROBABILISTIC ANALYSIS OF LOOP PROGRAMS
    SZABO, ME
    FARKAS, EJ
    COMPUTER LANGUAGES, 1989, 14 (02): : 125 - 136
  • [30] Incremental Analysis for Probabilistic Programs
    Zhang, Jieyuan
    Sui, Yulei
    Xue, Jingling
    STATIC ANALYSIS (SAS 2017), 2017, 10422 : 450 - 472