Probabilistic Model Checking

Lecturer: Professor Marta Kwiatkowska (University of Oxford, UK).

About the lecturer | Course Structure | Slides: 1 2 3 4 | Assignment

About the lecturer: Marta Kwiatkowska is Professor of Computing Systems and Fellow of Trinity College, University of Oxford. She was elected to Academia Europea in 2011 and received a prestigious ERC Advanced Grant VERIWARE "From software verification to everyware verification", 2010-15.

Kwiatkowska's research is concerned with modelling and automated verification techniques for probabilistic systems, with application to engineered and biological systems. Her work was recognised by invitations to speak at the LICS 2003, ESEC/FSE 2007, FASE/ETAPS 2011 and SAFECOMP 2012 conferences. The PRISM model checker ( developed under her leadership is internationally leading in the area and widely used for research and teaching. Applications of probabilistic model checking have spanned communication and security protocols, nanotechnology designs, power management and systems biology. Her research is supported by £3m of grant funding from EPSRC, EU, Oxford Martin School and Microsoft Research.

Marta Kwiatkowska serves on numerous programme committees and editorial boards of several journals, including Formal Methods in System Design, IEEE Transactions on Software Engineering and Royal Society's Philosophical Transactions A. She was lead organiser of the Royal Society Discussion Meeting "From computers to ubiquitous computing, by 2020" and guest co-editor of the associated Proceedings in Phil. Trans. R. Soc. A vol 366 no 1881.

Course structure: The course is based on a 20-lecture course taught by Marta Kwiatkowska at the University of Oxford. It covers the basics of discrete-time Markov chains and Markov deicision processes, the logics PCTL and LTL and their model checking.

LECTURE 1 (April 26, 2013): LECTURE 2 (April 27, 2013): CLASS 1 (April 27, 2013): LECTURE 3 (May 24, 2013): LECTURE 4 (May 25, 2013): CLASS 1 (May 25, 2013): Assignment:

You can find the problem set here. Please send your solutions (or questions, should you have any) to Bartosz Klin by Monday, July 1.