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] On the Termination Problem for Probabilistic Higher-Order Recursive Programs
    Kobayashi, Naoki
    Dal Lago, Ugo
    Grellois, Charles
    2019 34TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2019,
  • [42] ON THE TERMINATION PROBLEM FOR PROBABILISTIC HIGHER-ORDER RECURSIVE PROGRAMS
    Kobayashi, Naoki
    Dal Lago, Ugo
    Grellois, Charles
    LOGICAL METHODS IN COMPUTER SCIENCE, 2020, 16 (04) : 1 - 57
  • [43] A Framework for Reasoning about the Semantics of Logic Programs
    Bull Eur Assoc Theor Comput Sci, 59 (426):
  • [44] REASONING ABOUT TERMINATION OF PURE PROLOG PROGRAMS
    APT, KR
    PEDRESCHI, D
    INFORMATION AND COMPUTATION, 1993, 106 (01) : 109 - 157
  • [45] Reasoning about Multi-stage Programs
    Inoue, Jun
    Taha, Walid
    PROGRAMMING LANGUAGES AND SYSTEMS, 2012, 7211 : 357 - 376
  • [46] Reasoning about Programs Using a Scientific Method
    O'Hearn, Peter W.
    FORMAL METHODS AND SOFTWARE ENGINEERING, 2011, 6991 : 14 - 14
  • [47] Algebraic rules for reasoning about BSP programs
    Stewart, A
    Clint, M
    Gabarró, J
    CONSTRUCTIVE METHODS FOR PARALLEL PROGRAMMING, 2002, 10 : 41 - 57
  • [48] TUTORIAL NOTES - REASONING ABOUT LOGIC PROGRAMS
    BUNDY, A
    LECTURE NOTES IN ARTIFICIAL INTELLIGENCE, 1992, 636 : 252 - 277
  • [49] Reasoning about multi-stage programs
    Inoue, Jun
    Taha, Walid
    JOURNAL OF FUNCTIONAL PROGRAMMING, 2016, 26 : 1 - 53
  • [50] Probabilistic Temporal Logic for Reasoning about Bounded Policies
    Motamed, Nima
    Alechina, Natasha
    Dastani, Mehdi
    Doder, Dragan
    Logan, Brian
    PROCEEDINGS OF THE THIRTY-SECOND INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, IJCAI 2023, 2023, : 3296 - 3303
12345