EECI 2020: Computer Session: Stormpy: Difference between revisions
From Murray Wiki
Jump to navigationJump to search
| (3 intermediate revisions by the same user not shown) | |||
| Line 8: | Line 8: | ||
== Lecture Materials == | == Lecture Materials == | ||
* [ | * [http://www.cds.caltech.edu/~murray/courses/eeci-sp2020/C1_probabilistic-10Mar2020.pdf Lecture slides] | ||
* Example files: | * Example files: | ||
** Models and policies: [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], | ** Models and policies: [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], | ||
| Line 19: | Line 19: | ||
== Additional Information == | == Additional Information == | ||
{| width=100% | |||
|- align=middle | |||
| [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] | |||
| [http://ec2-3-124-204-95.eu-central-1.compute.amazonaws.com:8888 Group 3] | |||
| [http://ec2-3-124-187-217.eu-central-1.compute.amazonaws.com:8888 Group 4] | |||
|- align=middle | |||
| [http://ec2-3-121-200-138.eu-central-1.compute.amazonaws.com:8888 Group 5] | |||
| [http://ec2-18-197-182-3.eu-central-1.compute.amazonaws.com:8888 Group 6] | |||
| [http://ec2-54-93-43-158.eu-central-1.compute.amazonaws.com:8888 Group 7] | |||
| [http://ec2-52-57-123-29.eu-central-1.compute.amazonaws.com:8888 Group 8] | |||
|- align=middle | |||
| [http://ec2-3-124-206-21.eu-central-1.compute.amazonaws.com:8888 Group 9] | |||
| [http://ec2-3-125-42-83.eu-central-1.compute.amazonaws.com:8888 Group 10] | |||
| [http://ec2-18-195-242-25.eu-central-1.compute.amazonaws.com:8888 Group 11] | |||
| [http://ec2-18-196-190-175.eu-central-1.compute.amazonaws.com:8888 Group 12] | |||
|} | |||
Latest revision as of 08:00, 10 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
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 |
