A Practitioner's Guide to MDP Model Checking Algorithms (Artefact)

This artefact allows to review and replicate the experiments from the TACAS'23 paper A Practitioner's Guide to MDP Model Checking Algorithms. The package contains all original logfiles and the scripts that extract the relevant data from those logs to generate the plots as in the paper. Furthermore, the artefact contains the model checking tools `Storm` and `mcsta` with their dependencies and convenient installation scripts as well as all benchmark instances. We provide installation instructions for those LP solvers that, due to licensing reasons, could not be included in this artefact. The user can thus replicate all experiments from the paper. An appropriate subset of the experiments is given to allow a review in a timely manner. In addition, single experiments can be handpicked for replication.