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

doi:10.1007/978-3-662-54580-5_8

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

Mechanical and Aerospace Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

25 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 language	English
Title of host publication	Tools 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
Editors	Tiziana Margaria, Axel Legay
Pages	133-150
Number of pages	18
DOIs	https://doi.org/10.1007/978-3-662-54580-5_8
State	Published - 2017
Event	23rd 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 2017 → Apr 29 2017

Publication series

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

Conference

Conference	23rd 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/Territory	Sweden
City	Uppsala
Period	4/22/17 → 4/29/17

Bibliographical note

Publisher Copyright:
© Springer-Verlag GmbH Germany 2017.

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-662-54580-5_8

Cite this

Cubuktepe, M., Jansen, N., Junges, S., Katoen, J. P., Papusha, I., Poonawala, H. A., & Topcu, U. (2017). Sequential convex programming for the efficient verification of parametric MDPs. In T. Margaria, & A. Legay (Eds.), Tools 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 (pp. 133-150). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10206 LNCS). https://doi.org/10.1007/978-3-662-54580-5_8

Cubuktepe, Murat ; Jansen, Nils ; Junges, Sebastian et al. / Sequential convex programming for the efficient verification of parametric MDPs. Tools 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. editor / Tiziana Margaria ; Axel Legay. 2017. pp. 133-150 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{5fa4dc6212b9430084c630241a5f4aed,

title = "Sequential convex programming for the efficient verification of parametric MDPs",

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.",

author = "Murat Cubuktepe and Nils Jansen and Sebastian Junges and Katoen, {Joost Pieter} and Ivan Papusha and Poonawala, {Hasan A.} and Ufuk Topcu",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag GmbH Germany 2017.; 23rd 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 ; Conference date: 22-04-2017 Through 29-04-2017",

year = "2017",

doi = "10.1007/978-3-662-54580-5_8",

language = "English",

isbn = "9783662545799",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "133--150",

editor = "Tiziana Margaria and Axel Legay",

booktitle = "Tools 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",

}

Cubuktepe, M, Jansen, N, Junges, S, Katoen, JP, Papusha, I, Poonawala, HA & Topcu, U 2017, Sequential convex programming for the efficient verification of parametric MDPs. in T Margaria & A Legay (eds), Tools 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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10206 LNCS, pp. 133-150, 23rd 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, 4/22/17. https://doi.org/10.1007/978-3-662-54580-5_8

Sequential convex programming for the efficient verification of parametric MDPs. / Cubuktepe, Murat; Jansen, Nils; Junges, Sebastian et al.
Tools 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. ed. / Tiziana Margaria; Axel Legay. 2017. p. 133-150 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10206 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Sequential convex programming for the efficient verification of parametric MDPs

AU - Cubuktepe, Murat

AU - Jansen, Nils

AU - Junges, Sebastian

AU - Katoen, Joost Pieter

AU - Papusha, Ivan

AU - Poonawala, Hasan A.

AU - Topcu, Ufuk

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85017497733&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85017497733&partnerID=8YFLogxK

U2 - 10.1007/978-3-662-54580-5_8

DO - 10.1007/978-3-662-54580-5_8

M3 - Conference contribution

AN - SCOPUS:85017497733

SN - 9783662545799

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 133

EP - 150

BT - Tools 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

A2 - Margaria, Tiziana

A2 - Legay, Axel

T2 - 23rd 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

Y2 - 22 April 2017 through 29 April 2017

ER -

Cubuktepe M, Jansen N, Junges S, Katoen JP, Papusha I, Poonawala HA et al. Sequential convex programming for the efficient verification of parametric MDPs. In Margaria T, Legay A, editors, Tools 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. 2017. p. 133-150. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-662-54580-5_8

Sequential convex programming for the efficient verification of parametric MDPs

Abstract

Publication series

Conference

Bibliographical note

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this