Symbolic Computation of Maximal Probabilistic Reachability