Deprecated: $wgMWOAuthSharedUserIDs=false is deprecated, set $wgMWOAuthSharedUserIDs=true, $wgMWOAuthSharedUserSource='local' instead [Called from MediaWiki\HookContainer\HookContainer::run in /var/www/html/w/includes/HookContainer/HookContainer.php at line 135] in /var/www/html/w/includes/Debug/MWDebug.php on line 372

Notice: Unexpected clearActionName after getActionName already called in /var/www/html/w/includes/Context/RequestContext.php on line 321
Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes - QEST 2024 Artefact - MaRDI portal

Deprecated: Use of MediaWiki\Skin\SkinTemplate::injectLegacyMenusIntoPersonalTools was deprecated in Please make sure Skin option menus contains `user-menu` (and possibly `notifications`, `user-interface-preferences`, `user-page`) 1.46. [Called from MediaWiki\Skin\SkinTemplate::getPortletsTemplateData in /var/www/html/w/includes/Skin/SkinTemplate.php at line 691] in /var/www/html/w/includes/Debug/MWDebug.php on line 372

Deprecated: Use of MediaWiki\Skin\BaseTemplate::getPersonalTools was deprecated in 1.46 Call $this->getSkin()->getPersonalToolsForMakeListItem instead (T422975). [Called from Skins\Chameleon\Components\NavbarHorizontal\PersonalTools::getHtml in /var/www/html/w/skins/chameleon/src/Components/NavbarHorizontal/PersonalTools.php at line 66] in /var/www/html/w/includes/Debug/MWDebug.php on line 372

Deprecated: Use of QuickTemplate::(get/html/text/haveData) with parameter `personal_urls` was deprecated in MediaWiki Use content_navigation instead. [Called from MediaWiki\Skin\QuickTemplate::get in /var/www/html/w/includes/Skin/QuickTemplate.php at line 131] in /var/www/html/w/includes/Debug/MWDebug.php on line 372

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

From MaRDI portal
(Redirected from Dataset:6718570)



DOI10.5281/zenodo.12513996Zenodo12513996MaRDI QIDQ6718570

Dataset published at Zenodo repository.

Author name not available (Why is that?)

Publication date: 24 June 2024

Copyright license: No records found.



Description

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

Retrieved from "https://mardi.schubotz.org/w/index.php?title=Certificates_and_Witnesses_for_Multi-Objective_Queries_in_Markov_Decision_Processes_-_QEST_2024_Artefact&oldid=44852611"
Powered by MediaWiki