In the past probabilistic model checking hast mostly been restricted to finite state models. This thesis explores the possibilities of model checking with continuous stochastic logic (CSL) on 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). Next to the above methodological contributions of this thesis, we also use the new techniques for an extended case study on bottlenecks in wireless two-hop ad hoc networks. The results of our analysis are compared with extensive simulations and show excellent agreement for throughput, mean number of active sources and mean buffer occupancy at the bottleneck station.
|Award date||20 Jun 2008|
|Place of Publication||Zutphen|
|Publication status||Published - 20 Jun 2008|