A Theory of Slicing for Probabilistic Control-Flow Graphs

TL;DR

This paper develops a formal theory for slicing probabilistic programs represented as control-flow graphs, enabling precise analysis and reduction of such programs while ensuring semantic correctness.

Contribution

It introduces a novel probabilistic slicing framework with syntactic conditions and algorithms, extending classical program analysis techniques to probabilistic settings.

Findings

Syntactic conditions for probabilistic slicing are established.

Any slice satisfying these conditions is proven semantically correct.

An algorithm for computing the least slice is provided.

Abstract

We present a theory for slicing probabilistic imperative programs -- containing random assignments, and ``observe'' statements (for conditioning) -- represented as probabilistic control-flow graphs (pCFGs) whose nodes modify probability distributions. We show that such a representation allows direct adaptation of standard machinery such as data and control dependence, postdominators, relevant variables, etc to the probabilistic setting. We separate the specification of slicing from its implementation: first we develop syntactic conditions that a slice must satisfy; next we prove that any such slice is semantically correct; finally we give an algorithm to compute the least slice. To generate smaller slices, we may in addition take advantage of knowledge that certain loops will terminate (almost) always. A key feature of our syntactic conditions is that they involve two disjoint slices such that the variables of one slice are probabilistically independent of the variables of the other. This leads directly to a proof of correctness of probabilistic slicing. In a companion article we show adequacy of the semantics of pCFGs with respect to the standard semantics of structured probabilistic programs.