EECI 2020: Computer Session: Stormpy: Difference between revisions
From Murray Wiki
Jump to navigationJump to search
m (Murray moved page EECI 2020: Computer Session: stormpy to EECI 2020: Computer Session: Stormpy) |
No edit summary |
||
| Line 1: | Line 1: | ||
{{eeci-sp2020 header|prev=Probabilistic Systems|next=Discrete Abstractions}} | |||
{{righttoc}} | {{righttoc}} | ||
Revision as of 16:59, 29 February 2020
| 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: 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
