Analyzing Value Functions of States in Parametric Markov Chains

• URL: http://arxiv.org/abs/2504.17020v2
• Date: Sat, 26 Apr 2025 05:49:22 GMT
• Title: Analyzing Value Functions of States in Parametric Markov Chains
• Authors: Kasper Engelen, Guillermo A. Pérez, Shrisha Rao,
• Abstract summary: We first reduce monotonicity to asking whether the reachability probability from a given state is never less than that of another given state.<n>Recent results for the latter property imply an efficient algorithm to collapse same-value equivalence classes.<n>We show empirical evidence for the following: First, the collapse gives reductions in size for some existing benchmarks and significant reductions on some custom benchmarks.
• Score: 7.271205677308994
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Parametric Markov chains (pMC) are used to model probabilistic systems with unknown or partially known probabilities. Although (universal) pMC verification for reachability properties is known to be coETR-complete, there have been efforts to approach it using potentially easier-to-check properties such as asking whether the pMC is monotonic in certain parameters. In this paper, we first reduce monotonicity to asking whether the reachability probability from a given state is never less than that of another given state. Recent results for the latter property imply an efficient algorithm to collapse same-value equivalence classes, which in turn preserves verification results and monotonicity. We implement our algorithm to collapse "trivial" equivalence classes in the pMC and show empirical evidence for the following: First, the collapse gives reductions in size for some existing benchmarks and significant reductions on some custom benchmarks; Second, the collapse speeds up existing algorithms to check monotonicity and parameter lifting, and hence can be used as a fast pre-processing step in practice.

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)<n>The presented framework focuses on probabilistic reachability, which is a core problem in verification.
  arXiv  Detail & Related papers  (2024-03-14T08:54:19Z)
• Rethinking Classifier Re-Training in Long-Tailed Recognition: A Simple Logits Retargeting Approach [102.0769560460338]
  We develop a simple logits approach (LORT) without the requirement of prior knowledge of the number of samples per class. Our method achieves state-of-the-art performance on various imbalanced datasets, including CIFAR100-LT, ImageNet-LT, and iNaturalist 2018.
  arXiv  Detail & Related papers  (2024-03-01T03:27:08Z)
• Learning Hidden Markov Models When the Locations of Missing Observations are Unknown [54.40592050737724]
  We consider the general problem of learning an HMM from data with unknown missing observation locations. We provide reconstruction algorithms that do not require any assumptions about the structure of the underlying chain. We show that under proper specifications one can reconstruct the process dynamics as well as if the missing observations positions were known.
  arXiv  Detail & Related papers  (2022-03-12T22:40:43Z)
• Comparison of Markov chains via weak Poincar\'e inequalities with application to pseudo-marginal MCMC [0.0]
  We investigate the use of a certain class of functional inequalities known as weak Poincar'e inequalities to bound convergence of Markov chains to equilibrium. We show that this enables the derivation of subgeometric convergence bounds for methods such as the Independent Metropolis--Hastings sampler and pseudo-marginal methods for intractable likelihoods.
  arXiv  Detail & Related papers  (2021-12-10T15:36:30Z)
• 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)
• Incremental Verification of Fixed-Point Implementations of Neural Networks [0.19573380763700707]
  We develop and evaluate a novel symbolic verification framework using incremental bounded model checking (BMC), satisfiability modulo theories (SMT), and invariant inference. Our approach was able to verify and produce examples for 85.8% of 21 test cases considering different input images, and 100% of the properties related to covering methods.
  arXiv  Detail & Related papers  (2020-12-21T10:03:44Z)
• The Variational Method of Moments [65.91730154730905]
  conditional moment problem is a powerful formulation for describing structural causal parameters in terms of observables. Motivated by a variational minimax reformulation of OWGMM, we define a very general class of estimators for the conditional moment problem. We provide algorithms for valid statistical inference based on the same kind of variational reformulations.
  arXiv  Detail & Related papers  (2020-12-17T07:21:06Z)
• Understanding Implicit Regularization in Over-Parameterized Single Index Model [55.41685740015095]
  We design regularization-free algorithms for the high-dimensional single index model. We provide theoretical guarantees for the induced implicit regularization phenomenon.
  arXiv  Detail & Related papers  (2020-07-16T13:27:47Z)
• Recovering Joint Probability of Discrete Random Variables from Pairwise Marginals [22.77704627076251]
  Learning the joint probability of random variables (RVs) is the cornerstone of statistical signal processing and machine learning. Recent work has proposed to recover the joint probability mass function (PMF) of an arbitrary number of RVs from three-dimensional marginals. accurately estimating three-dimensional marginals can still be costly in terms of sample complexity. This work puts forth a new framework for learning the joint PMF using only pairwise marginals.
  arXiv  Detail & Related papers  (2020-06-30T15:43:44Z)
• Free Energy Wells and Overlap Gap Property in Sparse PCA [81.64027805404483]
  We study a variant of the sparse PCA (principal component analysis) problem in the "hard" regime. We show bounds on the depth of free energy wells for various Gibbs measures naturally associated to the problem. We prove that the Overlap Gap Property (OGP) holds in a significant part of the hard regime.
  arXiv  Detail & Related papers  (2020-06-18T17:18:02Z)
• Entropy Regularized Power k-Means Clustering [21.013169939337583]
  We propose a scalable majorization-minimization algorithm that enjoys closed-form updates and convergence guarantees. Our method retains the same computational complexity of $k$-means and power $k$-means, but yields significant improvements over both.
  arXiv  Detail & Related papers  (2020-01-10T14:05:44Z)

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.