This page is devoted to the paper: "Evaluating Probabilistic Model Checking Tools for Verification of Robot Control Policies" by Shashank Pathak, Luca Pulina and Armando Tacchella.
Here you may download problem instances for the experiments presented in the paper. Different encondings are available for the model checkers COMICS, PRISM and MRMC.
Caution! These files are large (approx. 1GB). Downloading without a fast connection might require a long time.