EECI 2020: Computer Session: Stormpy
From Murray Wiki
Jump to navigationJump to searchThe printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
| 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 |
