2015/04/01 by Friedrich Gretz, Gretz, Friedrich, Nils Jansen +9 · 2 citations
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Programming Languages (cs.PL) #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.1504.00198
openalex publication_date 2015/04/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We investigate the semantic intricacies of conditioning, a main feature in probabilistic programming. We provide a weakest (liberal) pre-condition (w(l)p) semantics for the elementary probabilistic programming language pGCL extended with conditioning. We prove that quantitative weakest (liberal) pre-conditions coincide with conditional (liberal) expected rewards in Markov chains and show that semantically conditioning is a truly conservative extension. We present two program transformations which entirely eliminate conditioning from any program and prove their correctness using the w(l)p-semantics. Finally, we show how the w(l)p-semantics can be used to determine conditional probabilities in a parametric anonymity protocol and show that an inductive w(l)p-semantics for conditioning in non-deterministic probabilistic programs cannot exist.