Find research datasets worth reusing
Search datasets from major research repositories and use ShareScore to quickly assess how well each record supports discovery, access, and reuse.
3
datasets available to search
ShareScore release 0.9.0
Dataset results
3 results for “Markov decision process”
Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes - Artefact - PEVA
<p><strong>Summary</strong><br>This artifact accompanies the PEVA submission "Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes". It contains the implementation (<code>switss-multi</code>) 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 <code>switss-multi</code> and describe how to use our tool via its command-line and programmatically via its Python interface.</p> <p><strong>Relation to paper</strong><br>This artifact can be used to reproduce all the experimental results (including examples) presented in the paper, that is:<br>- The toy examples presented in Example 12, Example 14, Example 22 and Example 34<br>- Table 3 in Section 6<br>- Table 4 in Section 6<br>- Table 5 in Section 6<br>- Table 8 in Section 6<br>- Figure 9 in Section 6<br>- Figure 10 in Section 6<br>- Figure 11 in Section 6</p> <p><strong>Structure</strong><br>This artifact consists of the following files and folders:<br>- <code>data</code>: Contains original raw experimental data presented in Section 6. Additionally, the log files and scripts for summarizing the raw experimental data are provided.<br>- <code>switss-multi/experiments</code>: Contains the PRISM models, PRISM properties (queries) and scripts for running the experiments.<br>- <code>switss-multi</code>: The source code of the implementation of our presented techniques.<br>- <code>switss-multi-docs</code>: A documentation of the Python API of <code>switss-multi</code>.<br>- <code>peva-docker-image.tar.gz</code>: The compressed Docker image, with the installed implementation (<code>switss-multi</code>), PRISM models, PRISM properties and the scripts for running the experiments and analysing the raw experimental data. Moreover, it contains a copy of the <code>data</code> folder, in case you want to run the analysis scripts on the original data.<br>- <code>docker-results</code>: An empty folder that will be populated with results when running the experiments and analysis with the provided Docker image.<br>- <code>LICENSE</code>: The license of this artifact (MIT license).<br>- <code>GUROBI-EULA</code>: The end-user license agreement of Gurobi (also see https://pypi.org/project/gurobipy/).<br>- <code>GPL-3.0</code>: The GPL 3.0 license. It is included because our dependency Storm (https://www.stormchecker.org) is licensed under it.</p>
Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes - QEST 2024 Artefact
<p>This artifact accompanies the QEST+FORMATS 2024 paper "Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes" (<a href="https://arxiv.org/abs/2406.08175">arXiv</a>). It contains the implementation (<code>switss-multi</code>) 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 <code>switss-multi</code> and describe how to use our tool via its command-line and programmatically via its Python interface.</p> <p><strong>Relation to paper</strong><br>This artifact can be used to reproduce all the experimental results (including examples) presented in the paper, that is:<br>- The toy examples presented in Example 1 and Example 2<br>- Table 1 in Section 5<br>- Table 3 in Appendix D<br>- Figure 5 in Appendix D<br>- Figure 6 in Appendix D<br>- Table 4 in Appendix D</p> <p><strong>Aritfact structure</strong><br>This artifact consists of the following files and folders:<br>- <code>data</code>: 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.<br>- <code>switss-multi</code>: The source code of the implementation of our presented techniques.<br>- <code>switss-multi-docs</code>: A documentation of the Python API of <code>switss-multi</code>.<br>- <code>qest-docker-image.tar.gz</code>: The compressed Docker image, with the installed implementation (<code>switss-multi</code>), PRISM models, PRISM properties and the scripts for running the experiments and analysing the raw experimental data. Moreover, it contains a copy of the <code>data</code> folder, in case you want to run the analysis scripts on the original data.<br>- <code>docker-results</code>: An empty folder that will be populated with results when running the experiments and analysis with the provided Docker image.<br>- <code>LICENSE</code>: The license of this artifact (MIT license).<br>- <code>GUROBI-EULA</code>: The end-user license agreement of Gurobi (also see https://pypi.org/project/gurobipy/).<br>- <code>GPL-3.0</code>: The GPL 3.0 license. It is included because our dependency Storm (https://www.stormchecker.org) is licensed under it.</p> <p><strong>Note on the versions:</strong> 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).</p> <p><strong>Acknowledgments:</strong> 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 Germany’s Excellence Strategy) and the DFG Grant 389792660 as part of TRR 248 (Foundations of Perspicuous Software System).</p>
Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes - Artefact
<div> <h1>Artefact for CAV 2024</h1> <a href="https://github.com/cxlvinchau/cav2024-experiments#artefact-for-cav-2024"></a></div> <p>This artefact accompanies the submission "Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes".</p> <div> <h2>Contents of this artefact</h2> <a href="https://github.com/cxlvinchau/cav2024-experiments#contents-of-this-artefact"></a></div> <p>This artefact consists of two different folders, namely <code>data</code> and <code>software</code>.</p> <div> <h3>The <code>data</code> folder</h3> <a href="https://github.com/cxlvinchau/cav2024-experiments#the-data-folder"></a></div> <p>The <code>data</code> folder contains data and results presented in the experimental section, along with models and properties that have been used. For every model and type of query (mean-payoff or reachability), there is a separate folder, containing the following types of files:</p> <ul> <li><code>data.csv</code> - A csv file where each row corresponds to a query and a model the query was considered for. Every row then contains information on the runtimes and model sizes. A detailed explanation of the columns can be found in the <code>README.md</code> of the data folder.</li> <li>PRISM model files with <code>.nm</code> or <code>.prism</code> extension, corresponding to the models used for the experiments.</li> <li>PRISM property files with <code>.props</code> extension, corresponding to the queries used for the experiments.</li> <li>A <code>README.md</code> with notes on the origins of the models.</li> </ul> <div> <h3>The <code>software</code> folder</h3> <a href="https://github.com/cxlvinchau/cav2024-experiments#the-software-folder"></a></div> <p>The <code>software</code> directory contains our implementation of the presented techniques, including computation of the certificates (aka certification), computation of witnessing schedulers and the computation of minimal witnessing subsystems. It consists of the following components:</p> <ul> <li><code>cpmc</code> contains the Python implementation of the techniques and consists of several submodules: <ul> <li><code>cpmc/core</code> implements classes for representing MDPs and other modeling components</li> <li><code>cpmc/mean_payoff</code> implements the techniques for working with multi-objective mean-payoff queries</li> <li><code>cpmc/reachability</code> implements the techniques for working with multi-objective reachability queries</li> <li><code>cpmc/prism</code> implements the translation of subsystems to PRISM code</li> <li><code>cpmc/test</code> contains unit tests that can be run by navigating into the folder and running <code>pytest .</code></li> </ul> </li> <li><code>experiments</code> contains scripts and utility files for running the experiments: <ul> <li><code>experiments/phil.py</code> Script for running the dining philosophers experiment</li> <li><code>experiments/csn.py</code> Script for running the csn mean-payoff experiment</li> <li><code>experiments/csn_reachability.py</code> Script for running the csn reachability experiment</li> <li><code>experiments/sensors.py</code> Script for running the sensors experiment</li> <li><code>experiments/consensus.py</code> Script for running the consensus (coin) experiment</li> <li><code>experiments/firewire.py</code> Script for running the firewire experiment</li> <li><code>experiments/main.py</code> Command line interface for runnign the experiments</li> </ul> </li> </ul>
ScienceDex guides
Understand access before you commit
These curated guides explain access requirements, typical timelines, costs, and reuse considerations for widely used research datasets.
Allen Brain Atlas
Allen Brain Atlas is an Allen Institute collection of brain map atlases, datasets, APIs, and analysis tools covering mouse, human, and non-human primate brain resources.
Annotated Behaviour and Observability Dataset (ABODe)
ABODe is a University of Edinburgh DataShare dataset for behavior classification in group-housed mice using home-cage video, identities, bounding boxes, ground-plate positions, and annotator labels.
DANDI Archive for NWB datasets
DANDI is a BRAIN Initiative archive for publishing and sharing neurophysiology data, including electrophysiology, optophysiology, and behavioral data packaged as NWB and related standards.
International Brain Laboratory public data
The International Brain Laboratory public data releases expose standardized mouse decision-making experiments, including Neuropixels recordings, widefield calcium imaging, behavior, and session metadata accessed through the ONE API.
OpenNeuro
OpenNeuro is a free, open platform for sharing neuroimaging datasets, with public search, dataset pages, and download paths for web, S3, DataLad, and the OpenNeuro CLI.