Quantitative Verification of Omega-regular Properties in Probabilistic Programming
This addresses the limitation of existing inference techniques that fail to handle temporal behaviors in probabilistic models, offering a solution for domains requiring rigorous temporal verification.
The paper tackles the problem of capturing temporal evolution in probabilistic programming by introducing temporal posterior inference (TPI), which computes posterior distributions over execution traces that satisfy omega-regular properties, conditioned on temporal observations, and demonstrates effective and efficient inference in benchmarks.
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.