smc4mdp is an implementation of the statistical model checking technique for Markov Decision Processes presented in our QEST 2012 paper [pdf]. The technique is implemented within the well-known Prism probabilistic model checker - basically, this means that you can (statistically) model check any Prism MDP model.

Here are source code and models. The authors are João Martins and David Henriques.