Name
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. |
Year | DOI | Venue |
|---|---|---|
2020 | 10.1007/978-3-030-68446-4_12 | LOPSTR |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
19 | 6 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Lutz Klinkenberg | 1 | 0 | 0.34 |
| Kevin Batz | 2 | 2 | 2.39 |
| Benjamin Lucien Kaminski | 3 | 126 | 10.46 |
| Joost-Pieter Katoen | 4 | 4444 | 289.65 |
| Joshua Moerman | 5 | 0 | 0.34 |
| Tobias Winkler | 6 | 1 | 1.36 |