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 - Artefact - PEVA - 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 - Artefact - PEVA

From MaRDI portal
(Redirected from Dataset:6718574)



DOI10.5281/zenodo.14012421Zenodo14012421MaRDI QIDQ6718574

Dataset published at Zenodo repository.

Author name not available (Why is that?)

Publication date: 30 October 2024

Copyright license: No records found.



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.






This page was built for dataset: Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes - Artefact - PEVA