EECI 2020: Computer Session: Stormpy

Prev: Probabilistic Systems

Course home

Next: Discrete Abstractions

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:
  • Models and policies: light.pm, ma.nm, mh.pm, policy.json,
  • Code analysis_light.ipynb, analysis_compose.ipynb, analysis_policy.ipynb, synthesis.ipynb

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

Additional Information

Group 1	Group 2	Group 3	Group 4
Group 5	Group 6	Group 7	Group 8
Group 9	Group 10	Group 11	Group 12