Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2603.15559 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915867444379648 |
|---|---|
| author | Volk, Matthias Heck, Linus Junges, Sebastian Katoen, Joost-Pieter Quatmann, Tim |
| author_facet | Volk, Matthias Heck, Linus Junges, Sebastian Katoen, Joost-Pieter Quatmann, Tim |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_15559 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Probabilistic Model Checking Taken by Storm Volk, Matthias Heck, Linus Junges, Sebastian Katoen, Joost-Pieter Quatmann, Tim Software Engineering Logic in Computer Science 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. |
| title | Probabilistic Model Checking Taken by Storm |
| topic | Software Engineering Logic in Computer Science |
| url | https://arxiv.org/abs/2603.15559 |