Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes - QEST 2024 Artefact
DOI10.5281/zenodo.12513996Zenodo12513996MaRDI QIDQ6718570FDOQ6718570
Dataset published at Zenodo repository.
Calvin Chau, Sascha Klüppelholz, Christel Baier
Publication date: 24 June 2024
Copyright license: Creative Commons Attribution 4.0 International
This artifact accompanies the QEST+FORMATS 2024 paper "Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes" (arXiv). 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 results presented in Section 5 and Appendix D. Additionally, it also contains the original raw experimental data presented in Section 5 and Appendix D 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 1 and Example 2- Table 1 in Section 5- Table 3 in Appendix D- Figure 5 in Appendix D- Figure 6 in Appendix D- Table 4 in Appendix D Aritfact 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 5 and Appendix D. 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.- qest-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. Note on the versions: The first version (v1) contains the data and implementation at the point of the paper submission. The second version (v2) contains a Docker image and more detailed documentation and was evaluated by the QEST+FORMATS 2024 Artifact Evaluation Comittee and awarded the artifact evaluation badge. This version (v3) incorporates the feedback of the QEST+FORMATS 2024 artifact evaluation and contains improvements on the second version (v2). Acknowledgments: We would like to thank the anonymous reviewers in the QEST+FORMATS Artifact Evaluation Committee for their valuable feedback. The authors were supported by the German Federal Ministry of Education and Research (BMBF) within the project SEMECO Q1 (03ZU1210AG) and by the German Research Foundation (DFG) through the Cluster of Excellence EXC 2050/1 (CeTI, project ID 390696704, as part of Germanys Excellence Strategy) and the DFG Grant 389792660 as part of TRR 248 (Foundations of Perspicuous Software System).
This page was built for dataset: Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes - QEST 2024 Artefact
