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] RELATIONAL QUANTIFIERS AND REASONING ABOUT PROGRAMS
LEIVANT, D
JOURNAL OF SYMBOLIC LOGIC, 1987, 52 (01) : 299 - 300
[32] Characterizing and reasoning about probabilistic and non-probabilistic expectation
Halpern, Joseph Y.
Pucella, Riccardo
JOURNAL OF THE ACM, 2007, 54 (03)
[33] Probabilistic reasoning about epistemic action narratives
D'Asaro, Fabio Aurelio
Bikakis, Antonis
Dickens, Luke
Miller, Rob
ARTIFICIAL INTELLIGENCE, 2020, 287
[34] Reasoning about conjunctive probabilistic concepts in childhood
Fisk, JE
Slattery, R
CANADIAN JOURNAL OF EXPERIMENTAL PSYCHOLOGY-REVUE CANADIENNE DE PSYCHOLOGIE EXPERIMENTALE, 2005, 59 (03): : 168 - 178
[35] Reasoning about complex probabilistic concepts in childhood
Fisk, John E.
Bury, Angela S.
Holden, Rachel
SCANDINAVIAN JOURNAL OF PSYCHOLOGY, 2006, 47 (06) : 497 - 504
[36] REASONING ABOUT PROBABILISTIC BEHAVIOR IN CONCURRENT SYSTEMS
PURUSHOTHAMAN, S
SUBRAHMANYAM, PA
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1987, 13 (06) : 740 - 745
[37] Reasoning about hybrid probabilistic knowledge bases
Mu, Kedian
Lin, Zuoquan
Jin, Zhi
Lu, Ruqian
PRICAI 2006: TRENDS IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2006, 4099 : 130 - 139
[38] Probabilistic Logic for Reasoning About Actions in Time
Dautovic, Sejla
Doder, Dragan
SYMBOLIC AND QUANTITATIVE APPROACHES TO REASONING WITH UNCERTAINTY, ECSQARU 2019, 2019, 11726 : 385 - 396
[39] Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving
Ye, Kangfeng
Foster, Simon
Woodcock, Jim
RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE (RAMICS 2021), 2021, 13027 : 465 - 482
[40] Qualitative and Quantitative Reasoning in Hybrid Probabilistic Logic Programs
Saad, Emad
ISIPTA 07-PROCEEDINGS OF THE FIFTH INTERNATIONAL SYMPOSIUM ON IMPRECISE PROBABILITY:THEORIES AND APPLICATIONS, 2007, : 375 - 384

← 1 2 3 4 5 →