KTH'15: Probabilistic verification and synthesis

The site contains various resources for the Probabilistic Verification and Synthesis course taught at KTH Institute of Technology (August 2015).

• Slides for the lectures given by Marta Kwiatkowska:
  • part 1 (Introduction + PRISM);
  • part 2 (Discrete-time Markov chains);
  • part 3 (Markov decision processes + strategy synthesis);
  • part 4 (LTL verification + stochastic games);
  • part 5 (Probabilistic timed automata).
  
  
• A lab session based on the PRISM tool.

Background reading

• The following papers are recommended background reading:
  • for Markov chains see this tutorial paper;
  • for Markov decision processes see this tutorial paper;
  • for stochastic games see this paper and this tool paper;
  • for probabilistic timed automata see this tutorial paper.
  
  
• The book Principles of of Model Checking by Christel Baier and Joost-Pieter Katoen is recommended reading for the course.
  
  
• There are further tutorial papers listed here.

Site hosted at the Department of Computer Science, University of Oxford