University of Konstanz
Graduiertenkolleg / PhD Program
Computer and Information Science

Guest Talks

title

Model checking infinite-state structured Markov chains

speaker

Dr. Anne Remke, University of Twente
Enschede, Netherlands

date & place

Thursday, 23.07.2009, 14:00 h
Room D247

abstract

In the past probabilistic model checking hast mostly been restricted to finite state models. This talk presents the possibilities of model checking with continuous stochastic logic (CSL) on structured infinite-state Markov chains.
We present an in-depth treatment of model checking algorithms for two special classes of infinite-state CTMCs:
(i) Quasi-birth-death processes (QBDs) are a special class of infinite-state CTMCs that combines a large degree of modeling expressiveness with efficient solution methods.
(ii) Jackson queuing networks (JQNs) are a very general class of queueing networks that find their application in a variety of settings. The state space of the CTMC that underlies a JQN, is highly structured, however, of infinite size in as many dimensions as there are queues, whereas the underlying state-space of a QBD can be seen as infinite in one dimension.

Using a new property-driven independency concept that is adapted to QBDs and JQNs, accordingly, we provide model checking algorithms for all the CSL operators. Special emphasis is given to the time-bounded until operator for which we present a new and efficient computational procedure named uniformization with representatives. By the use of an application-driven dynamic termination criterion, the algorithms stop whenever the property to be checked can be certified (or falsified).