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 (www.prismmodelchecker.org) 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):- Discrete-time Markov chains
- Probability measure on paths
- Reachability and persistence
- Computation of transient and steady-state probability
- Logic PCTL
- Model checking for PCTL (next, bounded until, reduction to linear equation for unbounded until, precomputation)
- Counterexamples
- Exercises on Markov chains, probability computation
- Examples of PCTL formulas, checking satisfaction, etc
- Markov decision processes
- Reachability
- PCTL model checking (reduction to linear programming for unbounded until, value iteration, policy iteration)
- Logic LTL
- Automata-based properties
- LTL model checking for MDPs
- Exercises on Markov decision processes, computation of minimum/maximum probabilities
- Examples of LTL model checking, etc
You can find the problem set here. Please send your solutions (or questions, should you have any) to Bartosz Klin by Monday, July 1.