Weakest precondition reasoning for expected run-times of probabilistic programs

DOI10.1007/978-3-662-49498-1_15zbMATH Open1335.68058DBLPconf/esop/KaminskiKMO16arXiv1601.01001OpenAlexW2222812367WikidataQ57800587 ScholiaQ57800587MaRDI QIDQ2802489FDOQ2802489

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

Publication date: 26 April 2016

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

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.

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

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Semantics with applications: an appetizer.
• An axiomatic basis for computer programming
• Title not available (Why is that?)
• Probability and Computing
• Title not available (Why is that?)
• Abstraction, Refinement and Proof for Probabilistic Systems
• Semantics of probabilistic programs
• A general framework for sound and complete Floyd-Hoare logics
• Title not available (Why is that?)
• Title not available (Why is that?)
• A probability perspective
• Probabilistic termination: soundness, completeness, and compositionality
• Automating program analysis
• Runtime analysis of probabilistic programs with unbounded recursion
• Title not available (Why is that?)
• FM 2005: Formal Methods
• A Hoare-like proof system for analysing the computation time of programs
• Formalization of time and space
• Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs
• On the Hardness of Almost–Sure Termination
• Logic Based Program Synthesis and Transformation

Cited In (26)

• Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs
• Time-bounded termination analysis for probabilistic programs with delays
• Quantitative program logic and expected time bounds in probabilistic distributed algorithms.
• Formalising Semantics for Expected Running Time of Probabilistic Programs
• Automatic Analysis of Expected Termination Time for Population Protocols
• Weakest preconditions in fibrations
• A temporal logic for proving properties of topologically general executions
• On the hardness of analyzing probabilistic programs
• A probabilistic analysis of loop programs
• Fair Termination for Parameterized Probabilistic Concurrent Systems
• Weakest preconditions in fibrations
• Exponential automatic amortized resource analysis
• Title not available (Why is that?)
• A trustful monad for axiomatic reasoning with probability and nondeterminism
• Verified analysis of random binary tree structures
• A specification logic for programs in the probabilistic guarded command language
• Computing expected runtimes for constant probability programs
• Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
• Quantum weakest preconditions for reasoning about expected runtimes of quantum programs
• Quantum expectation transformers for cost analysis
• Solving invariant generation for unsolvable loops
• A denotational semantics for low-level probabilistic programs with nondeterminism
• Moment-based analysis of Bayesian network properties
• A Type Theory for Probabilistic and Bayesian Reasoning
• 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)