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 条

[31] Geometric Semantic Genetic Programming for Recursive Boolean Programs
Moraglio, Alberto
Krawiec, Krzysztof
PROCEEDINGS OF THE 2017 GENETIC AND EVOLUTIONARY COMPUTATION CONFERENCE (GECCO'17), 2017, : 993 - 1000
[32] Modular Reasoning for Message-Passing Programs
Lei, Jinjiang
Qiu, Zongyan
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2014, 8687 : 277 - 294
[33] SMT-based model checking for recursive programs
Anvesh Komuravelli
Arie Gurfinkel
Sagar Chaki
Formal Methods in System Design, 2016, 48 : 175 - 205
[34] Fixpoint semantics and optimization of recursive Datalog programs with aggregates
Zaniolo, Carlo
Yang, Mohan
Das, Ariyam
Shkapsky, Alexander
Condie, Tyson
Interlandi, Matteo
THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2017, 17 (5-6) : 1048 - 1065
[35] Inductive synthesis of recursive logic programs: achievements and prospects
Flener, P
Yilmaz, S
JOURNAL OF LOGIC PROGRAMMING, 1999, 41 (2-3): : 141 - 195
[36] SMT-based model checking for recursive programs
Komuravelli, Anvesh
Gurfinkel, Arie
Chaki, Sagar
FORMAL METHODS IN SYSTEM DESIGN, 2016, 48 (03) : 175 - 205
[37] Plingo: A System for Probabilistic Reasoning in Answer Set Programming
Hahn, Susana
Janhunen, Tomi
Kaminski, Roland
Romero, Javier
Ruhling, Nicolas
Schaub, Torsten
THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2024,
[38] Reasoning about Monotonicity in Separation Logic
Timany, Amin
Birkedal, Lars
CPP '21: PROCEEDINGS OF THE 10TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, 2021, : 91 - 104
[39] Reasoning about preferences in argumentation frameworks
Modgil, Sanjay
ARTIFICIAL INTELLIGENCE, 2009, 173 (9-10) : 901 - 934
[40] Semantic Reasoning about the Sea of Nodes
Demange, Delphine
de Retana, Yon Fernandez
Pichardie, David
CC'18: PROCEEDINGS OF THE 27TH INTERNATIONAL CONFERENCE ON COMPILER CONSTRUCTION, 2018, : 163 - 173

← 1 2 3 4 5 →