Probabilistic Model Checking Taken by Storm
2026-03-16 • Software Engineering
Software EngineeringLogic in Computer Science
AI summaryⓘ
The authors explain how to use the Storm model checker, a tool that helps analyze systems with randomness and choices, called Markov decision processes (MDPs). They show how to build models using Python, check different properties, and find good strategies from those models. The paper also covers newer types of MDPs that deal with uncertainty, like interval MDPs and partially observable MDPs (POMDPs). The authors highlight how easy it is to create simple algorithms using Storm's existing tools.
probabilistic model checkingStorm model checkerMarkov decision processesPython modelingpoliciesinterval MDPPOMDPuncertaintymodel checking algorithmsreinforcement learning basics
Authors
Matthias Volk, Linus Heck, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann
Abstract
This tutorial paper presents a hands-on perspective on probabilistic model checking with the Storm model checker. Storm is a decade-old model checker that excels in performance and a rich Python-based ecosystem, which makes it easy to integrate in various workflows. This tutorial focuses on Markov decision processes (MDP), which are popular in a variety of fields. It 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.