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>