Sequential Convex Programming for the Efficient Verification of Parametric MDPs

DOI10.1007/978-3-662-54580-5_8zbMath1452.68117arXiv1702.00063OpenAlexW2587263590MaRDI QIDQ3303926

Ufuk Topcu, Nils Jansen, Ivan Papusha, Hasan A. Poonawala, Sebastian Junges, Murat Cubuktepe, 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) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (7)

Scenario-Based Verification of Uncertain MDPs ⋮ Fine-tuning the odds in Bayesian networks ⋮ Gradient-descent for randomized controllers under partial observability ⋮ Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination ⋮ Parameter-Independent Strategies for pMDPs via POMDPs ⋮ Parameter synthesis in Markov models: a gentle survey ⋮ Finding provably optimal Markov chains

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Smoothed model checking for uncertain continuous-time Markov chains
• Real-time dynamic programming for Markov decision processes with imprecise probabilities
• A tutorial on geometric programming
• Parameter synthesis for Markov models: faster than ever
• Precise parameter synthesis for stochastic biochemical systems
• Global Optimization with Polynomials and the Problem of Moments
• Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties
• Solving Non-linear Arithmetic
• Quantitative Multi-objective Verification for Probabilistic Systems
• Model Repair for Probabilistic Systems
• Nested Reachability Approximation for Discrete-Time Markov Chains with Univariate Parameters
• Fast randomized consensus using shared memory
• The Probabilistic Model Checking Landscape
• Pareto Curves for Probabilistic Model Checking
• Markovian Decision Processes with Uncertain Transition Probabilities
• Multi-objective Model Checking of Markov Decision Processes

This page was built for publication: Sequential Convex Programming for the Efficient Verification of Parametric MDPs