Sequential Convex Programming for the Efficient Verification of Parametric MDPs
Nils Jansen, UT Austin
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 programs are model repair and parameter synthesis. We demonstrate the scalability and quality of our approach by well-known benchmarks.
Bio:
Nils Jansen obtained his PhD in Computer Science with Erika Abraham and Joost-Pieter Katoen at RWTH Aachen University in Germany. After that, he hold postdoctoral positions at RWTH Aachen University and at the University of Texas at Austin. For his PhD thesis, he received the Borchers Badge of RWTH Aachen University. In 2017, he became a research associate with Ufuk Topcu at the University of Texas at Austin.

His research focuses on formal methods and verification with applications in machine learning, robotics, and optimal control.