EECI 2020: Probabilistic Systems - Revision history

Murray: /* Lecture Materials */

2020-03-10T07:57:46Z

Lecture Materials

← Older revision		Revision as of 07:57, 10 March 2020
Line 5:		Line 5:

	== Lecture Materials ==		== Lecture Materials ==
	* [ [http://www.cds.caltech.edu/~murray/courses/eeci-sp2020//L5_probabilistic-10Mar2020.pdf Lecture slides] (Presentation and notation follow that in "Principles of Model Checking" chapter 10 by Baier and Katoen.)		* [http://www.cds.caltech.edu/~murray/courses/eeci-sp2020//L5_probabilistic-10Mar2020.pdf Lecture slides] (Presentation and notation follow that in "Principles of Model Checking" chapter 10 by Baier and Katoen.)

	== Further Reading ==		== Further Reading ==

Murray: /* Lecture Materials */

2020-03-10T07:57:16Z

Lecture Materials

← Older revision		Revision as of 07:57, 10 March 2020
Line 5:		Line 5:

	== Lecture Materials ==		== Lecture Materials ==
	* [~~https~~://www.~~dropbox~~.~~com~~/s/~~23v517niko6bxhf~~/L5_probabilistic-~~2020~~.pdf~~?dl=0~~ Lecture slides] (Presentation and notation follow that in "Principles of Model Checking" chapter 10 by Baier and Katoen.)		* [ [http://www.cds.caltech.edu/~murray/courses/eeci-sp2020//L5_probabilistic-10Mar2020.pdf Lecture slides] (Presentation and notation follow that in "Principles of Model Checking" chapter 10 by Baier and Katoen.)

	== Further Reading ==		== Further Reading ==

Nok: /* Further Reading */

2020-03-03T16:42:27Z

Further Reading

← Older revision		Revision as of 16:42, 3 March 2020
Line 9:		Line 9:
	== Further Reading ==		== Further Reading ==
	* <p>[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. </p>		* <p>[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. </p>
	* <p>[https://530cb0a7-a-62cb3a1a-s-sites.googlegroups.com/site/tichakorn/~~cdc12_pompdp~~.pdf?attachauth=ANoY7cqyMmicYhlWMkoB7iz5CbxSlWswoBjhDGlO9KmKidxBF7XPwsPpBIan0jkz5g-L5tmEvNtVeLWRYUVW9IkUoiWpg2Rp9FAxMEYJo76l33RsURqvj3W1mMnmK25d5jnLXMsf1uVJXEIBfJzXxbM6I3GdQJfH9bG5spNvcjD3u41YTVh3XBM4Zn32kWp-cuK-4i_q9j_JiizN1Lbgf53y_yShRAADnA%3D%3D&attredirects=0 Control ~~of Probabilistic~~ Systems ~~under Dynamic, Partially Known Environments~~ with Temporal Logic Specifications], T. Wongpiromsarn ~~and~~ E. Frazzoli, ~~CDC 2012~~. ~~Examples~~ of ~~applying~~ probabilistic synthesis to autonomous driving ~~problems~~.</p>		* <p>[https://530cb0a7-a-62cb3a1a-s-sites.googlegroups.com/site/tichakorn/icra13.pdf?attachauth=ANoY7crKSLOes2FVUSIFvUAL1pMBFHwaF7BejOyR81PJ7ERfZmzCbNYmDg_O90rVDdhkoMP0G1FDI7dIpLuBRH4qJwrRRFatIe3VHJbRB4ETTZVUQeAb9FPLEZEvcA614D2lID6wiZtUpacyxrjPGxtLaN5vepGs_ZexGwijYJYODI740knnu1Cx9THrJenwaaeoZXRpLbvztjkQ1XEiUXx2oeuqXP7dKA%3D%3D&attredirects=0 Incremental Synthesis of Control Policies for Heterogeneous Multi-Agent Systems with Linear Temporal Logic Specifications], T. Wongpiromsarn, A. Ulusoy, C. Belta, E. Frazzoli and D. Rus, ICRA 2013. An incremental version of probabilistic synthesis, with autonomous driving examples.</p>
	* <p>[https://530cb0a7-a-62cb3a1a-s-sites.googlegroups.com/site/tichakorn/~~icra13~~.pdf?attachauth=ANoY7crKSLOes2FVUSIFvUAL1pMBFHwaF7BejOyR81PJ7ERfZmzCbNYmDg_O90rVDdhkoMP0G1FDI7dIpLuBRH4qJwrRRFatIe3VHJbRB4ETTZVUQeAb9FPLEZEvcA614D2lID6wiZtUpacyxrjPGxtLaN5vepGs_ZexGwijYJYODI740knnu1Cx9THrJenwaaeoZXRpLbvztjkQ1XEiUXx2oeuqXP7dKA%3D%3D&attredirects=0 ~~Incremental Synthesis~~ of ~~Control Policies for Heterogeneous Multi-Agent~~ Systems with ~~Linear~~ Temporal Logic Specifications], T. Wongpiromsarn~~, A. Ulusoy, C. Belta,~~ E. Frazzoli ~~and D. Rus~~, ~~ICRA 2013~~. ~~Similar to above~~, ~~but~~ with not fully observable agents.</p>		* <p>[https://530cb0a7-a-62cb3a1a-s-sites.googlegroups.com/site/tichakorn/cdc12_pompdp.pdf?attachauth=ANoY7cqyMmicYhlWMkoB7iz5CbxSlWswoBjhDGlO9KmKidxBF7XPwsPpBIan0jkz5g-L5tmEvNtVeLWRYUVW9IkUoiWpg2Rp9FAxMEYJo76l33RsURqvj3W1mMnmK25d5jnLXMsf1uVJXEIBfJzXxbM6I3GdQJfH9bG5spNvcjD3u41YTVh3XBM4Zn32kWp-cuK-4i_q9j_JiizN1Lbgf53y_yShRAADnA%3D%3D&attredirects=0 Control of Probabilistic Systems under Dynamic, Partially Known Environments with Temporal Logic Specifications], T. Wongpiromsarn and E. Frazzoli, CDC 2012. Another example, with not fully observable agents.</p>

	== Additional Information ==		== Additional Information ==

Nok: /* Further Reading */

2020-03-03T16:39:59Z

Murray at 17:26, 29 February 2020

2020-02-29T17:26:31Z

← Older revision		Revision as of 17:26, 29 February 2020
Line 3:		Line 3:

	This lecture provides an introduction to probabilistic model checking. We start with Markov chains as a mathematical model to describe behavior of probabilistic systems where a successor of each state is chosen according to a probability distribution. Then, we discuss basic concepts of probability theory necessary to reason about the quantitative properties of Markov chains. We then move to quantitative analysis of systems modeled by Markov chains, including reachability, regular safety and omega-regular properties. Finally, we introduce Markov decision processes (MDPs), a mathematical model that permits both probabilistic and nondeterministic choices and discuss policy synthesis for MDPs with LTL specifications.		This lecture provides an introduction to probabilistic model checking. We start with Markov chains as a mathematical model to describe behavior of probabilistic systems where a successor of each state is chosen according to a probability distribution. Then, we discuss basic concepts of probability theory necessary to reason about the quantitative properties of Markov chains. We then move to quantitative analysis of systems modeled by Markov chains, including reachability, regular safety and omega-regular properties. Finally, we introduce Markov decision processes (MDPs), a mathematical model that permits both probabilistic and nondeterministic choices and discuss policy synthesis for MDPs with LTL specifications.


	== Lecture Materials ==		== Lecture Materials ==

Murray at 16:57, 29 February 2020

2020-02-29T16:57:43Z

← Older revision		Revision as of 16:57, 29 February 2020
Line 1:		Line 1:
			{{eeci-sp2020 header\|prev=Model Checking\|next=Computer Session: Stormpy}}
	{{righttoc}}		{{righttoc}}

Murray: Murray moved page EECI 2020: Probabilistic systems to EECI 2020: Probabilistic Systems

2020-02-29T16:55:55Z

Murray moved page EECI 2020: Probabilistic systems to EECI 2020: Probabilistic Systems

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

Nok: /* Lecture Materials */

2020-02-27T20:29:32Z

Lecture Materials

← Older revision		Revision as of 20:29, 27 February 2020
Line 5:		Line 5:

	== Lecture Materials ==		== Lecture Materials ==
	* [https://www.dropbox.com/s/23v517niko6bxhf/~~L6_probabilistic~~-2020.pdf?dl=0 Lecture slides] (Presentation and notation follow that in "Principles of Model Checking" chapter 10 by Baier and Katoen.)		* [https://www.dropbox.com/s/23v517niko6bxhf/L5_probabilistic-2020.pdf?dl=0 Lecture slides] (Presentation and notation follow that in "Principles of Model Checking" chapter 10 by Baier and Katoen.)

	== Further Reading ==		== Further Reading ==

Nok at 19:44, 27 February 2020

2020-02-27T19:44:09Z

← Older revision		Revision as of 19:44, 27 February 2020
Line 5:		Line 5:

	== Lecture Materials ==		== Lecture Materials ==
	* ~~Lecture slides:~~ [https://www.dropbox.com/s/23v517niko6bxhf/L6_probabilistic-2020.pdf?dl=0 ~~Probabilistic Systems~~] (Presentation and notation follow that in "Principles of Model Checking" chapter 10 by Baier and Katoen.)		* [https://www.dropbox.com/s/23v517niko6bxhf/L6_probabilistic-2020.pdf?dl=0 Lecture slides] (Presentation and notation follow that in "Principles of Model Checking" chapter 10 by Baier and Katoen.)

	== Further Reading ==		== Further Reading ==

Nok: Created page with "{{righttoc}} This lecture provides an introduction to probabilistic model checking. We start with Markov chains as a mathematical model to describe behavior of probabilistic..."

2020-02-27T19:27:53Z

Created page with "{{righttoc}} This lecture provides an introduction to probabilistic model checking. We start with Markov chains as a mathematical model to describe behavior of probabilistic..."

New page

{{righttoc}}

This lecture provides an introduction to probabilistic model checking. We start with Markov chains as a mathematical model to describe behavior of probabilistic systems where a successor of each state is chosen according to a probability distribution. Then, we discuss basic concepts of probability theory necessary to reason about the quantitative properties of Markov chains. We then move to quantitative analysis of systems modeled by Markov chains, including reachability, regular safety and omega-regular properties. Finally, we introduce Markov decision processes (MDPs), a mathematical model that permits both probabilistic and nondeterministic choices and discuss policy synthesis for MDPs with LTL specifications.

== Lecture Materials ==
* Lecture slides: [https://www.dropbox.com/s/23v517niko6bxhf/L6_probabilistic-2020.pdf?dl=0 Probabilistic Systems] (Presentation and notation follow that in "Principles of Model Checking" chapter 10 by Baier and Katoen.)

== Further Reading ==
* <p>[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. </p>

== Additional Information ==

← Older revision		Revision as of 16:39, 3 March 2020
Line 9:		Line 9:
	== Further Reading ==		== Further Reading ==
	* <p>[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. </p>		* <p>[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. </p>
			* <p>[https://530cb0a7-a-62cb3a1a-s-sites.googlegroups.com/site/tichakorn/cdc12_pompdp.pdf?attachauth=ANoY7cqyMmicYhlWMkoB7iz5CbxSlWswoBjhDGlO9KmKidxBF7XPwsPpBIan0jkz5g-L5tmEvNtVeLWRYUVW9IkUoiWpg2Rp9FAxMEYJo76l33RsURqvj3W1mMnmK25d5jnLXMsf1uVJXEIBfJzXxbM6I3GdQJfH9bG5spNvcjD3u41YTVh3XBM4Zn32kWp-cuK-4i_q9j_JiizN1Lbgf53y_yShRAADnA%3D%3D&attredirects=0 Control of Probabilistic Systems under Dynamic, Partially Known Environments with Temporal Logic Specifications], T. Wongpiromsarn and E. Frazzoli, CDC 2012. Examples of applying probabilistic synthesis to autonomous driving problems.</p>
			* <p>[https://530cb0a7-a-62cb3a1a-s-sites.googlegroups.com/site/tichakorn/icra13.pdf?attachauth=ANoY7crKSLOes2FVUSIFvUAL1pMBFHwaF7BejOyR81PJ7ERfZmzCbNYmDg_O90rVDdhkoMP0G1FDI7dIpLuBRH4qJwrRRFatIe3VHJbRB4ETTZVUQeAb9FPLEZEvcA614D2lID6wiZtUpacyxrjPGxtLaN5vepGs_ZexGwijYJYODI740knnu1Cx9THrJenwaaeoZXRpLbvztjkQ1XEiUXx2oeuqXP7dKA%3D%3D&attredirects=0 Incremental Synthesis of Control Policies for Heterogeneous Multi-Agent Systems with Linear Temporal Logic Specifications], T. Wongpiromsarn, A. Ulusoy, C. Belta, E. Frazzoli and D. Rus, ICRA 2013. Similar to above, but with not fully observable agents.</p>

	== Additional Information ==		== Additional Information ==