Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes - Artefact - PEVA

SummaryThis artifact accompanies the PEVA submission "Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes". It contains the implementation (switss-multi) of the presented techniques, that is, the computation of certificates, witnessing subsystems and schedulers for multi-objective queries in MDPs. Further, the artifact contains the PRISM models, PRISM properties and scripts bundled in a Docker image for completely reproducing the experimental results presented in Section 6. Additionally, it also contains the original raw experimental data presented in Section 6 and the corresponding analysis scripts. Lastly, we provide a documentation of our implementation switss-multi and describe how to use our tool via its command-line and programmatically via its Python interface. Relation to paperThis artifact can be used to reproduce all the experimental results (including examples) presented in the paper, that is:- The toy examples presented in Example 10 and Example 12- Table 3 in Section 6- Table 4 in Section 6- Table 5 in Section 6- Table 8 in Section 6- Table 9 in Section 6- Figure 5 in Section 6- Figure 6 in Section 6 StructureThis artifact consists of the following files and folders:- data: Contains the PRISM models, PRISM properties (queries) and original raw experimental data presented in Section 6. Additionally, the log files and scripts for summarizing the raw experimental data are provided.- switss-multi: The source code of the implementation of our presented techniques.- switss-multi-docs: A documentation of the Python API of switss-multi.- peva-docker-image.tar.gz: The compressed Docker image, with the installed implementation (switss-multi), PRISM models, PRISM properties and the scripts for running the experiments and analysing the raw experimental data. Moreover, it contains a copy of the data folder, in case you want to run the analysis scripts on the original data.- docker-results: An empty folder that will be populated with results when running the experiments and analysis with the provided Docker image.- LICENSE: The license of this artifact (MIT license).- GUROBI-EULA: The end-user license agreement of Gurobi (also see https://pypi.org/project/gurobipy/).- GPL-3.0: The GPL 3.0 license. It is included because our dependency Storm (https://www.stormchecker.org) is licensed under it.摘要 本科研配套工件对应PEVA投稿论文《Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes》（《马尔可夫决策过程多目标查询的证书与见证系统》）。本工件包含本文所提技术的实现代码（switss-multi），可针对马尔可夫决策过程（Markov Decision Processes，下文简称MDPs）的多目标查询，计算对应证书、见证子系统与调度器。此外，本工件还包含打包为Docker镜像（Docker image）的PRISM模型、PRISM属性文件与脚本，可完全复现第6章中展示的全部实验结果。同时，本工件还收录了第6章中展示的原始实验数据与对应的分析脚本。最后，本工件提供了switss-multi实现的官方文档，并说明了如何通过命令行与Python编程接口使用该工具。 与论文的关联 本配套工件可复现论文中展示的全部实验结果（含所有示例），具体包括： - 示例10与示例12中的玩具示例 - 第6章的表3、表4、表5、表8、表9 - 第6章的图5、图6 工件结构 本配套工件包含以下文件与文件夹： - `data`：收录第6章中展示的PRISM模型、PRISM属性查询文件与原始实验数据，同时提供了用于汇总原始实验数据的日志文件与脚本。 - `switss-multi`：本文所提技术的实现源代码。 - `switss-multi-docs`：switss-multi的Python应用程序编程接口（Application Programming Interface，下文简称API）文档。 - `peva-docker-image.tar.gz`：压缩格式的Docker镜像，其中预装了switss-multi实现、PRISM模型、PRISM属性文件，以及用于运行实验与分析原始实验数据的脚本。该镜像附带一份`data`文件夹副本，方便用户基于原始数据运行分析脚本。 - `docker-results`：空文件夹，使用提供的Docker镜像运行实验与分析时，生成的结果将写入该文件夹。 - `LICENSE`：本配套工件的MIT许可证（MIT license）。 - `GUROBI-EULA`：Gurobi的最终用户许可协议（End-User License Agreement，EULA，可参考https://pypi.org/project/gurobipy/）。 - `GPL-3.0`：GNU通用公共许可证第3.0版（GNU General Public License v3.0），因本工件依赖Storm（https://www.stormchecker.org），故包含该许可证文本。