@inproceedings{10.1007/978-3-030-68446-4_12,
    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.},
    Address = {Cham},
    Author = {Klinkenberg, Lutz and Batz, Kevin and Kaminski, Benjamin Lucien and Katoen, Joost-Pieter and Moerman, Joshua and Winkler, Tobias},
    BookTitle = {Logic-Based Program Synthesis and Transformation},
    Editor = {Fern{\'a}ndez, Maribel},
    File = {Generating Functions for Probabilistic Programs - Klinkenberg2021\_Chapter\_GeneratingFunctionsForProbabil - n - n.pdf},
    ISBN = {978-3-030-68446-4},
    Pages = {231--248},
    Publisher = {Springer International Publishing},
    Title = {Generating Functions for Probabilistic Programs},
    Year = {2021},
    date-added = {2021-03-29 21:04:44 +0200},
    date-modified = {2021-03-29 21:04:44 +0200},
    doi = {10.1007/978-3-030-68446-4_12}
}

@inproceedings{10.1007/978-3-030-68446-4_12, 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.}, Address = {Cham}, Author = {Klinkenberg, Lutz and Batz, Kevin and Kaminski, Benjamin Lucien and Katoen, Joost-Pieter and Moerman, Joshua and Winkler, Tobias}, BookTitle = {Logic-Based Program Synthesis and Transformation}, Editor = {Fern{\'a}ndez, Maribel}, File = {Generating Functions for Probabilistic Programs - Klinkenberg2021_Chapter_GeneratingFunctionsForProbabil - n - n.pdf}, ISBN = {978-3-030-68446-4}, Pages = {231--248}, Publisher = {Springer International Publishing}, Title = {Generating Functions for Probabilistic Programs}, Year = {2021}, date-added = {2021-03-29 21:04:44 +0200}, date-modified = {2021-03-29 21:04:44 +0200}, doi = {10.1007/978-3-030-68446-4_12} }