Seminar: Model Checking Probabilistic Systems

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
Katoen
2
Model Checking Probabilistic and Nondeterministic Systems
Klink
3
Model Checking Stochastic Systems
Klink
4
Model Checking Probabilistic Timed Automata
Jansen
5
Model Checking Hybrid Systems
Abraham
6
Symbolic Model Checking
Katoen
7
Counterexample-guided Abstraction Refinement for Probabilistic Systems
Loup
8
Counterexample Generation using Bounded Model Checking
Abraham
9
Partial Order Reduction
Klink
10
Game-based Abstraction
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