Quantitative Verification of Omega-regular Properties in Probabilistic Programming
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915694107426816 |
|---|---|
| author | Wang, Peixin Bai, Jianhao Zhang, Min Ong, C. -H. Luke |
| author_facet | Wang, Peixin Bai, Jianhao Zhang, Min Ong, C. -H. Luke |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_21596 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Quantitative Verification of Omega-regular Properties in Probabilistic Programming Wang, Peixin Bai, Jianhao Zhang, Min Ong, C. -H. Luke Programming Languages Formal Languages and Automata Theory Machine Learning Logic in Computer Science Symbolic Computation F.3.1; F.3.2; D.3.1 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. |
| title | Quantitative Verification of Omega-regular Properties in Probabilistic Programming |
| topic | Programming Languages Formal Languages and Automata Theory Machine Learning Logic in Computer Science Symbolic Computation F.3.1; F.3.2; D.3.1 |
| url | https://arxiv.org/abs/2512.21596 |