Artifact for "Probabilistic Model Checking Taken by Storm"

Radboud Repository (Radboud University)

Abstract

The artifact provides the supplementary material for the tutorial on the probabilistic model checker Storm.The tutorial is a hands-on demonstration of the various workflows possible with Storm and focuses on Markov decision processes (MDP), which are popular in a variety of fields. The tutorial demonstrates the basic workflow, from Python-based modeling, model checking with a variety of properties, to the extraction of policies. Further, it showcases the support for recent topics that focus on different types of uncertainty, such as interval MDP and POMDP, and the ability to quickly implement simple algorithms on top of existing data structures. The artifact is a Docker image providing 5 Jupyter notebooks which allow to interactively follow this tutorial. For each of the five steps in Section 3-7, we provide a corresponding Jupyter notebook which allows to execute the corresponding code examples from the tutorial paper and obtain the outputs given in the paper.

Authors 5

1. Matthias Volk

   Eindhoven University of Technology

   Affiliation as printed

   Eindhoven University of Technology

2. Linus Heck

   Radboud University Nijmegen

   Affiliation as printed

   Radboud University Nijmegen

3. Sebastian Junges

   Radboud University Nijmegen

   Affiliation as printed

   Radboud University

4. Joost-Pieter Katoen Aachen

   RWTH Aachen University · University of Twente

   Affiliation as printed

   RWTH Aachen University

   University of Twente

5. Tim Quatmann Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University