Sequential Convex Programming for the Efficient Verification of Parametric MDPs

TL;DR

This paper introduces a sequential convex programming method to efficiently verify parametric Markov decision processes by transforming complex nonlinear problems into a series of geometric programs, improving scalability and solution quality.

Contribution

The paper presents a novel sequential optimization algorithm that convexifies signomial programs for parametric MDP verification, enabling efficient and scalable solutions.

Findings

Effective in handling well-known benchmarks

Produces sound but possibly suboptimal solutions

Demonstrates scalability and quality of results

Abstract

Multi-objective verification problems of parametric Markov decision processes under optimality criteria can be naturally expressed as nonlinear programs. We observe that many of these computationally demanding problems belong to the subclass of signomial programs. This insight allows for a sequential optimization algorithm to efficiently compute sound but possibly suboptimal solutions. Each stage of this algorithm solves a geometric programming problem. These geometric programs are obtained by convexifying the nonconvex constraints of the original problem. Direct applications of the encodings as nonlinear pro- grams are model repair and parameter synthesis. We demonstrate the scalability and quality of our approach by well-known benchmarks