eprintid: 10128255 rev_number: 17 eprint_status: archive userid: 608 dir: disk0/10/12/82/55 datestamp: 2021-05-21 09:27:35 lastmod: 2022-02-14 07:11:27 status_changed: 2021-05-21 09:27:35 type: proceedings_section metadata_visibility: show creators_name: Klinkenberg, L creators_name: Batz, K creators_name: Kaminski, BL creators_name: Katoen, JP creators_name: Moerman, J creators_name: Winkler, T title: Generating Functions for Probabilistic Programs ispublished: pub divisions: UCL divisions: B04 divisions: C05 divisions: F48 keywords: Probabilistic programs; Quantitative verification; Semantics; Formal power series note: This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. 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. date: 2021-02-13 date_type: published publisher: Springer official_url: https://doi.org/10.1007/978-3-030-68446-4_12 oa_status: green full_text_type: other language: eng primo: open primo_central: open_green verified: verified_manual elements_id: 1800663 doi: 10.1007/978-3-030-68446-4_12 isbn_13: 9783030684457 lyricists_name: Kaminski, Benjamin lyricists_id: BKAMI07 actors_name: Kaminski, Benjamin actors_id: BKAMI07 actors_role: owner full_text_status: public series: Lecture Notes in Computer Science publication: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) volume: 12561 pagerange: 231-248 event_title: International Symposium on Logic-Based Program Synthesis and Transformation issn: 1611-3349 book_title: Logic-Based Program Synthesis and Transformation citation: Klinkenberg, L; Batz, K; Kaminski, BL; Katoen, JP; Moerman, J; Winkler, T; (2021) Generating Functions for Probabilistic Programs. In: Logic-Based Program Synthesis and Transformation. (pp. pp. 231-248). Springer Green open access document_url: https://discovery.ucl.ac.uk/id/eprint/10128255/1/2007.06327v1.pdf