University of Konstanz
Graduiertenkolleg / PhD Program
Computer and Information Science

Colloquium of the Department and the PhD Program


Verifying probabilistic phenomena: theory or practice?


Prof. Dr. Joost-Pieter Katoen, RWTH Aachen, Germany
Aachen, Germany

date & place

Wednesday, 17.01.2007, 16:15 h
Room C252


Model checking of random phenomena enjoys a rapid increase of interest from different communities. Various software tools support the verification of Markov chains or variants thereof that exhibit nondeterminism. Applications range from randomised distributed algorithms, planning and AI, and security to biological process modeling and quantum computing. Verification engines have been integrated in existing tool chains for Petri nets, Statemate, and are used for a probabilistic extension of Promela, the input language of SPIN, one of the most widely used model checkers.

This talk reviews the foundations of this technique and discusses in detail some of the main recent advances in this field, such as abstraction, state space reduction, diagnostic feedback, and the treatment of costs.