Reasoning about Recursive Probabilistic Programs

被引：51
|
作者：
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 条
  • [1] REASONING ABOUT PROBABILISTIC PARALLEL PROGRAMS
    RAO, JR
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1994, 16 (03): : 798 - 842
  • [2] Reasoning about probabilistic sequential programs
    Chadha, R.
    Cruz-Filipe, L.
    Mateus, P.
    Sernadas, A.
    [J]. THEORETICAL COMPUTER SCIENCE, 2007, 379 (1-2) : 142 - 165
  • [3] Reasoning about probabilistic sequential programs in a probabilistic logic
    Ying, MS
    [J]. ACTA INFORMATICA, 2003, 39 (05) : 315 - 389
  • [4] Reasoning about probabilistic sequential programs in a probabilistic logic
    M. Ying
    [J]. Acta Informatica, 2003, 39 : 315 - 389
  • [5] ωPAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable Programs
    Huot, Mathieu
    Lew, Alexander K.
    Mansinghka, Vikash K.
    Staton, Sam
    [J]. 2023 38TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, LICS, 2023,
  • [6] Reasoning about states of probabilistic sequential programs
    Chadha, R.
    Mateus, P.
    Sernadas, A.
    [J]. COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2006, 4207 : 240 - 255
  • [7] Developing and reasoning about probabilistic programs in pGCL
    McIver, Annabelle
    Morgan, Carroll
    [J]. REFINEMENT TECHNIQUES IN SOFTWARE ENGINEERING, 2006, 3167 : 123 - 155
  • [8] Reasoning about "Reasoning about Reasoning" Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and Recursion
    Zhang, Yizhou
    Amin, Nada
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2022, 6 (POPL):
  • [9] Reasoning about reasoning by nested conditioning: Modeling theory of mind with probabilistic programs
    Stuhlmueller, A.
    Goodman, N. D.
    [J]. COGNITIVE SYSTEMS RESEARCH, 2014, 28 : 80 - 99
  • [10] Local Reasoning About Probabilistic Behaviour for Classical-Quantum Programs
    Deng, Yuxin
    Wu, Huiling
    Xu, Ming
    [J]. VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2024, PT II, 2024, 14500 : 163 - 184
12345