Difference between revisions of "EECI 2020: Probabilistic Systems"

From MurrayWiki
Jump to: navigation, search
(Lecture Materials)
m (Lecture Materials)
 
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 ==

Latest revision as of 07:57, 10 March 2020

Prev: Model Checking Course home Next: Computer Session: Stormpy

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 (Presentation and notation follow that in "Principles of Model Checking" chapter 10 by Baier and Katoen.)

Further Reading

Additional Information