Name
Abstract | ||
|---|---|---|
This article presents the complexity of reachability decision problems for 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. In particular, we study the complexity of finding values for these parameters such that the induced MDP satisfies some maximal or minimal reachability probability 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. |
Year | DOI | Venue |
|---|---|---|
2021 | 10.1016/j.jcss.2021.02.006 | Journal of Computer and System Sciences |
Keywords | DocType | Volume |
Parametric Markov decision processes,Formal verification,Existential theory of the reals,Computational complexity,Parameter synthesis | Journal | 119 |
ISSN | Citations | PageRank |
0022-0000 | 1 | 0.35 |
References | Authors | |
30 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sebastian Junges | 1 | 184 | 20.78 |
| Joost-Pieter Katoen | 2 | 4444 | 289.65 |
| Guillermo A. Pérez | 3 | 10 | 9.32 |
| Tobias Winkler | 4 | 1 | 1.36 |