On the Complexity of Reachability in Parametric Markov Decision Processes

2019/04/02 by Tobias Winkler, Sebastian Junges, Winkler, Tobias +5
Computer Science · #Bayesian Modeling and Causal Inference #Computational Complexity (cs.CC) #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1904.01503

openalex publication_date 2019/04/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

This paper studies parametric Markov decision processes (pMDPs), an extension to Markov decision processes (MDPs) where transitions probabilities are described by polynomials over a finite set of parameters. Fixing values for all parameters yields MDPs. In particular, this paper studies the complexity of finding values for these parameters such that the induced MDP satisfies some reachability constraints. We discuss different variants depending on the comparison operator in the constraints and the domain of the parameter values. We improve all known lower bounds for this problem, and notably provide ETR-completeness results for distinct variants of this problem. Furthermore, we provide insights in the functions describing the induced reachability probabilities, and how pMDPs generalise concurrent stochastic reachability games.

Related

• The Complexity of Reachability in Parametric Markov Decision Processes
• Graph-Based Reductions for Parametric and Weighted MDPs
• Structured Reachability Analysis for Markov Decision Processes
• Greatest Fixed Points of Probabilistic Min/Max Polynomial Equations, and\n Reachability for Branching Markov Decision Processes
• Anytime Guarantees for Reachability in Uncountable Markov Decision Processes