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