Efficient Analysis of Probabilistic Programs with an Unbounded Counter

TL;DR

This paper presents an efficient method for analyzing a subclass of infinite-state probabilistic programs modeled by probabilistic one-counter automata, focusing on expected termination time and probability of satisfying properties.

Contribution

It introduces polynomial-time approximation algorithms for key quantitative properties of pOC and establishes a novel connection between pOC and martingale theory.

Findings

Expected termination time can be approximated with arbitrary precision.

Probability of satisfying omega-regular properties can be efficiently estimated.

A divergence gap theorem bounds non-termination probability away from zero.

Abstract

We show that a subclass of infinite-state probabilistic programs that can be modeled by probabilistic one-counter automata (pOC) admits an efficient quantitative analysis. In particular, we show that the expected termination time can be approximated up to an arbitrarily small relative error with polynomially many arithmetic operations, and the same holds for the probability of all runs that satisfy a given omega-regular property. Further, our results establish a powerful link between pOC and martingale theory, which leads to fundamental observations about quantitative properties of runs in pOC. In particular, we provide a "divergence gap theorem", which bounds a positive non-termination probability in pOC away from zero.