Synthesizing Probabilistic Invariants via Doob's Decomposition

TL;DR

This paper introduces a novel method using Doob's decomposition to automatically synthesize complex martingales for probabilistic program analysis, avoiding constraint solving and enabling more powerful property inference.

Contribution

It presents a symbolic, constraint-free approach to generate and simplify martingales from arbitrary expressions, improving over existing semi-automatic methods.

Findings

Successfully applied to classical examples, surpassing current semi-automatic approaches.

Produces complex martingales expressed with conditional expectations.

Automates the optional stopping theorem application for property inference.

Abstract

When analyzing probabilistic computations, a powerful approach is to first find a martingale---an expression on the program variables whose expectation remains invariant---and then apply the optional stopping theorem in order to infer properties at termination time. One of the main challenges, then, is to systematically find martingales. We propose a novel procedure to synthesize martingale expressions from an arbitrary initial expression. Contrary to state-of-the-art approaches, we do not rely on constraint solving. Instead, we use a symbolic construction based on Doob's decomposition. This procedure can produce very complex martingales, expressed in terms of conditional expectations. We show how to automatically generate and simplify these martingales, as well as how to apply the optional stopping theorem to infer properties at termination time. This last step typically involves some simplification steps, and is usually done manually in current approaches. We implement our techniques in a prototype tool and demonstrate our process on several classical examples. Some of them go beyond the capability of current semi-automatic approaches.