EECI 2020: Computer Session: Stormpy: Difference between revisions
From Murray Wiki
Jump to navigationJump to search
No edit summary |
|||
| Line 20: | Line 20: | ||
== Additional Information == | == Additional Information == | ||
[http://ec2-18-194-114-236.eu-central-1.compute.amazonaws.com:8888 Group 1] | [http://ec2-18-194-114-236.eu-central-1.compute.amazonaws.com:8888 Group 1] | ||
[http://ec2-18-185-63-26.eu-central-1.compute.amazonaws.com:8888 Group 2] | |||
Revision as of 16:50, 7 March 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:
- 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
