Quantitative Verification of Omega-regular Properties in Probabilistic Programming

• URL: http://arxiv.org/abs/2512.21596v1
• Date: Thu, 25 Dec 2025 09:26:29 GMT
• Title: Quantitative Verification of Omega-regular Properties in Probabilistic Programming
• Authors: Peixin Wang, Jianhao Bai, Min Zhang, C. -H. Luke Ong,
• Abstract summary: We introduce temporal posterior inference, a new framework that unifies probabilistic programming with temporal logic.<n>We develop a new method for computing upper and lower bounds on the satisfaction of probabilities of omega-regular properties.<n>We implement our approach in a prototype tool, TPInfer, and evaluate it on a suite of benchmarks.
• Score: 12.097479337434878
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Robust Probabilistic Model Checking with Continuous Reward Domains [1.7829696876801548]
  We propose a novel method for handling both continuous and discrete reward distributions in Discrete Time Markov Chains.<n>Our method approximates the reward distribution with theoretically bounded error while preserving the statistical properties of the true distribution.
  arXiv  Detail & Related papers  (2025-02-06T22:03:18Z)
• Score Matching-based Pseudolikelihood Estimation of Neural Marked Spatio-Temporal Point Process with Uncertainty Quantification [59.81904428056924]
  We introduce SMASH: a Score MAtching estimator for learning markedPs with uncertainty quantification. Specifically, our framework adopts a normalization-free objective by estimating the pseudolikelihood of markedPs through score-matching. The superior performance of our proposed framework is demonstrated through extensive experiments in both event prediction and uncertainty quantification.
  arXiv  Detail & Related papers  (2023-10-25T02:37:51Z)
• When Rigidity Hurts: Soft Consistency Regularization for Probabilistic Hierarchical Time Series Forecasting [69.30930115236228]
  Probabilistic hierarchical time-series forecasting is an important variant of time-series forecasting. Most methods focus on point predictions and do not provide well-calibrated probabilistic forecasts distributions. We propose PROFHiT, a fully probabilistic hierarchical forecasting model that jointly models forecast distribution of entire hierarchy.
  arXiv  Detail & Related papers  (2023-10-17T20:30:16Z)
• Conformal Quantitative Predictive Monitoring of STL Requirements for Stochastic Processes [4.279881803310469]
  We introduce textitquantitative predictive monitoring (QPM), the first PM method to support processes and rich specifications given in Signal Temporal Logic (STL) QPM provides a quantitative measure of satisfaction by predicting the quantitative (aka robust) STL semantics of $phi$. We show how our monitors can be combined in a compositional manner to handle composite formulas.
  arXiv  Detail & Related papers  (2022-11-04T11:08:29Z)
• Probabilistic Reconciliation of Count Time Series [0.6810856082577402]
  We propose a definition of coherency and reconciled probabilistic forecast. It applies to both real-valued and count variables. It is based on a generalization of Bayes' rule and it can reconcile both real-value and count variables.
  arXiv  Detail & Related papers  (2022-07-19T15:23:09Z)
• Distributional Gradient Boosting Machines [77.34726150561087]
  Our framework is based on XGBoost and LightGBM. We show that our framework achieves state-of-the-art forecast accuracy.
  arXiv  Detail & Related papers  (2022-04-02T06:32:19Z)
• Probabilistic Forecasting with Generative Networks via Scoring Rule Minimization [5.5643498845134545]
  We use generative neural networks to parametrize distributions on high-dimensional spaces by transforming draws from a latent variable. We train generative networks to minimize a predictive-sequential (or prequential) scoring rule on a recorded temporal sequence of the phenomenon of interest. Our method outperforms state-of-the-art adversarial approaches, especially in probabilistic calibration.
  arXiv  Detail & Related papers  (2021-12-15T15:51:12Z)
• Robust and Adaptive Temporal-Difference Learning Using An Ensemble of Gaussian Processes [70.80716221080118]
  The paper takes a generative perspective on policy evaluation via temporal-difference (TD) learning. The OS-GPTD approach is developed to estimate the value function for a given policy by observing a sequence of state-reward pairs. To alleviate the limited expressiveness associated with a single fixed kernel, a weighted ensemble (E) of GP priors is employed to yield an alternative scheme.
  arXiv  Detail & Related papers  (2021-12-01T23:15:09Z)
• Complex Event Forecasting with Prediction Suffix Trees: Extended Technical Report [70.7321040534471]
  Complex Event Recognition (CER) systems have become popular in the past two decades due to their ability to "instantly" detect patterns on real-time streams of events. There is a lack of methods for forecasting when a pattern might occur before such an occurrence is actually detected by a CER engine. We present a formal framework that attempts to address the issue of Complex Event Forecasting.
  arXiv  Detail & Related papers  (2021-09-01T09:52:31Z)
• Remaining Useful Life Estimation Under Uncertainty with Causal GraphNets [0.0]
  A novel approach for the construction and training of time series models is presented. The proposed method is appropriate for constructing predictive models for non-stationary time series.
  arXiv  Detail & Related papers  (2020-11-23T21:28:03Z)
• Evaluating probabilistic classifiers: Reliability diagrams and score decompositions revisited [68.8204255655161]
  We introduce the CORP approach, which generates provably statistically Consistent, Optimally binned, and Reproducible reliability diagrams in an automated way. Corpor is based on non-parametric isotonic regression and implemented via the Pool-adjacent-violators (PAV) algorithm.
  arXiv  Detail & Related papers  (2020-08-07T08:22:26Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.