Robust Probabilistic Model Checking with Continuous Reward Domains

• URL: http://arxiv.org/abs/2502.04530v1
• Date: Thu, 06 Feb 2025 22:03:18 GMT
• Title: Robust Probabilistic Model Checking with Continuous Reward Domains
• Authors: Xiaotong Ji, Hanchun Wang, Antonio Filieri, Ilenia Epifani,
• Abstract summary: We propose a novel method for handling both continuous and discrete reward distributions in Discrete Time Markov Chains. Our method approximates the reward distribution with theoretically bounded error while preserving the statistical properties of the true distribution.
• Score: 1.7829696876801548
• License:
• Abstract: Probabilistic model checking traditionally verifies properties on the expected value of a measure of interest. This restriction may fail to capture the quality of service of a significant proportion of a system's runs, especially when the probability distribution of the measure of interest is poorly represented by its expected value due to heavy-tail behaviors or multiple modalities. Recent works inspired by distributional reinforcement learning use discrete histograms to approximate integer reward distribution, but they struggle with continuous reward space and present challenges in balancing accuracy and scalability. We propose a novel method for handling both continuous and discrete reward distributions in Discrete Time Markov Chains using moment matching with Erlang mixtures. By analytically deriving higher-order moments through Moment Generating Functions, our method approximates the reward distribution with theoretically bounded error while preserving the statistical properties of the true distribution. This detailed distributional insight enables the formulation and robust model checking of quality properties based on the entire reward distribution function, rather than restricting to its expected value. We include a theoretical foundation ensuring bounded approximation errors, along with an experimental evaluation demonstrating our method's accuracy and scalability in practical model-checking problems.

Related papers

• Theory on Score-Mismatched Diffusion Models and Zero-Shot Conditional Samplers [49.97755400231656]
  We present the first performance guarantee with explicit dimensional general score-mismatched diffusion samplers. We show that score mismatches result in an distributional bias between the target and sampling distributions, proportional to the accumulated mismatch between the target and training distributions. This result can be directly applied to zero-shot conditional samplers for any conditional model, irrespective of measurement noise.
  arXiv  Detail & Related papers  (2024-10-17T16:42:12Z)
• Dr. FERMI: A Stochastic Distributionally Robust Fair Empirical Risk Minimization Framework [12.734559823650887]
  In the presence of distribution shifts, fair machine learning models may behave unfairly on test data. Existing algorithms require full access to data and cannot be used when small batches are used. This paper proposes the first distributionally robust fairness framework with convergence guarantees that do not require knowledge of the causal graph.
  arXiv  Detail & Related papers  (2023-09-20T23:25:28Z)
• User-defined Event Sampling and Uncertainty Quantification in Diffusion Models for Physical Dynamical Systems [49.75149094527068]
  We show that diffusion models can be adapted to make predictions and provide uncertainty quantification for chaotic dynamical systems. We develop a probabilistic approximation scheme for the conditional score function which converges to the true distribution as the noise level decreases. We are able to sample conditionally on nonlinear userdefined events at inference time, and matches data statistics even when sampling from the tails of the distribution.
  arXiv  Detail & Related papers  (2023-06-13T03:42:03Z)
• On Tail Decay Rate Estimation of Loss Function Distributions [5.33024001730262]
  We develop a novel theory for estimating the tails of marginal distributions. We show that under some regularity conditions, the shape parameter of the marginal distribution is the maximum tail shape parameter of the family of conditional distributions.
  arXiv  Detail & Related papers  (2023-06-05T11:58:25Z)
• A Targeted Accuracy Diagnostic for Variational Approximations [8.969208467611896]
  Variational Inference (VI) is an attractive alternative to Markov Chain Monte Carlo (MCMC) Existing methods characterize the quality of the whole variational distribution. We propose the TArgeted Diagnostic for Distribution Approximation Accuracy (TADDAA)
  arXiv  Detail & Related papers  (2023-02-24T02:50:18Z)
• Robust Estimation for Nonparametric Families via Generative Adversarial Networks [92.64483100338724]
  We provide a framework for designing Generative Adversarial Networks (GANs) to solve high dimensional robust statistics problems. Our work extend these to robust mean estimation, second moment estimation, and robust linear regression. In terms of techniques, our proposed GAN losses can be viewed as a smoothed and generalized Kolmogorov-Smirnov distance.
  arXiv  Detail & Related papers  (2022-02-02T20:11:33Z)
• Predicting with Confidence on Unseen Distributions [90.68414180153897]
  We connect domain adaptation and predictive uncertainty literature to predict model accuracy on challenging unseen distributions. We find that the difference of confidences (DoC) of a classifier's predictions successfully estimates the classifier's performance change over a variety of shifts. We specifically investigate the distinction between synthetic and natural distribution shifts and observe that despite its simplicity DoC consistently outperforms other quantifications of distributional difference.
  arXiv  Detail & Related papers  (2021-07-07T15:50:18Z)
• Achieving Efficiency in Black Box Simulation of Distribution Tails with Self-structuring Importance Samplers [1.6114012813668934]
  The paper presents a novel Importance Sampling (IS) scheme for estimating distribution of performance measures modeled with a rich set of tools such as linear programs, integer linear programs, piecewise linear/quadratic objectives, feature maps specified with deep neural networks, etc.
  arXiv  Detail & Related papers  (2021-02-14T03:37:22Z)
• GenDICE: Generalized Offline Estimation of Stationary Values [108.17309783125398]
  We show that effective estimation can still be achieved in important applications. Our approach is based on estimating a ratio that corrects for the discrepancy between the stationary and empirical distributions. The resulting algorithm, GenDICE, is straightforward and effective.
  arXiv  Detail & Related papers  (2020-02-21T00:27:52Z)
• Distributionally Robust Bayesian Quadrature Optimization [60.383252534861136]
  We study BQO under distributional uncertainty in which the underlying probability distribution is unknown except for a limited set of its i.i.d. samples. A standard BQO approach maximizes the Monte Carlo estimate of the true expected objective given the fixed sample set. We propose a novel posterior sampling based algorithm, namely distributionally robust BQO (DRBQO) for this purpose.
  arXiv  Detail & Related papers  (2020-01-19T12:00:33Z)

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.