A game-based abstraction-refinement framework for Markov decision processes