Model Checking Probabilistic Systems
Seminar · Master
- Summer Term 2009
- Teachers: Erika Ábrahám, Joost-Pieter Katoen, Daniel Klink, Nils Jansen, Ulrich Loup
Model checking of probabilistic and hybrid systems has enjoyed a rapid increase of interest. Applications include randomized distributed algorithms, planning and AI, security, communication protocols, systems biology and quantum computing. Dedicated model checkers such as PRISM, MRMC, LiQuor and YMER support the verification of a wide class of models. This seminar focuses on the theoretical underpinnnings and advanced techniques improving the usability and efficiency.
Downloads
The papers and slides are now available for download (see your mail account for authentification details)!
Important Dates
| 07.4.2009 - 16:00 | Introductory meeting (Slides) |
|---|---|
| 18.5.2009 | Paper: Detailed Outline |
| 08.6.2009 | Paper: Chapters 2, …, n-1 completed |
| 22.6.2009 | Paper: Final version |
| 06.7.2009 | Slides: Complete version |
| 13.7.2009 | Slides: Final version |
| 20.7.2009 - 9:00 | Seminar |
Topics
A short introduction to each topic will be given in the introductory meeting. Some literature may only be accessible from within the RWTH net.
| Nr | Topic | Literature | Student | Supervisor |
|---|---|---|---|---|
| 1 | A Survey of Probabilistic Models | (1) | Katoen | |
| 2 | Model Checking Probabilistic and Nondeterministic Systems | (1) (2) | Klink | |
| 3 | Model Checking Stochastic Systems | [(1) | ||
| ](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.68.2348) | Klink | |||
| 4 | Model Checking Probabilistic Timed Automata | (1) | Jansen | |
| 5 | Model Checking Hybrid Systems | (1) (2) | Abraham | |
| 6 | Symbolic Model Checking | (1) (2) | Katoen | |
| 7 | Counterexample-guided Abstraction Refinement for Probabilistic Systems | (1) | Loup | |
| 8 | Counterexample Generation using Bounded Model Checking | (1) | Abraham | |
| 9 | Partial Order Reduction | (1) | Klink | |
| 10 | Game-based Abstraction | (1) | Klink |
Requirements
- Vordiplom Informatik or Bachelor in Computer Science (in particular:
basic knowledge in Automata Theory and Formal Languages) - The written exposition and the presentation can be done in either
German or English. - Basic knowledge in Model-Checking techniques is not mandatory
but helpful.
Contact person
Daniel Klink