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