Quantitative Verification of Omega-regular Properties in Probabilistic Programming

TL;DR

This paper introduces a novel framework called temporal posterior inference (TPI) that computes probabilistic distributions over execution traces satisfying omega-regular properties in probabilistic programming, providing rigorous guarantees and handling temporal observations.

Contribution

It unifies probabilistic programming with temporal logic, developing a new method for bounds on satisfaction probabilities and implementing a prototype tool for temporal property inference.

Findings

Effective inference over complex temporal properties

Efficient computation of satisfaction probability bounds

Successful evaluation on benchmark models

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.