Probabilistic model checking applied to autonomous spacecraft reconfiguration