Graph-Based Reductions for Parametric and Weighted MDPs
This work addresses computational complexity and efficiency issues for researchers and practitioners analyzing large parametric and weighted Markov decision processes, though it is incremental in nature.
The paper tackles the problem of determining when one state is never worse than another in parametric and weighted Markov decision processes, establishing coETR-completeness for this decision problem and providing a polynomial-time algorithm for Markov chains, along with efficient preprocessing rules for large MDPs.
We study the complexity of reductions for weighted reachability in parametric Markov decision processes. That is, we say a state p is never worse than q if for all valuations of the polynomial indeterminates it is the case that the maximal expected weight that can be reached from p is greater than the same value from q. In terms of computational complexity, we establish that determining whether p is never worse than q is coETR-complete. On the positive side, we give a polynomial-time algorithm to compute the equivalence classes of the order we study for Markov chains. Additionally, we describe and implement two inference rules to under-approximate the never-worse relation and empirically show that it can be used as an efficient preprocessing step for the analysis of large Markov decision processes.