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 条

[1]

Abraham Erika, 2014, Formal Methods for Executable Software Models. 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2014. Advanced Lectures: LNCS 8483, P65, DOI 10.1007/978-3-319-07317-0_3

[2]

Aguirre A., 2021, P ACM PROGRAMMING LA, P1

[3] FAST RANDOMIZED CONSENSUS USING SHARED MEMORY [J].

ASPNES, J ;

HERLIHY, M .

JOURNAL OF ALGORITHMS, 1990, 11 (03) :441-461

[4] Proofs of randomized algorithms in COQ [J].

Audebaud, Philippe ;

Paulin-Mohring, Christine .

SCIENCE OF COMPUTER PROGRAMMING, 2009, 74 (08) :568-589

[5]

Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1

[6] Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes [J].

Baier, Christel ;

Klein, Joachim ;

Leuschner, Linda ;

Parker, David ;

Wunderlich, Sascha .

COMPUTER AIDED VERIFICATION, CAV 2017, PT I, 2017, 10426 :160-180

[7] Fixpoint Theory - Upside Down [J].

Baldan, Paolo ;

Eggert, Richard ;

Koenig, Barbara ;

Padoan, Tommaso .

FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, FOSSACS 2021, 2021, 12650 :62-81

[8] Data-Driven Invariant Learning for Probabilistic Programs [J].

Bao, Jialu ;

Trivedi, Nitesh ;

Pathak, Drashti ;

Hsu, Justin ;

Roy, Subhajit .

COMPUTER AIDED VERIFICATION (CAV 2022), PT I, 2022, 13371 :33-54

[9]

Barthe Gilles, 2012, Mathematics of Program Construction. Proceedings 11th International Conference, MPC 2012, P1, DOI 10.1007/978-3-642-31113-0_1

[10]

Barthe G., 2020, FDN PROBABILISTIC PR

← 1 2 3 4 5 6 7 8 9 10 →