Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This tutorial paper provides a practical guide to probabilistic model checking using the Storm model checker, emphasizing its performance and Python integration capabilities. It focuses on Markov decision processes (MDPs) and demonstrates modeling, property verification, and policy extraction. The tutorial also highlights Storm's support for handling various types of uncertainty, including interval MDPs and POMDPs, and its extensibility for implementing custom algorithms.
Storm's decade-long development now offers a powerful, Python-integrated environment for probabilistic model checking, making it easier than ever to analyze Markov decision processes and models with uncertainty.
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.