Optimal planning for architecture-based self-adaptation via model checking of stochastic games