@inproceedings{discovery10128255,
           title = {Generating Functions for Probabilistic Programs},
            year = {2021},
       publisher = {Springer},
         journal = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
           month = {February},
          series = {Lecture Notes in Computer Science},
       booktitle = {Logic-Based Program Synthesis and Transformation},
           pages = {231--248},
          volume = {12561},
            note = {This version is the author accepted manuscript. For information on re-use, please refer to the publisher's terms and conditions.},
            issn = {1611-3349},
          author = {Klinkenberg, L and Batz, K and Kaminski, BL and Katoen, JP and Moerman, J and Winkler, T},
        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.},
             url = {https://doi.org/10.1007/978-3-030-68446-4\%5f12},
        keywords = {Probabilistic programs; Quantitative verification; Semantics; Formal power series}
}