Generating Functions for Probabilistic Programs

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

doi:10.1007/978-3-030-68446-4_12

Generating Functions for Probabilistic Programs

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

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

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	https://doi.org/10.1007/978-3-030-68446-4_12
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	https://link.springer.com/book/10.1007/978-3-030-68446-4

Keywords

Formal power series
Probabilistic programs
Quantitative verification
Semantics

Access to Document

10.1007/978-3-030-68446-4_12

1 Preprint

Generating Functions for Probabilistic Programs
Klinkenberg, L., Batz, K., Kaminski, B. L., Katoen, J.-P., Moerman, J. & Winkler, T., Jul 2020, Cornell University - arXiv.
Research output: Working paper / Preprint › Preprint

Open Access

Cite this

Klinkenberg, L., Batz, K., Kaminski, B. L., Katoen, J.-P., Moerman, J., & Winkler, T. (2021). Generating Functions for Probabilistic Programs. In Maribel Fernández (Ed.), Logic-Based Program Synthesis and Transformation: 30th International Symposium, LOPSTR 2020, Bologna, Italy, September 7–9, 2020, Proceedings (1 ed., pp. 231-248). Springer. https://doi.org/10.1007/978-3-030-68446-4_12

Klinkenberg, Lutz ; Batz, Kevin ; Kaminski, Benjamin Lucien et al. / Generating Functions for Probabilistic Programs. Logic-Based Program Synthesis and Transformation: 30th International Symposium, LOPSTR 2020, Bologna, Italy, September 7–9, 2020, Proceedings. editor / Maribel Fernández. 1. ed. Cham : Springer, 2021. pp. 231-248 (Lecture Notes in Computer Science, Vol. 12561).

@inproceedings{b23db3b436c145529f2382aa32492858,

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.",

keywords = "Formal power series, Probabilistic programs, Quantitative verification, Semantics",

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.; 30th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2020 ; Conference date: 07-09-2020 Through 09-09-2020",

year = "2021",

month = feb,

day = "13",

doi = "10.1007/978-3-030-68446-4\_12",

language = "English",

isbn = "978-3-030-68445-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "231--248",

editor = "\{Maribel Fern{\'a}ndez\}",

booktitle = "Logic-Based Program Synthesis and Transformation",

address = "United States",

edition = "1",

url = "https://link.springer.com/book/10.1007/978-3-030-68446-4",

}

Klinkenberg, L, Batz, K, Kaminski, BL, Katoen, J-P, Moerman, J & Winkler, T 2021, Generating Functions for Probabilistic Programs. in Maribel Fernández (ed.), Logic-Based Program Synthesis and Transformation: 30th International Symposium, LOPSTR 2020, Bologna, Italy, September 7–9, 2020, Proceedings. 1 edn, Springer, Cham, Lecture Notes in Computer Science, vol. 12561, pp. 231-248, 30th International Symposium on Logic-Based Program Synthesis and Transformation, Bologna, Italy, 7/09/20. https://doi.org/10.1007/978-3-030-68446-4_12

Generating Functions for Probabilistic Programs. / Klinkenberg, Lutz; Batz, Kevin; Kaminski, Benjamin Lucien et al.
Logic-Based Program Synthesis and Transformation: 30th International Symposium, LOPSTR 2020, Bologna, Italy, September 7–9, 2020, Proceedings. ed. / Maribel Fernández. 1. ed. Cham: Springer, 2021. p. 231-248 (Lecture Notes in Computer Science, Vol. 12561).

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

TY - GEN

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 - 2021/2/13

Y1 - 2021/2/13

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.

KW - Formal power series

KW - Probabilistic programs

KW - Quantitative verification

KW - Semantics

U2 - 10.1007/978-3-030-68446-4_12

DO - 10.1007/978-3-030-68446-4_12

M3 - Conference Article in proceeding

SN - 978-3-030-68445-7

SN - 978-3-030-68447-1

T3 - Lecture Notes in Computer Science

SP - 231

EP - 248

BT - Logic-Based Program Synthesis and Transformation

A2 - Maribel Fernández,

PB - Springer

CY - Cham

T2 - 30th International Symposium on Logic-Based Program Synthesis and Transformation

Y2 - 7 September 2020 through 9 September 2020

ER -

Klinkenberg L, Batz K, Kaminski BL, Katoen JP, Moerman J, Winkler T. Generating Functions for Probabilistic Programs. In Maribel Fernández, editor, Logic-Based Program Synthesis and Transformation: 30th International Symposium, LOPSTR 2020, Bologna, Italy, September 7–9, 2020, Proceedings. 1 ed. Cham: Springer. 2021. p. 231-248. (Lecture Notes in Computer Science, Vol. 12561). doi: 10.1007/978-3-030-68446-4_12

Generating Functions for Probabilistic Programs

Abstract

Publication series

Symposium

Keywords

Access to Document

Fingerprint

Research output

Generating Functions for Probabilistic Programs

Cite this