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)
, Article 39. 10.1145/3434320.
Preview |
Text
Kaminski_3434320.pdf - Published Version Download (445kB) | Preview |
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 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1145/3434320 |
| Publisher version: | https://doi.org/10.1145/3434320 |
| Language: | English |
| Additional information: | This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited. |
| Keywords: | probabilistic programs, randomized algorithms, formal verification, quantitative verification, completeness, weakest precondition, weakest preexpectation |
| UCL classification: | UCL 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 |
Archive Staff Only
 |
View Item |
