Performance Evaluation and Model Checking: a Perfect Match

Joost-Pieter Katoen
University of Twente
Friday, 13 June, 2003 (All day)

Markov chains are one of the most important stochastic processes. They have been widely used to determine system performance and dependability characteristics such as the throughput of production lines, the mean time between failure in safety-critical systems, and bottleneck analysis for high-speed communication networks. Their analysis most often concerns the computation of steady-state and transient-state probabilities.

In this talk, we present branching temporal logics for expressing real-time probabilistic properties over Markov chains and show how such properties can be checked in a fully automated way. These logics can express standard steady-state and transient-state probabilities in a lucid and abstract way and allow for the specification of more involved, non-trivial performance measures. The algorithms used are a combination of numerical analysis methods (such as uniformization and techniques for solving linear systems of equations), graph algorithms and -- most importantly -- model checking. We show how this approach can be applied to discrete-time and continuous- time Markov chains and reward extensions thereof and show some practical applications.

Photographs of the seminar:

Picture of J-P Katoen Picture of J-P Katoen
Click to enlarge !