On the Complexity of Reachability in Parametric Markov Decision Processes

DOI10.4230/LIPIcs.CONCUR.2019.14OpenAlexW3099141145MaRDI QIDQ5875375

Sebastian Junges, Guillermo A. Pérez, Tobias Winkler, Joost-Pieter Katoen

Publication date: 3 February 2023

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

zbMATH Keywords

complexityformal verificationETRparametric Markov decision processes

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (1)

The complexity of reachability in parametric Markov decision processes

Uses Software

• PRISM
• Storm
• PROPhESY

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A survey of stochastic \(\omega \)-regular games
• Fixed points, Nash equilibria, and the existential theory of the reals
• Efficient solutions to factored MDPs with imprecise transition probabilities
• Parametric probabilistic transition systems for system design and analysis
• Representing polynomials by positive linear functions on compact convex polyhedra
• On the computational complexity and geometry of the first-order theory of the reals. I: Introduction. Preliminaries. The geometry of semi-algebraic sets. The decision problem for the existential theory of the reals
• Continuity of the value of competitive Markov decision processes
• Bounded-parameter Markov decision processes
• Qualitative reachability for open interval Markov chains
• On the complexity of model checking interval-valued discrete time Markov chains
• Parameter synthesis for Markov models: faster than ever
• Bayesian statistical parameter synthesis for linear temporal properties of stochastic models
• Reachability in augmented interval Markov chains
• Reachability analysis of uncertain systems using bounded-parameter Markov decision processes
• Precise parameter synthesis for stochastic biochemical systems
• Distributed probabilistic input/output automata: expressiveness, (un)decidability and algorithms
• Concurrent reachability games
• Realizability of Graphs and Linkages
• Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties
• Robustness of Structurally Equivalent Concurrent Parity Games
• On the Computational Complexity of Stochastic Controller Optimization in POMDPs
• Model Repair for Probabilistic Systems
• Perturbation Analysis in Verification of Discrete-Time Markov Chains
• Existence of p-Equilibrium and Optimal Stationary Strategies in Stochastic Games
• Robust Markov Decision Processes
• Robust Control of Markov Decision Processes with Uncertain Transition Matrices
• Discounted and positive stochastic games
• The Complexity of Decentralized Control of Markov Decision Processes
• Theoretical Aspects of Computing - ICTAC 2004
• Stochastic Games
• Tools and Algorithms for the Construction and Analysis of Systems
• Algorithms in real algebraic geometry
• Synthesis in pMDPs: a tale of 1001 parameters
• Accelerated model checking of parametric Markov chains

This page was built for publication: On the Complexity of Reachability in Parametric Markov Decision Processes