Sequential convex programming for the efficient verification of parametric MDPs

DOI10.1007/978-3-662-54580-5_8MaRDI QIDQ3303926zbMATH OpenOpenAlexFDO

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

Publication date 5 August 2020

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1702.00063

Mathematics Subject Classification ID

Convex programming (90C25) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60)

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

Recommendations

• Synthesis in pMDPs: a tale of 1001 parameters
• Parameter synthesis for Markov models: faster than ever
• Polynomial-time verification of PCTL properties of MDPs with convex uncertainties
• Scenario-based verification of uncertain MDPs
• Multi-Objective Model Checking of Markov Decision Processes

Cites work

• scientific article; zbMATH DE number 1818892 (Why is no real title available?)
• scientific article; zbMATH DE number 3614066 (Why is no real title available?)
• scientific article; zbMATH DE number 2107836 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A tutorial on geometric programming
• Fast randomized consensus using shared memory
• Global optimization with polynomials and the problem of moments
• Markovian Decision Processes with Uncertain Transition Probabilities
• Model repair for probabilistic systems
• Multi-objective Model Checking of Markov Decision Processes
• Nested Reachability Approximation for Discrete-Time Markov Chains with Univariate Parameters
• Parameter synthesis for Markov models: faster than ever
• Pareto curves for probabilistic model checking
• Polynomial-time verification of PCTL properties of MDPs with convex uncertainties
• Precise parameter synthesis for stochastic biochemical systems
• Quantitative multi-objective verification for probabilistic systems
• Real-time dynamic programming for Markov decision processes with imprecise probabilities
• Smoothed model checking for uncertain continuous-time Markov chains
• Solving non-linear arithmetic
• The probabilistic model checking landscape

Cited in

(12)

• Parameter synthesis for Markov models: covering the parameter space
• Synthesis in pMDPs: a tale of 1001 parameters
• Interval Markov decision processes with multiple objectives: from robust strategies to Pareto curves
• Finding provably optimal Markov chains
• Scenario-based verification of uncertain MDPs
• SEA-PARAM: exploring schedulers in parametric MDPs
• Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination
• Fine-tuning the odds in Bayesian networks
• Gradient-descent for randomized controllers under partial observability
• Parameter-Independent Strategies for pMDPs via POMDPs
• Parameter synthesis in Markov models: a gentle survey
• A practitioner's guide to MDP model checking algorithms

Describes a project that uses

Uses Software

• iscasMc
• PROPhESY
• Prophet
• Storm
• PARAM
• Ipopt
• Mosek
• PRISM

This page was built for publication: Sequential convex programming for the efficient verification of parametric MDPs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3303926)