Quantitative Verification of Omega-regular Properties in Probabilistic Programming

TL;DR

This paper addresses the gap between Bayesian posterior inference for probabilistic programs and temporal reasoning over executions. It introduces Temporal Posterior Inference (TPI) to compute the posterior probability $\Pr(\varphi \mid \psi)$ where $\varphi$ and $\psi$ are $\omega$-regular properties over traces. An automata-theoretic framework encodes temporal specifications as deterministic Rabin automata (DRAs) and decomposes the Rabin condition into persistence and recurrence via FOV/IOV concepts. The authors develop stochastic barrier certificates to bound the persistence and recurrence probabilities and combine them to obtain sound bounds on the overall satisfaction probability. A prototype TPInfer is implemented and evaluated on benchmarks with unbounded loops, demonstrating accurate, sound, and scalable temporal posterior verification for probabilistic programs.

Abstract

Probabilistic programming provides a high-level framework for specifying statistical models as executable programs with built-in randomness and conditioning. Existing inference techniques, however, typically compute posterior distributions over program states at fixed time points, most often at termination, thereby failing to capture the temporal evolution of probabilistic behaviors. We introduce temporal posterior inference (TPI), a new framework that unifies probabilistic programming with temporal logic by computing posterior distributions over execution traces that satisfy omega-regular specifications, conditioned on possibly temporal observations. To obtain rigorous quantitative guarantees, we develop a new method for computing upper and lower bounds on the satisfaction probabilities of omega-regular properties. Our approach decomposes Rabin acceptance conditions into persistence and recurrence components and constructs stochastic barrier certificates that soundly bound each component. We implement our approach in a prototype tool, TPInfer, and evaluate it on a suite of benchmarks, demonstrating effective and efficient inference over rich temporal properties in probabilistic models.