Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Probabilistic Model Checking Taken by Storm

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.

Probabilistic Model Checking Taken by Storm

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.
Paper Structure (25 sections, 2 equations, 6 figures)

This paper contains 25 sections, 2 equations, 6 figures.

Table of Contents

  1. What is Probabilistic Model Checking?
  2. Preliminaries
  3. Step One: Modeling
  4. The Orchard Game
  5. The Orchard Model
  6. Defining the Orchard MDP in Stormvogel
  7. Defining the Orchard MDP in the Prism Language
  8. Model Inspection
  9. Step Two: Model Checking
  10. Reachability
  11. Total Rewards
  12. Beyond
  13. Step Three: Working with Policies
  14. Computing Policies
  15. Analyzing the Induced Submodel
  16. ...and 10 more sections

Figures (6)

  • Figure 1: Probabilistic model checking (extended from DBLP:conf/birthday/HenselJQ025 with tutorial-specific content in small font)
  • Figure 2: State space of the simplified MDP.
  • Figure 3: Visualization of the winning probability on the simplified MDP.
  • Figure 4: Winning probability within given number of rounds.
  • Figure 5: Winning probability in the pMC.
  • ...and 1 more figures

Theorems & Definitions (2)

  • definition 1: Markov decision process (MDP)
  • definition 2: POMDP