Inferring covariances for probabilistic programs

DOI10.1007/978-3-319-43425-4_14MaRDI QIDQ1693100zbMATH OpenOpenAlexDBLPWikidataFDO

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

Publication date 11 January 2018

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

zbMATH Keywords

covarianceprobabilistic programsrun-time

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Abstract: We study weakest precondition reasoning about the (co)variance of outcomes and the variance of run-times of probabilistic programs with conditioning. For outcomes, we show that approximating (co)variances is computationally more difficult than approximating expected values. In particular, we prove that computing both lower and upper bounds for (co)variances is $Sigm{a}_2^0$-complete. As a consequence, neither lower nor upper bounds are computably enumerable. We therefore present invariant-based techniques that do enable enumeration of both upper and lower bounds, once appropriate invariants are found. Finally, we extend this approach to reasoning about run-time variances.

Recommendations

• On the hardness of analyzing probabilistic programs
• Weakest precondition reasoning for expected run-times of probabilistic programs
• Conditioning in probabilistic programming
• Reasoning about Recursive Probabilistic Programs
• Inferring expected runtimes of probabilistic integer programs using expected sizes

Cited in

(1)

• On the hardness of analyzing probabilistic programs

This page was built for publication: Inferring covariances for probabilistic programs

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