Greatest fixed points of probabilistic min/max polynomial equations, and reachability for branching Markov decision processes

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.