Lower Bounds for Possibly Divergent Probabilistic Programs

被引：4
作者：
Feng, Shenghua [1 ]
Chen, Mingshuai [2 ]
Su, Han [1 ]
Kaminski, Benjamin Lucien [3 ,4 ]
Katoen, Joost-Pieter [5 ]
Zhan, Naijun [1 ]
机构：
[1] Chinese Acad Sci, Univ Chinese Acad Sci, Inst Software, SKLCS, Beijing, Peoples R China
[2] Zhejiang Univ, Hangzhou, Peoples R China
[3] Saarland Univ, Saarland Informat Campus, Saarbrucken, Germany
[4] UCL, London, England
[5] Rhein Westfal TH Aachen, Aachen, Germany
来源：
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL | 2023年 / 7卷 / OOPSLA期
基金：
国家重点研发计划;
关键词：
probabilistic programs; quantitative verification; weakest preexpectations; lower bounds; almost-sure termination; uniform integrability; INVARIANT GENERATION; MODEL CHECKING; BISIMULATION; SEMANTICS;
D O I：
10.1145/3586051
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We present a new proof rule for verifying lower bounds on quantities of probabilistic programs. Our proof rule is not confined to almost-surely terminating programs - as is the case for existing rules - and can be used to establish non-trivial lower bounds on, e.g., termination probabilities and expected values, for possibly divergent probabilistic loops, e.g., the well-known three-dimensional random walk on a lattice.
引用
收藏
页数：31
相关论文
共 102 条
[51]   The Quantitative Verification Benchmark Set [J].
Hartmanns, Arnd ;
Klauck, Michaela ;
Parker, David ;
Quatmann, Tim ;
Ruijters, Enno .
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT I, 2019, 11427 :344-350
[52]   A probability perspective [J].
Hehner, Eric C. R. .
FORMAL ASPECTS OF COMPUTING, 2011, 23 (04) :391-419
[53]  
Hicks Michael, 2014, PROGRAMMING LANGUAGE
[54]   Probabilistic Bisimulation for Parameterized Systems (with Applications to Verifying Anonymous Protocols) [J].
Hong, Chih-Duo ;
Lin, Anthony W. ;
Majumdar, Rupak ;
Rummer, Philipp .
COMPUTER AIDED VERIFICATION, CAV 2019, PT I, 2019, 11561 :455-474
[55]   The Tarski-Kantorovitch principle and the theory of iterated function systems [J].
Jachymski, J ;
Gajek, L ;
Pokarowski, P .
BULLETIN OF THE AUSTRALIAN MATHEMATICAL SOCIETY, 2000, 61 (02) :247-261
[56]   Bounded Model Checking for Probabilistic Programs [J].
Jansen, Nils ;
Dehnert, Christian ;
Kaminski, Benjamin Lucien ;
Katoen, Joost-Pieter ;
Westhofen, Lukas .
AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2016, 2016, 9938 :68-85
[57]  
Jones Claire, 1990, Probabilistic Non-Determinism
[58]  
Kaminski B.L., 2019, Advanced weakest precondition calculi for probabilistic programs
[59]   On the hardness of analyzing probabilistic programs [J].
Kaminski, Benjamin Lucien ;
Katoen, Joost-Pieter ;
Matheja, Christoph .
ACTA INFORMATICA, 2019, 56 (03) :255-285
[60]   Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms [J].
Kaminski, Benjamin Lucien ;
Katoen, Joost-Pieter ;
Matheja, Christoph ;
Olmedo, Federico .
JOURNAL OF THE ACM, 2018, 65 (05)
12345678910