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.
Original language | English |
---|---|
Title of host publication | Logic-Based Program Synthesis and Transformation |
Subtitle of host publication | 30th International Symposium, LOPSTR 2020, Bologna, Italy, September 7–9, 2020, Proceedings |
Editors | Maribel Fernández |
Place of Publication | Cham |
Publisher | Springer |
Pages | 231-248 |
Number of pages | 18 |
Edition | 1 |
ISBN (Electronic) | 978-3-030-68446-4 |
ISBN (Print) | 978-3-030-68445-7, 978-3-030-68447-1 |
DOIs | |
Publication status | Published - 13 Feb 2021 |
Event | 30th International Symposium on Logic-Based Program Synthesis and Transformation - Bologna, Italy Duration: 7 Sept 2020 → 9 Sept 2020 https://link.springer.com/book/10.1007/978-3-030-68446-4 |
Publication series
Series | Lecture Notes in Computer Science |
---|---|
Volume | 12561 |
ISSN | 0302-9743 |
Symposium
Symposium | 30th International Symposium on Logic-Based Program Synthesis and Transformation |
---|---|
Abbreviated title | LOPSTR 2020 |
Country/Territory | Italy |
City | Bologna |
Period | 7/09/20 → 9/09/20 |
Internet address |