Convex Optimization for Parameter Synthesis in MDPs
From MaRDI portal
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.
Cited in
(9)- Using Convex Switching Techniques for Partially Observable Decision Processes
- Technical Note—On the Convexity of Policy Regions in Partially Observed Systems
- Maximizing the set of recurrent states of an MDP subject to convex constraints
- \textsf{PFL}: a probabilistic logic for fault trees
- Automatically finding the right probabilities in Bayesian networks
- Robust almost-sure reachability in multi-environment MDPs
- Efficient sensitivity analysis for parametric robust Markov chains
- Parameter synthesis for Markov models: covering the parameter space
- A PSPACE algorithm for almost-sure rabin objectives in multi-environment MDPs
This page was built for publication: Convex Optimization for Parameter Synthesis in MDPs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6053142)
