Markov decision processes (MDPs) are the prime model to capture decision-making under uncertainty. That is, MDPs and its extensions are suitable to describe how agents interact with an unpredictable and potentially hostile environment.
We take a model-centric view and ask key questions such: What is the probability to reach an error state? or What is the best policy to steer a robot to the target within a given energy budget?
In this tutorial, we present the probabilistic model checking tool Storm that can automatically answer these questions, even in the absence of precisely known models or partial observability. Storm supports various input languages such as variations of Petri nets, fault trees, and domain-specific probabilistic programming languages. It supports questions that allow trading off various objectives, provides precise results with strict guarantees, is open access, and is accessible via a Python API.
- Understand the theory behind probabilistic model checking.
- Get to know the most important algorithms
- Learn how to model systems as Markov chains and Markov decision processes.
- Learn how to formulate queries about the behavior of a system.
- Learn how to use the Storm probabilistic model checker.
Structure of the workshop
Part 1: Fundamentals of Probabilistic Model Checking
We will start with an introduction into the basics of probabilistic model checking. We will discuss the important notions of Markov chains and Markov decision processes and define the semantics of the temporal logics LTL and CTL.
- Markov chains and Markov decision processes.
- LTL and CTL.
Part 2: Fault Tree Analysis
Fault tree analysis is a popular technique in safety and reliability engineering. Dynamic fault trees are a flexible model that is able to capture common dependability patterns, such as spare management, functional dependencies, and sequencing. We will discuss how to use Storm to analyze dynamic fault trees.
Part 3: Hands-on probabilistic Model Checking with Storm
We will then move on to a hands-on session where we will use the Storm probabilistic model checker to verify properties of some simple models.
- Storm probabilistic model checker
Part 4: Parameter Synthesis in Markov Models.
So far, we have only considered the case where the parameters of a Markov model are known. In many applications, however, some parameters are free to choose. In this part, we will discuss how to synthesize parameters of a Markov model such that a given specification is satisfied with high probability.
- Parameter synthesis in Markov models.
- Basic knowledge of probability theory.
- Mo particular programming skills are required.
- No prior knowledge of machine learning is required.