EECI 2020: Computer Session: Stormpy

Hands-on probabilistic model checking exercises using stormpy.

• quantitative analysis of PCTL specifications against Markov chain model
• control strategy synthesis.

Lecture Materials

• Lecture slides
• * Example files: light.pm, ma.nm, mh.pm, policy.json, analysis_light.py, analysis_compose.py, analysis_policy.py, synthesis.py

Further Reading

• Principles of Model Checking, C. Baier and J.-P. Katoen, The MIT Press, 2008. A detailed reference on model checking. Slides for this lecture follow Chapter 10 of this reference.

• stormpy. A comprehensive reference on stormpy

• prism. For the PRISM Language and properties