# Quantitative Verification of Omega-regular Properties in Probabilistic Programming

arXiv: https://arxiv.org/abs/2512.21596 · HTML: https://mlsanity.com/paper/2512.21596/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 17 of its 39 references that are in the map.
- First posted on arXiv 25 Dec 2025.

## Builds on (most cited first, 17 of 17)

- [An Introduction to Probabilistic Programming](https://mlsanity.com/paper/1809.10756/) (2018)
- [From Spot 2.0 to Spot 2.10: What's New?](https://mlsanity.com/paper/2206.11366/) (2022)
- [Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs](https://mlsanity.com/paper/1510.08517/) (2015)
- [Quantitative Supermartingale Certificates](https://mlsanity.com/paper/2504.05065/) (2025)
- [Supermartingale Certificates for Quantitative Omega-regular Verification and Control](https://mlsanity.com/paper/2505.18833/) (2025)
- [Inner-Approximating Reachable Sets for Polynomial Systems with Time-Varying Uncertainties](https://mlsanity.com/paper/1811.01086/) (2018)
- [Polynomial Invariant Generation for Non-deterministic Recursive Programs](https://mlsanity.com/paper/1902.04373/) (2019)
- [Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs](https://mlsanity.com/paper/1601.01001/) (2016)
- [Bounded Expectations: Resource Analysis for Probabilistic Programs](https://mlsanity.com/paper/1711.08847/) (2017)
- [Cost Analysis of Nondeterministic Probabilistic Programs](https://mlsanity.com/paper/1902.04659/) (2019)
- [Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time](https://mlsanity.com/paper/1902.04744/) (2019)
- [Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants](https://mlsanity.com/paper/2205.06152/) (2022)
- [Lower Bounds for Possibly Divergent Probabilistic Programs](https://mlsanity.com/paper/2302.06082/) (2023)
- [Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving](https://mlsanity.com/paper/2307.13160/) (2023)
- [Proving Expected Sensitivity of Probabilistic Programs](https://mlsanity.com/paper/1708.02537/) (2017)
- [A Unifying Approach to Product Constructions for Quantitative Temporal Inference](https://mlsanity.com/paper/2407.10465/) (2024)
- [Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops](https://mlsanity.com/paper/2411.10393/) (2024)

## Abstract (arXiv)

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.