Proactive latency-aware adaptation is an approach for self-adaptive systems that improves over reactive adaptation by considering both the current and anticipated adaptation needs of the system, and taking into account the latency of adaptation tactics so that they can be started with the necessary lead time. Making an adaptation decision with these characteristics requires solving an optimization problem to select the adaptation path that maximizes an objective function over a finite look-ahead horizon. Since this is a problem of selecting adaptation actions in the context of the probabilistic behavior of the environment, Markov decision processes (MDP) are a suitable approach. However, given all the possible interactions between the different and possibly concurrent adaptation tactics, the system, and the environment, constructing the MDP is a complex task. Probabilistic model checking can be used to deal with this problem since it takes as input a formal specification of the stochastic system, which is internally translated into an MDP, and solved. One drawback of this solution is that the MDP has to be constructed every time an adaptation decision has to be made to incorporate the latest predictions of the environment behavior. In this paper we present an approach that eliminates that run-time overhead by constructing most of the MDP offline, also using formal specification. At run time, the adaptation decision is made by solving the MDP through stochastic dynamic programming, weaving in the stochastic environment model as the solution is computed. Our experimental results show that this approach reduces the adaptation decision time by an order of magnitude compared to the probabilistic model checking approach, while producing the same results.