Generating Functions for Probabilistic Programs

Lutz Klinkenberg; Kevin Batz; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Joshua Moerman; Tobias Winkler

Generating Functions for Probabilistic Programs

Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Tobias Winkler

Research output: Working paper / Preprint › Preprint › Academic

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
Publisher	Cornell University - arXiv
Publication status	Published - Jul 2020
Externally published	Yes

Access to Document

1 Conference Article in proceeding

Generating Functions for Probabilistic Programs
Klinkenberg, L., Batz, K., Kaminski, B. L., Katoen, J.-P., Moerman, J. & Winkler, T., 13 Feb 2021, Logic-Based Program Synthesis and Transformation: 30th International Symposium, LOPSTR 2020, Bologna, Italy, September 7–9, 2020, Proceedings. Maribel Fernández (ed.). 1 ed. Cham: Springer, p. 231-248 18 p. (Lecture Notes in Computer Science, Vol. 12561).
Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

Cite this

@techreport{e931a19eb5aa48679e74dff98b5f6374,

title = "Generating Functions for Probabilistic Programs",

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{\textquoteright}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.",

author = "Lutz Klinkenberg and Kevin Batz and Kaminski, {Benjamin Lucien} and Joost-Pieter Katoen and Joshua Moerman and Tobias Winkler",

note = "DBLP License: DBLP's bibliographic metadata records provided through http://dblp.org/ are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.",

year = "2020",

month = jul,

language = "English",

publisher = "Cornell University - arXiv",

address = "United States",

type = "WorkingPaper",

institution = "Cornell University - arXiv",

}

TY - UNPB

T1 - Generating Functions for Probabilistic Programs

AU - Klinkenberg, Lutz

AU - Batz, Kevin

AU - Kaminski, Benjamin Lucien

AU - Katoen, Joost-Pieter

AU - Moerman, Joshua

AU - Winkler, Tobias

N1 - DBLP License: DBLP's bibliographic metadata records provided through http://dblp.org/ are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.

PY - 2020/7

Y1 - 2020/7

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.

AB - 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.

M3 - Preprint

BT - Generating Functions for Probabilistic Programs

PB - Cornell University - arXiv

ER -

Generating Functions for Probabilistic Programs

Abstract

Access to Document

Fingerprint

Research output

Generating Functions for Probabilistic Programs

Cite this