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

University of Twente Research Information

Abstract

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.

Authors 4

1. Arnd Hartmanns

   University of Twente

   Affiliation as printed

   University of Twente, Enschede, The Netherlands

2. Sebastian Junges

   Radboud University Nijmegen

   Affiliation as printed

   Radboud University, Nijmegen, The Netherlands

3. Tim Quatmann Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

4. Maximilian Weininger

   Technical University of Munich

   Affiliation as printed

   Technical University of Munich, Munich, Germany