Reasoning about Recursive Probabilistic Programs

DOI10.1145/2933575.2935317zbMATH Open1401.68048arXiv1603.02922OpenAlexW2294463722MaRDI QIDQ4635928FDOQ4635928

Authors: Federico Olmedo, Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen 

Publication date: 23 April 2018

Published in: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/1603.02922

Recommendations

• Reasoning about probabilistic sequential programs
• Reasoning about probabilistic sequential programs in a probabilistic logic
• scientific article; zbMATH DE number 3890702
• Reasoning About States of Probabilistic Sequential Programs
• Automated reasoning for probabilistic sequential programs with theorem proving
• Mathematics of Program Construction
• Understanding probabilistic programs
• Fine-grained semantics for probabilistic programs
• Probabilistic programming inference via intensional semantics

zbMATH Keywords

recursionprogram verificationexpected runtimeprobabilisitic programmingweakest pre-condition calculus

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (24)

• Calibrating generative models: the probabilistic Chomsky-Schützenberger hierarchy
• Inferring expected runtimes of probabilistic integer programs using expected sizes
• Time-bounded termination analysis for probabilistic programs with delays
• Probabilistic programming inference via intensional semantics
• A weakest pre-expectation semantics for mixed-sign expectations
• Weakest precondition reasoning for expected run-times of probabilistic programs
• Efficient analysis of probabilistic programs with an unbounded counter
• Reasoning about probabilistic sequential programs
• Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
• On Lexicographic Proof Rules for Probabilistic Termination
• Weakest precondition reasoning for expected runtimes of randomized algorithms
• A type theory for probabilistic and Bayesian reasoning
• On lexicographic proof rules for probabilistic termination
• Runtime analysis of probabilistic programs with unbounded recursion
• Title not available (Why is that?)
• Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems
• Refinement algebra for probabilistic programs
• Quantum weakest preconditions for reasoning about expected runtimes of quantum programs
• A denotational semantics for low-level probabilistic programs with nondeterminism
• Formal semantics of a classical-quantum language
• Inferring covariances for probabilistic programs
• Title not available (Why is that?)
• Certificates for probabilistic pushdown automata via optimistic value iteration
• Runtime analysis of probabilistic programs with unbounded recursion

This page was built for publication: Reasoning about Recursive Probabilistic Programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635928)