Synthesis in pMDPs: A Tale of 1001 Parameters
This work addresses the challenge of parameter synthesis in pMDPs for verification and control applications, representing an incremental improvement by applying existing optimization techniques to scale up the problem.
The paper tackles the synthesis problem for parametric Markov decision processes (pMDPs) by formulating it as a quadratically-constrained quadratic program (QCQP) and using a convex-concave procedure (CCP) to find local optima, enabling solution for models with thousands of parameters as demonstrated in the tool PROPhESY.
This paper considers parametric Markov decision processes (pMDPs) whose transitions are equipped with affine functions over a finite set of parameters. The synthesis problem is to find a parameter valuation such that the instantiated pMDP satisfies a specification under all strategies. We show that this problem can be formulated as a quadratically-constrained quadratic program (QCQP) and is non-convex in general. To deal with the NP-hardness of such problems, we exploit a convex-concave procedure (CCP) to iteratively obtain local optima. An appropriate interplay between CCP solvers and probabilistic model checkers creates a procedure --- realized in the open-source tool PROPhESY --- that solves the synthesis problem for models with thousands of parameters.