Convex Optimization for Parameter Synthesis in MDPs

• URL: http://arxiv.org/abs/2107.00108v1
• Date: Wed, 30 Jun 2021 21:23:56 GMT
• Title: Convex Optimization for Parameter Synthesis in MDPs
• Authors: Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, and Ufuk Topcu
• Abstract summary: 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.
• Score: 19.808494349302784
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Probabilistic model checking aims to prove whether a Markov decision process (MDP) satisfies a temporal logic specification. The underlying methods rely on an often unrealistic assumption that the MDP is precisely known. Consequently, parametric MDPs (pMDPs) extend MDPs with transition probabilities that are functions over unspecified parameters. The parameter synthesis problem is to compute an instantiation of these unspecified parameters such that the resulting MDP satisfies the temporal logic specification. We formulate the parameter synthesis problem as a quadratically constrained quadratic program (QCQP), which is nonconvex and is NP-hard to solve in general. We develop two approaches that iteratively obtain locally optimal solutions. The first approach exploits the so-called convex-concave procedure (CCP), and the second approach utilizes a sequential convex programming (SCP) method. The techniques improve the runtime and scalability by multiple orders of magnitude compared to black-box CCP and SCP by merging ideas from convex optimization and probabilistic model checking. We demonstrate the approaches on a satellite collision avoidance problem with hundreds of thousands of states and tens of thousands of parameters and their scalability on a wide range of commonly used benchmarks.

Related papers

• Synthesizing Tight Privacy and Accuracy Bounds via Weighted Model Counting [5.552645730505715]
  Two core challenges are finding expressive, compact, and efficient encodings of distributions of DP algorithms. We address the first challenge by developing a method for tight privacy and accuracy bound synthesis. We develop a framework for leveraging inherent symmetries in DP algorithms.
  arXiv  Detail & Related papers  (2024-02-26T19:29:46Z)
• Fast, Scalable, Warm-Start Semidefinite Programming with Spectral Bundling and Sketching [53.91395791840179]
  We present Unified Spectral Bundling with Sketching (USBS), a provably correct, fast and scalable algorithm for solving massive SDPs. USBS provides a 500x speed-up over the state-of-the-art scalable SDP solver on an instance with over 2 billion decision variables.
  arXiv  Detail & Related papers  (2023-12-19T02:27:22Z)
• QSlack: A slack-variable approach for variational quantum semi-definite programming [5.0579795245991495]
  Quantum computers could provide a speedup over the best known classical algorithms. We show how to solve optimization problems involving semi-definite and linear programs. We show that our implementations of both the primal and dual for these problems approach the ground truth.
  arXiv  Detail & Related papers  (2023-12-06T19:00:01Z)
• Numerical Methods for Convex Multistage Stochastic Optimization [86.45244607927732]
  We focus on optimisation programming (SP), Optimal Control (SOC) and Decision Processes (MDP) Recent progress in solving convex multistage Markov problems is based on cutting planes approximations of the cost-to-go functions of dynamic programming equations. Cutting plane type methods can handle multistage problems with a large number of stages, but a relatively smaller number of state (decision) variables.
  arXiv  Detail & Related papers  (2023-03-28T01:30:40Z)
• Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics [64.72260320446158]
  We propose a method for synthesising controllers for Markov jump linear systems. Our method is based on a finite-state abstraction that captures both the discrete (mode-jumping) and continuous (stochastic linear) behaviour of the MJLS. We apply our method to multiple realistic benchmark problems, in particular, a temperature control and an aerial vehicle delivery problem.
  arXiv  Detail & Related papers  (2022-12-01T17:36:30Z)
• Efficient semidefinite bounds for multi-label discrete graphical models [6.226454551201676]
  One of the main queries on such models is to identify the SDPWCSP Function on Cost of a Posteri (MAP) Networks. We consider a traditional dualized constraint approach and a dedicated dedicated SDP/Monteiro style method based on row-by-row updates.
  arXiv  Detail & Related papers  (2021-11-24T13:38:34Z)
• STRIDE along Spectrahedral Vertices for Solving Large-Scale Rank-One Semidefinite Relaxations [27.353023427198806]
  We consider solving high-order semidefinite programming relaxations of nonconstrained optimization problems (POPs) Existing approaches, which solve the SDP independently from the POP, either cannot scale to large problems or suffer from slow convergence due to the typical uneneracy of such SDPs. We propose a new algorithmic framework called SpecTrahedral vErtices (STRIDE)
  arXiv  Detail & Related papers  (2021-05-28T18:07:16Z)
• Two-Stage Stochastic Optimization via Primal-Dual Decomposition and Deep Unrolling [86.85697555068168]
  Two-stage algorithmic optimization plays a critical role in various engineering and scientific applications. There still lack efficient algorithms, especially when the long-term and short-term variables are coupled in the constraints. We show that PDD-SSCA can achieve superior performance over existing solutions.
  arXiv  Detail & Related papers  (2021-05-05T03:36:00Z)
• Parallel Stochastic Mirror Descent for MDPs [72.75921150912556]
  We consider the problem of learning the optimal policy for infinite-horizon Markov decision processes (MDPs) Some variant of Mirror Descent is proposed for convex programming problems with Lipschitz-continuous functionals. We analyze this algorithm in a general case and obtain an estimate of the convergence rate that does not accumulate errors during the operation of the method.
  arXiv  Detail & Related papers  (2021-02-27T19:28:39Z)
• Adaptive Sampling for Best Policy Identification in Markov Decision Processes [79.4957965474334]
  We investigate the problem of best-policy identification in discounted Markov Decision (MDPs) when the learner has access to a generative model. The advantages of state-of-the-art algorithms are discussed and illustrated.
  arXiv  Detail & Related papers  (2020-09-28T15:22:24Z)

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.