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 条
  • [21] LINEARIZING SOME RECURSIVE LOGIC PROGRAMS
    GUESSARIAN, I
    PIN, JE
    IEEE TRANSACTIONS ON KNOWLEDGE AND DATA ENGINEERING, 1995, 7 (01) : 137 - 149
  • [22] Probabilistic Fuzzy Reasoning in a Coherent Setting
    Coletti, Giulianella
    Petturiti, Davide
    Vantaggi, Barbara
    PROCEEDINGS OF THE 8TH CONFERENCE OF THE EUROPEAN SOCIETY FOR FUZZY LOGIC AND TECHNOLOGY (EUSFLAT-13), 2013, 32 : 440 - 447
  • [23] Running Probabilistic Programs Backwards
    Toronto, Neil
    McCarthy, Jay
    Van Horn, David
    PROGRAMMING LANGUAGES AND SYSTEMS, 2015, 9032 : 53 - 79
  • [24] On the hardness of analyzing probabilistic programs
    Kaminski, Benjamin Lucien
    Katoen, Joost-Pieter
    Matheja, Christoph
    ACTA INFORMATICA, 2019, 56 (03) : 255 - 285
  • [25] Synthesizing Recursive Programs through Dataflow Constraints
    Mateu, Marta Davila
    COMPANION PROCEEDINGS OF THE 2023 ACM SIGPLAN INTERNATIONAL CONFERENCE ON SYSTEMS, PROGRAMMING, LANGUAGES, AND APPLICATIONS: SOFTWARE FOR HUMANITY, SPLASH COMPANION 2023, 2023, : 25 - 27
  • [26] PARALLELIZING RECURSIVE LOGIC PROGRAMS THROUGH DECOMPOSITION
    KLINGLER, A
    PENNER, V
    COMPUTERS AND ARTIFICIAL INTELLIGENCE, 1993, 12 (05): : 441 - 459
  • [27] Efficient parallel execution of irregular recursive programs
    Prechelt, L
    Hänssgen, SU
    IEEE TRANSACTIONS ON PARALLEL AND DISTRIBUTED SYSTEMS, 2002, 13 (02) : 167 - 178
  • [28] InfoVis Interaction Techniques in Animation of Recursive Programs
    Angel Velazquez-Iturbide, J.
    Perez-Carrasco, Antonio
    ALGORITHMS, 2010, 3 (01) : 76 - 91
  • [29] A Theory of Slicing for Imperative Probabilistic Programs
    Amtoft, Torben
    Banerjee, Anindya
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2020, 42 (02):
  • [30] The theory of interval probabilistic logic programs
    Dekhtyar, Alex
    Dekhtyar, Michael I.
    ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2009, 55 (3-4) : 355 - 388
12345