Part 2: Introduction to Storm

Matthias Volk



[www.stormchecker.org](https://www.stormchecker.org)

Press spacebar to navigate

Storm

A modern probabilistic model checker

  • State-of-the-art: best performance at QComp 2020
  • Modular: dedicated solvers for each task, interchange libraries
  • Written in C++, Python interface via stormpy
  • Open-source, developed since 2012, over 170,000 lines of code

Getting Storm

  • Native support for Linux and macOS (homebrew formula)
  • Virtual machine and Docker containers (also for Windows)

Getting Storm for this presentation

We use a Docker container based on Jupyter Notebook throughout this presentation.

Installation steps:

  1. Install Docker for your OS
  2. Download (>1 GB) and start the container:
    docker run -it -p 8080:8080 --name stormpyter movesrwth/stormpyter:discotec2020
    
  3. Open the Jupyter website indicated in the command line: 127.0.0.1:8080/...
  4. Open file discotec_storm.ipynb
  5. The presentation should start automatically

Hands-on presentation

  • This is an interactive presentation. You can execute all commands by yourself!
  • Navigate with spacebar and shift+spacebar
  • All interactive commands can be executed with shift+enter
  • Switch between presentation and notebook with alt+r

Example

In [ ]:
!storm

You should see the Storm version information.

You can even change the code! Try adding the flag --version.

Dining philosophers

  • Formulated in 1965 by Edsger Dijkstra
  • Philosophers become hungry from thinking
  • Every hungry philosophers wants to eat
  • Before eating, pick up left and right fork

Dining philosophers

Problem

No fully distributed and symmetric deterministic algorithm is possible (Lehmann, Rabin 1981)

  • Deadlock if all philosophers first pick up left fork

Solution

➜ Use randomized algorithm

Algorithm by Lehmann and Rabin (POPL'81)

  • Random choice whether first picking left or right fork

Randomized dining philosophers (Lehmann, Rabin)

  1. thinking
  2. hungry:
    1. flip coin to choose first fork
    2. try to pick up first fork
    3. if successful continue, else keep trying
    4. try to pick up second fork
    5. if successful continue, otherwise put down first fork and think again
  3. eating
  4. put down left and right fork and think again
s=0 -> (s'=0); //stay thinking
s=0 -> (s'=1); //trying
// draw randomly
s=1 -> 0.5 : (s'=2) + 0.5 : (s'=3); 
s=2 &  lfree -> (s'=4); //pick up left
s=2 & !lfree -> (s'=2); //left not free
...
// Finished eating
s=9  -> (s'=10); //put down left 
s=10 -> (s'=0);  //go back to thinking

Source: Prism Website

Prism file for randomized dining philosophers

Prism file specifying algorithm for 3 processes todo: add picture with prism code

Source: Prism Website

Building model with Storm

Read prism file for 3 philosophers with Storm:

In [ ]:
!storm --prism examples/phil3.nm --buildfull

Model checking

  • Model: randomized dining philosophers
  • Properties:
    • Starvation freedom
    • Mutual exclusion for forks
    • Average waiting time
    • ...

Model checking DTMC

  • Assume scheduling of processes follows uniform distribution
    ➜ Yields discrete-time Markov chain (DTMC)

"Probability that no philosopher is ever hungry"

In [ ]:
!storm --prism examples/phil3.pm --prop 'P=? [G !"hungry"]'  |tail -n+12

Model checking DTMC

"Percentage of time spent eating"

In [ ]:
!storm --prism examples/phil3.pm --prop 'S=? ["eat"]' |tail -4

Model checking DTMC

Liveness: "If a philosopher is hungry then eventually some philosopher eats"

In [ ]:
!storm --prism examples/phil3.pm --prop 'filter(forall, P>=1 [F "eat"], "hungry")' |tail -4

Model checking MDP

  • Allow arbitrary scheduling of processes now
    ➜ Yields Markov decision process (MDP) containing non-determinism

"(Minimal/Maximal) Probability that no philosopher is ever hungry"

In [ ]:
!storm --prism examples/phil3.nm --prop 'Pmin=? [G !"hungry"];Pmax=? [G !"hungry"]' |tail -n+12

Model checking MDP

Liveness: "If a philosopher is hungry then eventually some philosopher eats"

In [ ]:
!storm --prism examples/phil3.nm --prop 'filter(forall, P>=1 [F "eat"], "hungry")' |tail -3

Model checking MDP

Problem: unfair schedulers avoid scheduling hungry philosophers
Solution: use adapted algorithm without fairness assumptions (Duflot, Fribourg, Picaronny, 2004)

In [ ]:
!storm --prism examples/phil-nofair3.nm --prop 'filter(forall, P>=1 [F "eat"], "hungry")' |tail -3

Model checking deterministic algorithm

Consider (wrong) deterministic algorithm where always left fork is picked first.
Before: s=1 -> 0.5 : (s'=2) + 0.5 : (s'=3);
After: s=1 -> 1 : (s'=2);

In [ ]:
!storm --prism examples/phil-nofair-det3.nm --prop 'filter(forall, P>=1 [F "eat"], "hungry")' |tail -3

Computing waiting times for philosophers

"Probability that a hungry philosopher eats within 10 steps"

In [ ]:
!storm --prism examples/phil-nofair3.nm --prop 'filter(min, Pmin=? [F<=10 "eat"], "hungry");filter(avg, Pmin=? [F<=10 "eat"], "hungry")' |tail -7

Computing waiting times for philosophers

"Expected number of steps (in the worst-case) that a hungry philosopher needs to take before eating"

In [ ]:
!storm --prism examples/phil-nofair3.nm --prop 'filter(max, Rmax=? [F "eat"], "hungry")' |tail -3

Modularity of Storm

  • Use different input formats
  • Modularity allows to use different solvers and libraries

Input formats

In [ ]:
!storm --jani examples/phil-nofair3.jani -jprop |tail -7

Computing exact values

  • Floating point arithmetic and convergence criteria might not be precise
    ➜ use exact (rational) numbers and sound algorithms off-the-shelf
  • Drawback: performance might decrease
In [ ]:
!storm --prism examples/phil-nofair3.nm --prop 'filter(max, Rmax=? [F "eat"], "hungry")' |tail -2
In [ ]:
!storm --prism examples/phil-nofair3.nm --prop 'filter(max, Rmax=? [F "eat"], "hungry")' --exact |tail -2

Engines in Storm

Storm supports different model representations:

  • Sparse matrix:
    • Model building is time and memory intensive
    • Fast numerical computations
  • Binary Decision Diagrams (BDD):
    • Fast and memory efficient model building if model is structured
    • Slower numerical computations
  • Hybrid approach:
    • Build with BDD, use sparse matrix for numerical computations
  • ...

Engines in Storm

In [ ]:
!storm --engine sparse --prism examples/phil-nofair5.nm --prop 'Pmax=? [F no_eat>1]' |tail -n+7
In [ ]:
!storm --engine dd --prism examples/phil-nofair5.nm --prop 'Pmax=? [F no_eat>1]' --ddlib cudd |tail -n+7

Bisimulation minimization

  • Reduces state-space size without loosing information
  • Exploits symmetries
In [ ]:
!storm --bisimulation --prism examples/phil-nofair3.nm --prop 'filter(forall, P>=1 [F "eat"], "hungry")' |tail -n+7

Summary

  • Basic introduction to Storm command-line interface
  • Correctness of dining philosophers algorithm
  • Storm supports broad range of models and properties
  • Different engines allow tailored analysis per model and property

Next:

Stormpy: Python bindings for Storm
➜ Easy and rapid prototyping for probabilistic model checking

In [ ]: