2026-07-21T03:11:33Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10916 2024-03-06T10:47:11Z ddc:004 open_access

On the Complexity of Reachability in Parametric Markov Decision Processes Winkler, Tobias Junges, Sebastian Pérez, Guillermo A. Katoen, Joost-Pieter Parametric Markov decision processes Formal verification ETR Complexity 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Tobias Winkler and Sebastian Junges and Guillermo A. Pérez and Joost-Pieter Katoen 2019 Is Part Of LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2019.14 urn:nbn:de:0030-drops-109162 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.14 eng https://creativecommons.org/licenses/by/3.0/legalcode