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 条

[41] A Framework for Reasoning About Uncertainty in Ontologies [J].

Jabbour, Said ;

Ma, Yue ;

Raddaoui, Badran .

IEEE INTELLIGENT SYSTEMS, 2022, 37 (06) :27-37

[42] Lower Bounds for Possibly Divergent Probabilistic Programs [J].

Feng, Shenghua ;

Chen, Mingshuai ;

Su, Han ;

Kaminski, Benjamin Lucien ;

Katoen, Joost-Pieter ;

Zhan, Naijun .

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2023, 7 (OOPSLA)

[43] On Probabilistic Termination of Functional Programs with Continuous Distributions [J].

Beutner, Raven ;

Ong, Luke .

PROCEEDINGS OF THE 42ND ACM SIGPLAN INTERNATIONAL CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '21), 2021, :1312-1326

[44] Learning the Parameters of Probabilistic Answer Set Programs [J].

Azzolini, Damiano ;

Bellodi, Elena ;

Riguzzi, Fabrizio .

INDUCTIVE LOGIC PROGRAMMING, ILP 2022, 2024, 13779 :1-14

[45] MAP Inference in Probabilistic Answer Set Programs [J].

Azzolini, Damiano ;

Bellodi, Elena ;

Riguzzi, Fabrizio .

AIXIA 2022 - ADVANCES IN ARTIFICIAL INTELLIGENCE, 2023, 13796 :413-426

[46] A higher-order function approach to evolve recursive programs [J].

Yu, T .

GENETIC PROGRAMMING THEORY AND PRACTICE III, 2006, 9 :93-108

[47] Programming and reasoning about actors that share state [J].

Caldwell, Sam ;

Garnock-jones, Tony ;

Felleisen, Matthias .

JOURNAL OF FUNCTIONAL PROGRAMMING, 2024, 34

[48] Metric Reasoning About λ-Terms: The Affine Case [J].

Crubille, Raphaelle ;

Dal Lago, Ugo .

2015 30TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2015, :633-644

[49] Sibilla: A tool for reasoning about collective systems [J].

Del Giudice, Nicola ;

Matteucci, Lorenzo ;

Quadrini, Michela ;

Rehman, Aniqa ;

Loreti, Michele .

SCIENCE OF COMPUTER PROGRAMMING, 2024, 235

[50] Towards Verified Stochastic Variational Inference for Probabilistic Programs [J].

Lee, Wonyeol ;

Yu, Hangyeol ;

Rival, Xavier ;

Yang, Hongseok .

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2020, 4 (POPL)

← 1 2 3 4 5 →