Difference between revisions of "EECI 2020: Computer Session: Stormpy"

From MurrayWiki
Jump to: navigation, search
(Additional Information)
(Lecture Materials)
 
Line 8: 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:  
 
* 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],

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