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

This artefact allows to review and replicate the experiments from the TACAS'23 paper <strong>A Practitioner's Guide to MDP Model Checking Algorithms</strong>. 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.本科研工件可用于审阅并复现发表于TACAS'23的论文《马尔可夫决策过程（Markov Decision Process，MDP）模型检验算法从业者指南》（A Practitioner's Guide to MDP Model Checking Algorithms）中的实验。本工件包含所有原始日志文件，以及用于从日志中提取相关数据以复现论文中图表的脚本。此外，本工件还附带了模型检验工具Storm、mcsta及其依赖项、便捷安装脚本，以及全部基准测试用例。针对因授权限制无法纳入本工件的线性规划（Linear Programming，LP）求解器，我们提供了安装指引。使用者可借此复现论文中的所有实验。为便于及时完成审阅，我们提供了适量的实验子集。此外，使用者也可手动挑选单个实验进行复现。