Welcome to Stormvogel! (Github, Pypi, Docs, Discord Server)

This notebook provides an overview as well as some example usage and pointers to further material.

Running the Docker container

Using Docker, you can easily run Stormvogel as follows:

docker pull stormvogel/stormvogel
docker run -it -p 8080:8080 stormvogel/stormvogel

See the GitHub repository for more advanced installation options.

What is model checking?

Many processes in science and technology can be analyzed using a state-based model. In the broadest sense, such a model includes states, transitions between states, and usually some kind of output or way to interact with an environment. Once we have a model, we might want to know if this model satisfies certain properties or constraints. The process of determining whether a given model satisfies some property is called model checking.

Example: The behaviour of a self-driving might can be modeled using a Markov model that behaves like the car. We might then check if the model (and hopefully by extension the actual car) satisfies the property that it will always stop driving when it observes a red light.

Below we have a model of a self-driving car. The idea is that the car always choose whether to ‘wait’ or to ‘brake’. Whether this care is safe (unable to reach the state ‘accident’), depends on the choices that are made by the agent.

[1]:

from stormvogel import *
vis = show(examples.create_car_mdp(), layout=stormvogel.layout.Layout("layouts/car.json"))

Test request failed. See 'Communication server remark' in docs. Disable warning by use_server=False.
Network

There are two flavours of model checking: deterministic and probabilistic. In this tool, we exclusively focus on probabilistic model checking.

Over the last decades, many tools to automate probabilistic model checking have been developed at various institutions, but the most succesful ones by far are PRISM and Storm. Stormvogel is built on top of Storm, but also compatible with PRISM.

What is Storm, Stormpy and Stormvogel?

  • Storm is a model checker developed at RWTH Aachen University using C/C++. It is currently considered one of the best model checking tools (it is an order of magnitude faster than PRISM in many cases). It is designed in a low-level way that allows users a great level of control over the internal representation of the models. This means that Storm is very efficient, but also difficult to use.

  • Stormpy is an API with Python bindings for Storm. It is structured mostly similarly to Storm itself.

  • Stormvogel is a series of APIs and visualization tools built on top of stormpy. The goal of Stormvogel is to provide an accessible way to do probabilistic model checking and to provide educational tools about model checking. It is being developped at Radboud University.

What does Stormvogel provide?

  • APIs for constructing Stormvogel models. Currently, DTMCs, MDPs, CTMCs, POMDPs and Markov Automata are supported.

    • The model API can be used to construct a model directly by explicitely defining a set of states and transitions.

    • The pgc API can be used to construct a model by defining a delta function. The structure is similar to PRISM.

    • The PRISM API can be used to construct a model using the PRISM syntax, which has been the standard in model checking over the last years.

    • Futhermore, all the APIs and formats that are supported in Stormpy (Janji, etc.) can also be used, since models can be converted back and forth from and to stormpy with ease.

  • Visualization.

    • Visualize your models by displaying the states, actions and edges

    • Edit and save/load the layout of your models interactively using a GUI

    • Display model checking results in an interactive way

    • Visualize a simulation of a model

  • Seemless conversion between stormvogel and stormpy models.

  • Tooling for model checking.

    • A function for model checking that takes a PRISM property string. Note that this uses Storm under the hood, so it is probably fast.

    • A GUI for making it easier to construct these property strings for beginners (the property builder)

  • Accesible examples and documentation

  • More extensions are in development

Details about these can be found in the remaining notebooks.

Questions/help, bugs & contributing

To suggest a feature or report a bug, simply create an issue on Github. If you would like to contribute to the project yourself, you can always create a pull request or join our public Discord server.

Stormvogel was developed at Radboud University Nijmegen in 2024-2025 by Linus Heck, Pim Leerkes and Ivo Melse under the supervision of Sebastian Junges and Matthias Volk. We would like to thank the Dutch Research Council (NWO) for providing funding for the project.

Good luck using stormvogel! And if you ever get bored or frustrated, the bird is here to cheer you up! (This bird is in fact a singleton DTMC)

[2]:

bird = show_bird()
Network 
[ ]: