TY  - GEN
N1  - This version is the author accepted manuscript. For information on re-use, please refer to the publisher?s terms and conditions.
AV  - public
SP  - 231
Y1  - 2021/02/13/
EP  - 248
TI  - Generating Functions for Probabilistic Programs
T3  - Lecture Notes in Computer Science
A1  - Klinkenberg, L
A1  - Batz, K
A1  - Kaminski, BL
A1  - Katoen, JP
A1  - Moerman, J
A1  - Winkler, T
KW  - Probabilistic programs; Quantitative verification; Semantics; Formal power series
UR  - https://doi.org/10.1007/978-3-030-68446-4_12
PB  - Springer
SN  - 1611-3349
N2  - 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.
ID  - discovery10128255
ER  -