EECI 2020: Computer Session: Stormpy - Revision history

Murray: /* Lecture Materials */

2020-03-10T08:00:30Z

Lecture Materials

← Older revision		Revision as of 08:00, 10 March 2020
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],

Murray: /* Additional Information */

2020-03-08T15:49:35Z

Additional Information

@@ Line 19: / Line 19: @@
 ==  Additional Information ==
-[http://ec2-18-194-114-236.eu-central-1.compute.amazonaws.com:8888 Group 1]
+{| width=100%
+|- align=middle
-[http://ec2-18-185-63-26.eu-central-1.compute.amazonaws.com:8888 Group 2]
+| [http://ec2-18-194-114-236.eu-central-1.compute.amazonaws.com:8888 Group 1]

Murray: /* Additional Information */

2020-03-07T16:50:20Z

Additional Information

← Older revision		Revision as of 16:50, 7 March 2020
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]

Murray at 08:11, 7 March 2020

2020-03-07T08:11:13Z

← Older revision		Revision as of 08:11, 7 March 2020
Line 19:		Line 19:

	== Additional Information ==		== Additional Information ==
			[http://ec2-18-194-114-236.eu-central-1.compute.amazonaws.com:8888 Group 1]

Nok: /* Lecture Materials */

2020-03-03T01:56:00Z

Lecture Materials

← Older revision		Revision as of 01:56, 3 March 2020
Line 9:		Line 9:
	== 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]		* 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 ==

Murray at 16:59, 29 February 2020

2020-02-29T16:59:57Z

← Older revision		Revision as of 16:59, 29 February 2020
Line 1:		Line 1:
			{{eeci-sp2020 header\|prev=Probabilistic Systems\|next=Discrete Abstractions}}

	{{righttoc}}		{{righttoc}}

Murray: Murray moved page EECI 2020: Computer Session: stormpy to EECI 2020: Computer Session: Stormpy

2020-02-29T16:57:56Z

Murray moved page EECI 2020: Computer Session: stormpy to EECI 2020: Computer Session: Stormpy

← Older revision		Revision as of 16:57, 29 February 2020
(No difference)

Nok: /* Lecture Materials */

2020-02-27T19:50:14Z

Lecture Materials

← Older revision		Revision as of 19:50, 27 February 2020
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]		* 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 ==

Nok at 19:50, 27 February 2020

2020-02-27T19:50:03Z

← Older revision		Revision as of 19:50, 27 February 2020
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 ==

Nok: Created page with "{{righttoc}} Hands-on probabilistic model checking exercises using stormpy. * quantitative analysis of PCTL specifications against Markov chain model * control strategy synt..."

2020-02-27T19:43:33Z

Created page with "{{righttoc}} Hands-on probabilistic model checking exercises using stormpy. * quantitative analysis of PCTL specifications against Markov chain model * control strategy synt..."

New page

{{righttoc}}

Hands-on probabilistic model checking exercises using stormpy.
* quantitative analysis of PCTL specifications against Markov chain model
* control strategy synthesis.

== Lecture Materials ==
* [https://www.dropbox.com/s/f7emn3p77w57nx9/C1_probabilistic.pdf?dl=0 Lecture slides]

== Further Reading ==
* [http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=11481 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. 
* [https://moves-rwth.github.io/stormpy stormpy]. A comprehensive reference on stormpy 
* [https://www.prismmodelchecker.org/manual/Main/Welcome prism]. For the PRISM Language and properties 

== Additional Information ==