Stormvogel Documentation

Stormvogel provides easy and user-friendly APIs for creating, visualizing, and debugging probabilistic Markov models.

Get started here!

Getting Started

• Welcome to Stormvogel!

Source Code Repository and Issue Tracker:

GitHub Repository

PyPI Package:

PyPI Package

Documentation Index:

Orchard Tutorial

• Step One: Modeling
  • The Orchard Game
  • The Orchard Model
  • Data structures with Stormvogel
  • Defining the Orchard MDP
  • Building the models
  • Defining the MDP in the Prism language
  • Model inspection
• Step Two: Model Checking
  • Preparation
  • Reachability
  • Total rewards
  • Beyond
• Step Three: Working with Policies
  • Preparation
  • Computing Policies
  • Analyzing the Induced Submodel
  • Compact Policies
• Step Four: MDPs with More Uncertainty
  • Preparation
  • Imprecise Probabilities
  • Partially Observable MDPs
• Next Steps
  • Preparation
  • Model representation
  • Bisimulation
  • Model checking algorithms
  • Writing an LP-based MDP Model Checker

Core Stormvogel Concepts

• Building DTMCs
  • The Knuth die
  • Simple communication
• Building MDPs
  • The study dilemma
  • Grid model
• Building CTMCs
• Building POMDPs
• Working with Stormvogel and Stormpy
• Simulator

Stormvogel Goes To The Gym

• Gymnasium integration
  • FrozenLake
  • CliffWalking
  • Taxi
• Gymnasium sampling
  • FrozenLake
  • Blackjack
  • Acrobot

Advanced Features

• Parametric and Interval Models
  • Interval Models
• Visual value iteration and Markov Chain evolution
  • Value iteration
  • DTMC evolution
• Policy iteration
• Generating GIFs
• Parallel composition
  • m1
  • m2
  • Quotient model
• End component elimination
• Advanced Model Visualization
  • Javascript visualization
  • Positioning algorithms
  • Matplotlib visualization
• API Reference
  • stormvogel

Version info:

Last update: Mar 26, 2026.

Current version: 0.10.2.

Search for a specific page:

• Index

• Module Index

• Search Page