Convex Optimization for Parameter Synthesis in MDPs

IEEE Transactions on Automatic Control, vol. 67, pp. 6333–6348

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, 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.

Authors 5

1. Murat Cubuktepe

   The University of Texas at Austin

   Affiliation as printed

   Department of Aerospace Engineering and Engineering Mechanics, University of Texas at Austin, Austin, TX, USA

   University of Texas at Austin

2. Nils Jansen

   Radboud University Nijmegen · The University of Texas at Austin

   Affiliation as printed

   Institute for Computing and Information Science, Radboud University Nijmegen, Nijmegen, The Netherlands

   University of Texas at Austin

3. Sebastian Junges

   Radboud University Nijmegen

   Affiliation as printed

   Institute for Computing and Information Science, Radboud University Nijmegen, Nijmegen, The Netherlands

   Radboud University Nijmegen

4. Joost-Pieter Katoen Aachen Departement of Computer Science

   RWTH Aachen University · University of California, Berkeley

   Affiliation as printed

   Departement of Computer Science, RWTH Aachen University, Aachen, Germany

   University of California–Berkeley

5. Ufuk Topcu Aachen

   The University of Texas at Austin · RWTH Aachen University

   Affiliation as printed

   Department of Aerospace Engineering and Engineering Mechanics, University of Texas at Austin, Austin, TX, USA

   RWTH Aachen University