Weakest precondition reasoning for expected run-times of probabilistic programs

DOI10.1007/978-3-662-49498-1_15MaRDI QIDQ2802489zbMATH OpenOpenAlexDBLPWikidataFDO

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

Publication date 26 April 2016

Published in Programming Languages and Systems (Search for Journal in Brave)

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

zbMATH Keywords

program verificationweakest preconditionprobabilistic programsexpected run-timepositive almost-sure termination

Mathematics Subject Classification ID

Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: This paper presents a wp-style calculus for obtaining bounds on the expected run-time of probabilistic programs. Its application includes determining the (possibly infinite) expected termination time of a probabilistic program and proving positive almost-sure termination - does a program terminate with probability one in finite expected time? We provide several proof rules for bounding the run-time of loops, and prove the soundness of the approach with respect to a simple operational model. We show that our approach is a conservative extension of Nielson's approach for reasoning about the run-time of deterministic programs. We analyze the expected run-time of some example programs including a one-dimensional random walk and the coupon collector problem.

Recommendations

• Weakest precondition reasoning for expected runtimes of randomized algorithms
• Reasoning about Recursive Probabilistic Programs
• Formalising Semantics for Expected Running Time of Probabilistic Programs
• Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs
• On the hardness of analyzing probabilistic programs

Cites work

• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• scientific article; zbMATH DE number 51770 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 1927425 (Why is no real title available?)
• scientific article; zbMATH DE number 1832220 (Why is no real title available?)
• scientific article; zbMATH DE number 819814 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A Hoare-like proof system for analysing the computation time of programs
• A general framework for sound and complete Floyd-Hoare logics
• A probability perspective
• Abstraction, Refinement and Proof for Probabilistic Systems
• An axiomatic basis for computer programming
• Automating program analysis
• FM 2005: Formal Methods
• Formalization of time and space
• Logic Based Program Synthesis and Transformation
• On the hardness of almost-sure termination
• Probabilistic termination: soundness, completeness, and compositionality
• Probability and Computing
• Runtime analysis of probabilistic programs with unbounded recursion
• Semantics of probabilistic programs
• Semantics with applications: an appetizer.
• Weakest precondition reasoning for expected run-times of probabilistic programs

Cited in

(33)

• Fair termination for parameterized probabilistic concurrent systems
• Inferring expected runtimes of probabilistic integer programs using expected sizes
• Time-bounded termination analysis for probabilistic programs with delays
• Quantitative program logic and expected time bounds in probabilistic distributed algorithms.
• Weakest precondition reasoning for expected run-times of probabilistic programs
• A weakest pre-expectation semantics for mixed-sign expectations
• Formalising Semantics for Expected Running Time of Probabilistic Programs
• Efficient analysis of probabilistic programs with an unbounded counter
• A temporal logic for proving properties of topologically general executions
• On the hardness of analyzing probabilistic programs
• Weakest preconditions in fibrations
• A probabilistic analysis of loop programs
• Weakest precondition reasoning for expected runtimes of randomized algorithms
• Weakest preconditions in fibrations
• A type theory for probabilistic and Bayesian reasoning
• Exponential automatic amortized resource analysis
• Runtime analysis of probabilistic programs with unbounded recursion
• scientific article; zbMATH DE number 2147036 (Why is no real title available?)
• A trustful monad for axiomatic reasoning with probability and nondeterminism
• Verified analysis of random binary tree structures
• Computing expected runtimes for constant probability programs
• A specification logic for programs in the probabilistic guarded command language
• Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
• Automatic analysis of expected termination time for population protocols
• Quantum weakest preconditions for reasoning about expected runtimes of quantum programs
• Quantum expectation transformers for cost analysis
• A denotational semantics for low-level probabilistic programs with nondeterminism
• Solving invariant generation for unsolvable loops
• Moment-based analysis of Bayesian network properties
• Inferring covariances for probabilistic programs
• Automatic probabilistic program verification through random variable abstraction
• Data-Driven Invariant Learning for Probabilistic Programs
• Probabilistic program verification via inductive synthesis of inductive invariants

This page was built for publication: Weakest precondition reasoning for expected run-times of probabilistic programs

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