UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Relatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-Based Reasoning

Batz, K; Kaminski, BL; Katoen, J-P; Matheja, C; (2021) Relatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-Based Reasoning. Proceedings of the ACM on Programming Languages , 5 (POPL) 10.1145/3434320. (In press).

[img] Text
main.pdf - Accepted version
Access restricted to UCL open access staff until 25 May 2021.

Download (995kB)

Abstract

We study a syntax for specifying quantitative “assertions” - functions mapping program states to numbers - for probabilistic program verification. We prove that our syntax is expressive in the following sense: Given any probabilistic program C, if a function f is expressible in our syntax, then the function mapping each initial state σ to the expected value of f evaluated in the final states reached after termination C on σ (also called the weakest preexpectation wp[C](f)) is also expressible in our syntax. As a consequence, we obtain a relatively complete verification system for verifying expected values and probabilities in the sense of Cook: Apart from a single reasoning step about the inequality of two functions given as syntactic expressions in our language, given f, g, and C, we can check whether g ≤ wp[C](f).

Type: Article
Title: Relatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-Based Reasoning
DOI: 10.1145/3434320
Publisher version: https://dl.acm.org/journal/pacmpl
Language: English
Keywords: probabilistic programs, randomized algorithms, formal verification, quantitative verification, completeness, weakest precondition, weakest preexpectation
UCL classification: UCL
UCL > Provost and Vice Provost Offices
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: https://discovery.ucl.ac.uk/id/eprint/10115802
Downloads since deposit
1Download
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item