Press *spacebar* to navigate

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

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

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

- Install Docker for your OS
- Download (>1 GB) and start the container:
`docker run -it -p 8080:8080 --name stormpyter movesrwth/stormpyter:discotec2020`

- Open the Jupyter website indicated in the command line: 127.0.0.1:8080/...
- Open file
**discotec_storm.ipynb** - The presentation should start automatically

- 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*

In [ ]:

```
!storm
```

You should see the Storm version information.

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

.

- 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*

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

- Deadlock if all philosophers first pick up left fork

➜ Use *randomized* algorithm

Algorithm by Lehmann and Rabin (POPL'81)

- Random choice whether first picking left or right fork

- thinking
- hungry:
- flip coin to choose first fork
- try to pick up first fork
- if successful continue, else keep trying
- try to pick up second fork
- if successful continue, otherwise put down first fork and think again

- eating
- 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 specifying algorithm for 3 processes todo: add picture with prism code

Source: Prism Website

Read prism file for 3 philosophers with Storm:

In [ ]:

```
!storm --prism examples/phil3.nm --buildfull
```

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

- 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
```

"*Percentage of time spent eating*"

In [ ]:

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

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
```

- 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
```

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
```

**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
```

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
```

"*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
```

"*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
```

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

- Storm supports a variety of input formats:
- Prism language
- Jani modelling language
- Explicit format
- Generalized stochastic Petri nets

In [ ]:

```
!storm --jani examples/phil-nofair3.jani -jprop |tail -7
```

- 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
```

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

- ...

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
```

- 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
```

- 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

**Stormpy**: Python bindings for Storm

➜ Easy and rapid prototyping for probabilistic model checking

In [ ]:

```
```