Verification and synthesis problems of parametric Markov decision processes can be naturally expressed as nonlinear programs. Our results are based on two key insights.

First, we first observe that many of these computationally demanding problems belong to the subclass of signomial programs. Second, we show how the nonlinear program can be formulated as a quadratically-constrained quadratic program (QCQP) and is non-convex in general.

The first insight allows for a sequential optimization algorithm to efficiently compute sound but possibly suboptimal solutions. Each stage of this algorithm solves a convexified version of the original problem.

The second insight allows to exploit a convex-concave procedure (CCP) to iteratively obtain local optima. An appropriate interplay between convex optimization solvers and probabilistic model checkers creates a procedure — realized in the tool PROPheSY — that is the first to solve the synthesis problem for well-known benchmarks with thousands of parameters.

Moreover, employing these scalability improvements, we establish and demonstrate the applicability of parameter synthesis to strategy computation for partially observable Markov decision processes.