Reasoning about Recursive Probabilistic Programs

被引：52

作者：

Olmedo, Federico ^{[1
]}

Kaminski, Benjamin Lucien ^{[1
]}

Katoen, Joost-Pieter ^{[1
]}

Matheja, Christoph ^{[1
]}

机构：

[1] Rhein Westfal TH Aachen, Aachen, Germany

来源：

PROCEEDINGS OF THE 31ST ANNUAL ACM-IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2016) | 2016年

关键词：

recursion; probabilisitic programming; program verification; weakest pre-condition calculus; expected runtime; SEMANTICS; CALCULUS;

D O I：

10.1145/2933575.2935317

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

This paper presents a wp-style calculus for obtaining expectations on the outcomes of (mutually) recursive probabilistic programs. We provide several proof rules to derive one- and two-sided bounds for such expectations, and show the soundness of our wp-calculus with respect to a probabilistic pushdown automaton semantics. We also give a wp-style calculus for obtaining bounds on the expected runtime of recursive programs that can be used to determine the (possibly infinite) time until termination of such programs.

引用

页码：672 / 681

页数：10

共 50 条

[21] Reasoning algebraically about probabilistic loops
Meinicke, Larissa
Hayes, Ian J.
FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2006, 4260 : 380 - +
[22] Reasoning about Actions in a Probabilistic Setting
Baral, C
Tran, N
Tuan, LC
EIGHTEENTH NATIONAL CONFERENCE ON ARTIFICIAL INTELLIGENCE (AAAI-02)/FOURTEENTH INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE (IAAI-02), PROCEEDINGS, 2002, : 507 - 512
[23] Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
Aguirre, Alejandro
Haselwarter, Philipp G.
de Medeiros, Markus
Li, Kwing Hei
Gregersen, Simon Oddershede
Tassarotti, Joseph
Birkedal, Lars
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2024, 8 (ICFP):
[24] Model Checking Temporal Properties of Recursive Probabilistic Programs
Winkler, Tobias
Gehnen, Christina
Katoen, Joost-Pieter
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FOSSACS 2022), 2022, 13242 : 449 - 469
[25] MODEL CHECKING TEMPORAL PROPERTIES OF RECURSIVE PROBABILISTIC PROGRAMS
Winkler, Tobias
Gehnen, Christina
Katoen, Joost-Pieter
LOGICAL METHODS IN COMPUTER SCIENCE, 2023, 19 (04)
[26] Reasoning about incompletely defined programs
Walther, C
Schweitzer, S
LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2005, 3835 : 427 - 442
[27] Reasoning about faulty quantum programs
Paolo Zuliani
Acta Informatica, 2009, 46 : 403 - 432
[28] Reasoning About Imperative Quantum Programs
Chadha, R.
Mateus, P.
Sernadas, A.
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 158 : 19 - 39
[29] It is declarative - On reasoning about logic programs
Drabent, W
LOGIC PROGRAMMING: PROCEEDINGS OF THE 1999 INTERNATIONAL CONFERENCE ON LOGIC PROGRAMMING, 1999, : 607 - 607
[30] Reasoning about faulty quantum programs
Zuliani, Paolo
ACTA INFORMATICA, 2009, 46 (06) : 403 - 432

← 1 2 3 4 5 →