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
    [J]. 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
    [J]. 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
    [J]. 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
    [J]. 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
    [J]. JOURNAL OF LOGIC PROGRAMMING, 1999, 41 (2-3): : 141 - 195
  • [36] SMT-based model checking for recursive programs
    Komuravelli, Anvesh
    Gurfinkel, Arie
    Chaki, Sagar
    [J]. 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
    [J]. THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2024,
  • [38] Reasoning about Monotonicity in Separation Logic
    Timany, Amin
    Birkedal, Lars
    [J]. 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
    [J]. ARTIFICIAL INTELLIGENCE, 2009, 173 (9-10) : 901 - 934
  • [40] Semantic Reasoning about the Sea of Nodes
    Demange, Delphine
    de Retana, Yon Fernandez
    Pichardie, David
    [J]. CC'18: PROCEEDINGS OF THE 27TH INTERNATIONAL CONFERENCE ON COMPILER CONSTRUCTION, 2018, : 163 - 173
12345