A Semantics for Probabilistic Control-Flow Graphs

TL;DR

This paper introduces a new operational semantics for probabilistic control-flow graphs that accurately models probabilistic imperative programs with random and conditioning statements, enabling reliable reasoning about program correctness.

Contribution

It provides a novel semantics for pCFGs, relating them to structured probabilistic programs and proving translation adequacy for sound reasoning.

Findings

Semantic translation preserves probabilistic behavior

Operational semantics aligns with denotational semantics

Enables correctness reasoning for probabilistic program transformations

Abstract

This article develops a novel operational semantics for probabilistic control-flow graphs (pCFGs) of probabilistic imperative programs with random assignment and "observe" (or conditioning) statements. The semantics transforms probability distributions (on stores) as control moves from one node to another in pCFGs. We relate this semantics to a standard, expectation-transforming, denotational semantics of structured probabilistic imperative programs, by translating structured programs into (unstructured) pCFGs, and proving adequacy of the translation. This shows that the operational semantics can be used without loss of information, and is faithful to the "intended" semantics and hence can be used to reason about, for example, the correctness of transformations (as we do in a companion article).