Klinkenberg, L;
Batz, K;
Kaminski, BL;
Katoen, JP;
Moerman, J;
Winkler, T;
(2021)
Generating Functions for Probabilistic Programs.
In:
Logic-Based Program Synthesis and Transformation.
(pp. pp. 231-248).
Springer
Preview |
Text
2007.06327v1.pdf - Accepted Version Download (371kB) | Preview |
Abstract
This paper investigates the usage of generating functions (GFs) encoding measures over the program variables for reasoning about discrete probabilistic programs. To that end, we define a denotational GF-transformer semantics for probabilistic while-programs, and show that it instantiates Kozen’s seminal distribution transformer semantics. We then study the effective usage of GFs for program analysis. We show that finitely expressible GFs enable checking super-invariants by means of computer algebra tools, and that they can be used to determine termination probabilities. The paper concludes by characterizing a class of—possibly infinite-state—programs whose semantics is a rational GF encoding a discrete phase-type distribution.
| Type: | Proceedings paper |
|---|---|
| Title: | Generating Functions for Probabilistic Programs |
| Event: | International Symposium on Logic-Based Program Synthesis and Transformation |
| ISBN-13: | 9783030684457 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-030-68446-4_12 |
| Publisher version: | https://doi.org/10.1007/978-3-030-68446-4_12 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| Keywords: | Probabilistic programs; Quantitative verification; Semantics; Formal power series |
| 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/10128255 |
Loading...
Loading...Loading...Loading...Archive Staff Only
 |
View Item |
