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

Artefact for CAV 2024

This artefact accompanies the submission "Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes".

Contents of this artefact

This artefact consists of two different folders, namely data and software.

The data folder

The data 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:

data.csv - 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 README.md of the data folder.

PRISM model files with .nm or .prism extension, corresponding to the models used for the experiments.

PRISM property files with .props extension, corresponding to the queries used for the experiments.

A README.md with notes on the origins of the models.

The software folder

The software 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:

cpmc contains the Python implementation of the techniques and consists of several submodules:

cpmc/core implements classes for representing MDPs and other modeling components

cpmc/mean_payoff implements the techniques for working with multi-objective mean-payoff queries

cpmc/reachability implements the techniques for working with multi-objective reachability queries

cpmc/prism implements the translation of subsystems to PRISM code

cpmc/test contains unit tests that can be run by navigating into the folder and running pytest .

experiments contains scripts and utility files for running the experiments:

experiments/phil.py Script for running the dining philosophers experiment

experiments/csn.py Script for running the csn mean-payoff experiment

experiments/csn_reachability.py Script for running the csn reachability experiment

experiments/sensors.py Script for running the sensors experiment

experiments/consensus.py Script for running the consensus (coin) experiment

experiments/firewire.py Script for running the firewire experiment

experiments/main.py Command line interface for runnign the experiments