Supermartingale Certificates for Parametric MDPs

• URL: http://arxiv.org/abs/2609.12715v1
• Date: Fri, 11 Sep 2026 11:10:49 GMT
• Title: Supermartingale Certificates for Parametric MDPs
• Abstract summary: We consider the problems of formal verification and synthesis in parametric Markov decision processes (MDPs) with general measurable state and action spaces.<n>The heart of our approach is a parameter flattening transformation, which allows us to transform parametric MDPs into semantically equivalent non-parametric MDPs.<n>We introduce the novel notion of parametric supermartingale certificates, which generalize traditional supermartingale certificates---used for non- MDPs---to the parametric setting.
• Score: 0.7734726150561088
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We consider the problems of formal verification and synthesis in parametric Markov decision processes (MDPs) with general measurable state and action spaces. The heart of our approach is a parameter flattening transformation, which allows us to transform parametric MDPs into semantically equivalent non-parametric MDPs. Building on this transformation, we introduce the novel notion of parametric supermartingale certificates, which generalize the traditional supermartingale certificates---used for non-parametric MDPs---to the parametric setting. We use our parametric supermartingale certificates to design algorithms for verification and approximate synthesis in polynomial arithmetic parametric MDPs. This leads to the first verification and synthesis algorithms for parametric MDPs with general state and action spaces. We implement our algorithms and experimentally evaluate them on several continuous parametric random walk benchmarks.

Related papers

• Symmetry-Twisted Multi-Entropies: Order Parameters for 2D SPT Phases [0.9558392439655014]
  We show that symmetry-protected topological phases (SPTs) can be distinguished by their entanglement properties.<n>We propose a pair of nonlocal order parameters that can detect and distinguish all bosonic SPTs in 2D protected by internal discrete, Abelian unitary symmetries.<n>Our results suggest multipartite entanglement to be a defining feature of SPTs.
  arXiv  Detail & Related papers  (2026-07-13T18:00:01Z)
• Robust Parameter Learning for Uncertain MDPs [55.60489406616378]
  Learning-based approaches to verifying unknown Markov decision processes (MDPs) often employ uncertain MDPs.<n>We propose to learn such models using parametric MDPs (pMDPs), where transition probabilities are expressions over a set of parameters.<n>We project statistical uncertainty from empirical transition frequencies onto the pMDP's parameter space, yielding a probably approximately correct (PAC) uncertainty model for the underlying MDP.
  arXiv  Detail & Related papers  (2026-05-02T09:22:05Z)
• Metrological symmetries in singular quantum multi-parameter estimation [0.0]
  We show that metrological symmetries appear in the Bayesian posterior distribution as lines of persistent likelihood running through the space of unknown parameters.<n>These lines are contour lines of the effective parameters which, through suitable parameter transformations, can be estimated and follow their own effective CRBs.
  arXiv  Detail & Related papers  (2025-03-07T14:52:40Z)
• Scaling Exponents Across Parameterizations and Optimizers [94.54718325264218]
  We propose a new perspective on parameterization by investigating a key assumption in prior work. Our empirical investigation includes tens of thousands of models trained with all combinations of threes. We find that the best learning rate scaling prescription would often have been excluded by the assumptions in prior work.
  arXiv  Detail & Related papers  (2024-07-08T12:32:51Z)
• Regularizing Towards Soft Equivariance Under Mixed Symmetries [23.603875905608565]
  We present a regularizer-based method for building a model for a dataset with mixed approximate symmetries. We show that our method achieves better accuracy than prior approaches while discovering the approximate symmetry levels correctly.
  arXiv  Detail & Related papers  (2023-06-01T05:33:41Z)
• PALT: Parameter-Lite Transfer of Language Models for Knowledge Graph Completion [108.8941541255567]
  This paper presents a parameter-lite transfer learning approach of pretrained language models (LM) for knowledge graph (KG) completion. Instead of finetuning, which modifies all LM parameters, we only tune a few new parameters while keeping the original LM parameters fixed. We show that, by tuning far fewer parameters than finetuning, LMs transfer non-trivially to most tasks and reach competitiveness with prior state-of-the-art approaches.
  arXiv  Detail & Related papers  (2022-10-25T02:22:29Z)
• E-detectors: a nonparametric framework for sequential change detection [86.15115654324488]
  We develop a fundamentally new and general framework for sequential change detection. Our procedures come with clean, nonasymptotic bounds on the average run length. We show how to design their mixtures in order to achieve both statistical and computational efficiency.
  arXiv  Detail & Related papers  (2022-03-07T17:25:02Z)
• Convex Optimization for Parameter Synthesis in MDPs [19.808494349302784]
  Probabilistic model checking aims to prove whether a Markov decision process satisfies a temporal logic specification. We develop two approaches that iteratively obtain locally optimal runtime solutions. We demonstrate the approaches on a satellite parameter synthesis problem with hundreds of thousands of parameters and their scalability on a wide range of commonly used benchmarks.
  arXiv  Detail & Related papers  (2021-06-30T21:23:56Z)
• Stochastic Gradient MCMC with Multi-Armed Bandit Tuning [2.2559617939136505]
  We propose a novel bandit-based algorithm that tunes SGMCMC hyperparameters to maximize the accuracy of the posterior approximation. We support our results with experiments on both simulated and real datasets, and find that this method is practical for a wide range of application areas.
  arXiv  Detail & Related papers  (2021-05-27T11:00:31Z)
• A Kernel-Based Approach to Non-Stationary Reinforcement Learning in Metric Spaces [53.47210316424326]
  KeRNS is an algorithm for episodic reinforcement learning in non-stationary Markov Decision Processes. We prove a regret bound that scales with the covering dimension of the state-action space and the total variation of the MDP with time.
  arXiv  Detail & Related papers  (2020-07-09T21:37:13Z)
• Meta-Learning Symmetries by Reparameterization [63.85144439337671]
  We present a method for learning and encoding equivariances into networks by learning corresponding parameter sharing patterns from data. Our experiments suggest that it can automatically learn to encode equivariances to common transformations used in image processing tasks.
  arXiv  Detail & Related papers  (2020-07-06T17:59:54Z)

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.