Abstraction Framework for Markov Decision Processes and PCTL via Games - Kattenbelt, M; Huth, M (Oxford University Computing Laboratory, 2009)