EECI 2020: Computer Session: Stormpy: Difference between revisions

From Murray Wiki
Jump to navigationJump to search
 
(6 intermediate revisions by 2 users not shown)
Line 1: Line 1:
{{eeci-sp2020 header|prev=Probabilistic Systems|next=Discrete Abstractions}}
{{righttoc}}
{{righttoc}}


Line 6: Line 8:


==  Lecture Materials ==
==  Lecture Materials ==
* [https://www.dropbox.com/s/f7emn3p77w57nx9/C1_probabilistic.pdf?dl=0 Lecture slides]  
* [http://www.cds.caltech.edu/~murray/courses/eeci-sp2020/C1_probabilistic-10Mar2020.pdf 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]
* 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],
** Code [https://www.dropbox.com/s/k56l72yuud0wh9m/analysis_light.ipynb?dl=0 analysis_light.ipynb], [https://www.dropbox.com/s/s0a67cilq5wc2bc/analysis_compose.ipynb?dl=0 analysis_compose.ipynb], [https://www.dropbox.com/s/p2kx6pzf26ik3t1/analysis_policy.ipynb?dl=0 analysis_policy.ipynb], [https://www.dropbox.com/s/chrt9atu98ybl0l/synthesis.ipynb?dl=0 synthesis.ipynb]


== Further Reading ==
== Further Reading ==
Line 15: 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

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
Retrieved from "https://murray.cds.caltech.edu/index.php?title=EECI_2020:_Computer_Session:_Stormpy&oldid=23527"