References: Chapter 10 of the book "Principles of Model Checking", MIT Press, May 2008, by Christel Baier and Joost-Pieter Katoen; course slides by David Parker.

Date	Topics covered
Oct 9	Introduction, Discrete Time Markov Chains (DTMCs) - definitions, some properties, Bertrand's paradox.
Oct 11	Probability spaces, paths of a DTMC, cylinder sets.
	Homework Assignment
Oct 18	DTMCs: Probabilistic reachability, computing reachibility probabilities as a fixed point of a linear equation system, iterative method, least fixed point characterization, bounded reachability.
Oct 23	DTMCs: Transient state probabilities, long run behaviours/steady-state distributions, computation and characterization, qualitative and quantitative properties.
Oct 25	Markov reward models: DTMCs with costs and rewards, expected reward for reachability, cost-bounded reachability, constrained reachability, long run properties.
	Quiz (Nov 11)
Nov 6	Markov decision processes (MDPs), capturing nondeterminism and probabilities, definitions, examples, schedulers.
Nov 8	MDPs: reachability properties, qualitative reachability, optimality equations, optimal schedulers.
Nov 13	MDPs: computing reachability probability over optimal schedulers, value iteration algorithm, linear program formulation, policy iteration.
Nov 15	PRISM Tool for probabilistic systems - demo and presentation by Ganesh Narwane.
Nov 16	Tutorial
Nov 26	Exam

Note: this course is related to / is a part of CS620: New Trends in Information Technology, co-taught by Ashutosh Trivedi and CS 691: Concepts, Algorithms and Tools for Model-Checking, co-taught by S. Krishna.

- Lecture 1 (June 4): Turing machines (Slides)

- Tutorial (June 5): No new material was covered (Quiz)

- Lecture 2 (June 7): Decidability and Undecidability(Slides)

- Lecture 3 (June 10): Reductions and Rice's Theorem (Slides)

- Tutorial (June 11): No new material was covered

- Midsem (June 12)

- Lecture 4 (June 14): Post's correspondence problem (PCP) and introduction to complexity theory (Slides)

- 1hr Guest Lecture (June 14 at 11.30am): Propositional and first-order logic - by Abhishek Sankaran

- 1hr Guest Lecture (June 17 at 10.45am): Monadic second-order logic and connections to finite automata - by Abhishek Sankaran

Further details of the entire course can be found here.