Sequential convex programming for the efficient verification of parametric MDPs

Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost Pieter Katoen, Ivan Papusha, Hasan A. Poonawala, Ufuk Topcu

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

19 Scopus citations

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.

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings
EditorsTiziana Margaria, Axel Legay
Pages133-150
Number of pages18
DOIs
StatePublished - 2017
Event23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017 - Uppsala, Sweden
Duration: Apr 22 2017Apr 29 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10206 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017
Country/TerritorySweden
City Uppsala
Period4/22/174/29/17

Bibliographical note

Funding Information:
Partly funded by the awards AFRL # FA8650-15-C-2546, DARPA # W911NF-16-1-0001, ARO # W911NF-15-1-0592, ONR # N00014-15-IP-00052, ONR # N00014-16-1-3165, and NSF # 1550212. Also funded by the Excellence Initiative of the German federal and state government and the CDZ project CAP (GZ 1023).

Publisher Copyright:
© Springer-Verlag GmbH Germany 2017.

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science (all)

Fingerprint

Dive into the research topics of 'Sequential convex programming for the efficient verification of parametric MDPs'. Together they form a unique fingerprint.

Cite this