PAC Approximation and DIRECT Optimization for Parametric Markov Models
Authors: Zhiming Chi, Ying Liu, Andrea Turrini, Lijun Zhang, David N. Jansen
Organizations: Key Laboratory of System Software (Chinese Academy of Sciences), Beijing, China · Institute of Software, Chinese Academy of Sciences, Beijing, China · University of Chinese Academy of Sciences, Beijing, China · Institute of Optics and Electronics, Chinese Academy of Sciences, Chengdu, China · Institute of Intelligent Software Guangzhou, Guangzhou, China
Abstract
In this paper, we consider the parameter synthesis and optimization problem for parametric Markov decision processes (pMDPs), the extension of classical MDPs where exact probability values are replaced by parametric expressions. Computing the rational function f\lsf that maps parameter valuations to the satisfaction value of a PRCTL property \lsf is a computationally expensive task, particularly for pMDPs where the optimal policy may vary across the parameter space. We adopt the \emph{scenario approach} to efficiently synthesize a probably approximately correct (PAC) approximation \ApproxFunOfPropertyf of f\lsf: by sampling parameter configurations and solving a linear program, we obtain a polynomial approximation whose error margin \margin is guaranteed, with prescribed confidence, for all but an \errorRate-fraction of the parameter domain under the sampling distribution. We further show how this PAC framework can be combined with statistical model checking (SMC), enabling the analysis of black-box parametric models. Building on the PAC approximation, we integrate the DIRECT (DIviding RECTangles) algorithm for derivative-free global optimization over the parameter space. We establish conditional optimality-gap guarantees: under explicit Lipschitz and PAC-good-set assumptions, the difference between the true optimum f\lsf(\parameters∗) and the value found by DIRECT is bounded by a partition-diameter term and, in the PAC case, an additional approximation-error term. An empirical evaluation on 2997 benchmarks focuses on the new DIRECT-based optimization component. The results show that DIRECT variants solve fewer instances than the scenario optimizer, but on their common successful instances they often return slightly better objective values and usually run faster, while remaining close to the scenario values within the PAC margin.
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.
Learning-based approaches to verifying unknown Markov decision processes (MDPs) often employ uncertain MDPs. These models use, for example, confidence intervals to capture transition uncertainty and allow synthesis of policies that are robust to this uncertainty. However, this approach typically quantifies uncertainty independently for individual transition probabilities, ignoring dependencies due to shared latent quantities. We propose to learn such models using parametric MDPs (pMDPs), where transition probabilities are expressions over a set of parameters. 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 that respects the algebraic dependencies between transitions. The resulting models are algorithmically challenging to solve, so we propose a hierarchy of sound polytopic outer approximations of the induced confidence set. We implement and evaluate our approach, demonstrating substantially tighter uncertainty estimates than classical interval-based uncertain MDP learning techniques.
We present an optimization-based framework for robust permissive synthesis for Interval Markov Decision Processes (IMDPs). While robust IMDP controller synthesis typically yields a single policy and most permissive-synthesis methods assume exact transition models, we synthesize multi-strategies that retain multiple actions while guaranteeing satisfaction of probabilistic reachability or expected-reward specifications under all admissible transition probabilities. We formulate the problem as a mixed-integer linear program (MILP) that maximizes the number of enabled state--action pairs subject to robust Bellman constraints. We develop two encodings: a direct vertex-enumeration formulation and a dualization-based formulation that avoids explicit enumeration of uncertainty-polytope vertices and has size linear in the number of successor transitions. Experiments on four benchmark domains show that both encodings achieve the same optimal permissiveness and scale to IMDPs with hundreds of thousands of states. Compared with standard robust single-policy synthesis, the resulting multi-strategies retain substantially more action choices.