EECI 2020: Computer Session: Stormpy: Difference between revisions
From Murray Wiki
Jump to navigationJump to search
No edit summary |
|||
| Line 7: | Line 7: | ||
== Lecture Materials == | == Lecture Materials == | ||
* [https://www.dropbox.com/s/f7emn3p77w57nx9/C1_probabilistic.pdf?dl=0 Lecture slides] | * [https://www.dropbox.com/s/f7emn3p77w57nx9/C1_probabilistic.pdf?dl=0 Lecture slides] | ||
* Example files: [https://www.dropbox.com/s/hvk96u652m1m40d/light.pm?dl=0 light.pm], [https://www.dropbox.com/s/8bdi777j6aw8wc8/ma.nm?dl=0 ma.nm], [https://www.dropbox.com/s/1pp4klntys3zyac/mh.pm?dl=0 mh.pm], [https://www.dropbox.com/s/87ec672ifdi5yh5/policy.json?dl=0 policy.json], [https://www.dropbox.com/s/oagkzn0hnfeor2a/analysis_light.py?dl=0 analysis_light.py], [https://www.dropbox.com/s/81weaf5qyqahepa/analysis_compose.py?dl=0 analysis_compose.py], [https://www.dropbox.com/s/c561i4zcdw44p4t/analysis_policy.py?dl=0 analysis_policy.py], [https://www.dropbox.com/s/ctf79j7r34mgud7/synthesis.py?dl=0 synthesis.py] | |||
== Further Reading == | == Further Reading == | ||
Revision as of 19:50, 27 February 2020
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
