Greatest fixed points of probabilistic min/max polynomial equations, and reachability for branching Markov decision processes
Information and Computation(2018)
摘要
We give polynomial time algorithms for quantitative (and qualitative) reachability analysis for Branching Markov Decision Processes (BMDPs). Specifically, given a BMDP, and given an initial population, where the objective of the controller is to maximize (or minimize) the probability of eventually reaching a population that contains an object of a desired (or undesired) type, we give algorithms for approximating the supremum (infimum) reachability probability, within desired precision ϵ>0, in time polynomial in the encoding size of the BMDP and in log(1/ϵ). We furthermore give P-time algorithms for computing ϵ-optimal strategies for both maximization and minimization of reachability probabilities. We also give P-time algorithms for all associated qualitative analysis problems, namely: deciding whether the optimal (supremum or infimum) reachability probabilities are 0 or 1. Prior to this paper, approximation of optimal reachability probabilities for BMDPs was not even known to be decidable.Our algorithms exploit the following basic fact: we show that for any BMDP, its maximum (minimum) non-reachability probabilities are given by the greatest fixed point (GFP) solution g⁎∈[0,1]n of a corresponding monotone max (min) Probabilistic Polynomial System of equations (max/minPPS), x=P(x), which are the Bellman optimality equations for a BMDP with non-reachability objectives. We show how to compute the GFP of max/minPPSs to desired precision in P-time.We also study more general branching simple stochastic games (BSSGs) with (non-)reachability objectives. We show that: (1) the value of these games is captured by the GFP, g⁎, of a corresponding max-minPPS, x=P(x); (2) the quantitative problem of approximating the value is in TFNP; and (3) the qualitative problems associated with the value are all solvable in P-time.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要