A Semantics for Probabilistic Control-Flow Graphs
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).
Cite
@article{arxiv.1711.02256,
title = {A Semantics for Probabilistic Control-Flow Graphs},
author = {Torben Amtoft and Anindya Banerjee},
journal= {arXiv preprint arXiv:1711.02256},
year = {2017}
}
Comments
In a companion paper, also just submitted to arXiv, the semantics is used to reason about slicing. So as to make each paper self-contained, there is some overlap between them