Probabilistic Model Checking Taken by Storm
Matthias Volk, Linus Heck, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann

TL;DR
This tutorial introduces probabilistic model checking using the Storm tool, emphasizing its performance, Python integration, and application to Markov decision processes and uncertainty models.
Contribution
It provides a comprehensive, hands-on guide to using Storm for probabilistic model checking, including recent extensions for uncertainty handling.
Findings
Effective workflow for MDP modeling and verification
Support for advanced uncertainty models like POMDP and interval MDP
Ease of implementing algorithms on existing data structures
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Adversarial Robustness in Machine Learning · Bayesian Modeling and Causal Inference
