What Are the Odds? Improving the foundations of Statistical Model Checking

• URL: http://arxiv.org/abs/2404.05424v1
• Date: Mon, 8 Apr 2024 11:47:46 GMT
• Title: What Are the Odds? Improving the foundations of Statistical Model Checking
• Authors: Tobias Meggendorfer, Maximilian Weininger, Patrick Wienhöft,
• Abstract summary: Markov decision processes (MDPs) are a fundamental model for decision making under uncertainty. Traditionally verification algorithms assume exact knowledge of the probabilities that govern the behaviour of an MDP. We propose specialised approaches that exploit our knowledge of the MDP.
• Score: 3.789219860006095
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Markov decision processes (MDPs) are a fundamental model for decision making under uncertainty. They exhibit non-deterministic choice as well as probabilistic uncertainty. Traditionally, verification algorithms assume exact knowledge of the probabilities that govern the behaviour of an MDP. As this assumption is often unrealistic in practice, statistical model checking (SMC) was developed in the past two decades. It allows to analyse MDPs with unknown transition probabilities and provide probably approximately correct (PAC) guarantees on the result. Model-based SMC algorithms sample the MDP and build a model of it by estimating all transition probabilities, essentially for every transition answering the question: ``What are the odds?'' However, so far the statistical methods employed by the state of the art SMC algorithms are quite naive. Our contribution are several fundamental improvements to those methods: On the one hand, we survey statistics literature for better concentration inequalities; on the other hand, we propose specialised approaches that exploit our knowledge of the MDP. Our improvements are generally applicable to many kinds of problem statements because they are largely independent of the setting. Moreover, our experimental evaluation shows that they lead to significant gains, reducing the number of samples that the SMC algorithm has to collect by up to two orders of magnitude.

Related papers

• Learning Algorithms for Verification of Markov Decision Processes [20.5951492453299]
  We present a general framework for applying learning algorithms to the verification of Markov decision processes (MDPs) The presented framework focuses on probabilistic reachability, which is a core problem in verification.
  arXiv  Detail & Related papers  (2024-03-14T08:54:19Z)
• Online POMDP Planning with Anytime Deterministic Guarantees [11.157761902108692]
  Planning under uncertainty can be mathematically formalized using partially observable Markov decision processes (POMDPs) Finding an optimal plan for POMDPs can be computationally expensive and is feasible only for small tasks. We derive a deterministic relationship between a simplified solution that is easier to obtain and the theoretically optimal one.
  arXiv  Detail & Related papers  (2023-10-03T04:40:38Z)
• Measuring and Modeling Uncertainty Degree for Monocular Depth Estimation [50.920911532133154]
  The intrinsic ill-posedness and ordinal-sensitive nature of monocular depth estimation (MDE) models pose major challenges to the estimation of uncertainty degree. We propose to model the uncertainty of MDE models from the perspective of the inherent probability distributions. By simply introducing additional training regularization terms, our model, with surprisingly simple formations and without requiring extra modules or multiple inferences, can provide uncertainty estimations with state-of-the-art reliability.
  arXiv  Detail & Related papers  (2023-07-19T12:11:15Z)
• Provably Efficient UCB-type Algorithms For Learning Predictive State Representations [55.00359893021461]
  The sequential decision-making problem is statistically learnable if it admits a low-rank structure modeled by predictive state representations (PSRs) This paper proposes the first known UCB-type approach for PSRs, featuring a novel bonus term that upper bounds the total variation distance between the estimated and true models. In contrast to existing approaches for PSRs, our UCB-type algorithms enjoy computational tractability, last-iterate guaranteed near-optimal policy, and guaranteed model accuracy.
  arXiv  Detail & Related papers  (2023-07-01T18:35:21Z)
• Meta-Uncertainty in Bayesian Model Comparison [0.0]
  We propose a fully probabilistic framework for quantifying meta-uncertainty. We demonstrate the utility of the proposed method in the context of conjugate Bayesian regression, likelihood-based inference with Markov chain Monte Carlo, and simulation-based inference with neural networks.
  arXiv  Detail & Related papers  (2022-10-13T18:10:29Z)
• PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP [0.34410212782758043]
  We provide the first algorithm to compute mean payoff probably approximately correctly in unknown MDP. We do not require any knowledge of the state space, only a lower bound on the minimum transition probability. In addition to providing probably approximately correct (PAC) bounds for our algorithm, we also demonstrate its practical nature by running experiments on standard benchmarks.
  arXiv  Detail & Related papers  (2022-06-03T09:13:27Z)
• Robust Anytime Learning of Markov Decision Processes [8.799182983019557]
  In data-driven applications, deriving precise probabilities from limited data introduces statistical errors. Uncertain MDPs (uMDPs) do not require precise probabilities but instead use so-called uncertainty sets in the transitions. We propose a robust anytime-learning approach that combines a dedicated Bayesian inference scheme with the computation of robust policies.
  arXiv  Detail & Related papers  (2022-05-31T14:29:55Z)
• Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise [59.47042225257565]
  We present a novel planning method that does not rely on any explicit representation of the noise distributions. First, we abstract the continuous system into a discrete-state model that captures noise by probabilistic transitions between states. We capture these bounds in the transition probability intervals of a so-called interval Markov decision process (iMDP)
  arXiv  Detail & Related papers  (2021-10-25T06:18:55Z)
• Probabilistic Gradient Boosting Machines for Large-Scale Probabilistic Regression [51.770998056563094]
  Probabilistic Gradient Boosting Machines (PGBM) is a method to create probabilistic predictions with a single ensemble of decision trees. We empirically demonstrate the advantages of PGBM compared to existing state-of-the-art methods.
  arXiv  Detail & Related papers  (2021-06-03T08:32:13Z)
• Stein Variational Model Predictive Control [130.60527864489168]
  Decision making under uncertainty is critical to real-world, autonomous systems. Model Predictive Control (MPC) methods have demonstrated favorable performance in practice, but remain limited when dealing with complex distributions. We show that this framework leads to successful planning in challenging, non optimal control problems.
  arXiv  Detail & Related papers  (2020-11-15T22:36:59Z)
• Density of States Estimation for Out-of-Distribution Detection [69.90130863160384]
  DoSE is the density of states estimator. We demonstrate DoSE's state-of-the-art performance against other unsupervised OOD detectors.
  arXiv  Detail & Related papers  (2020-06-16T16:06:25Z)

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.