Synthesis in pMDPs: A Tale of 1001 Parameters

TL;DR

This paper introduces a novel approach for parameter synthesis in parametric Markov decision processes by formulating the problem as a QCQP and solving it iteratively with CCP, enabling handling of models with thousands of parameters.

Contribution

It presents a new formulation of pMDP synthesis as a QCQP and develops an iterative CCP-based method implemented in PROPhESY for large-scale models.

Findings

Successfully solves synthesis problems with thousands of parameters.

Provides a practical iterative method for non-convex QCQPs.

Demonstrates effectiveness through implementation in an open-source tool.

Abstract

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.