Abstract. Computer systems are ubiquitous in almost all spheres of our life, motivating the need for them to function correctly and in a timely manner. Continuous time Markov chains (CTMCs) are a widely used formalism for the performance analysis of computer systems. A large variety of useful performance measures can be derived from a CTMC via the computation of its steady-state probabilities. Traditional methods for performance analysis typically require the generation and storage of the underlying state space of the CTMC, and the processing of the state space for the numerical solution. CTMC models for even trivial real-life systems are usually huge, and both the amount of required memory and the time to compute the solution pose a major difficulty.

In this thesis, we present techniques which extend the size of analysable models on a single workstation, with the goal for alleviating the state space explosion problem. We introduce explicit and symbolic disk-based methods which relax the storage limitations of contemporary techniques and are able to extend the size of solvable models by an order of magnitude. We also propose a new sparse storage scheme which provides 30% or more savings over the conventional sparse schemes and improves the solution speed. Furthermore, we present modifications to multi-terminal binary decision diagrams (MTBDDs), a symbolic data structure for storing CTMCs. The modifications improve the time and memory properties of this data structure, and allow an efficient implementation of the Gauss-Seidel iterative method, which was not possible previously.

Using the techniques introduced in this thesis, we demonstrate analysis of models with over 1.2 billion states and 16 billion transitions on a single workstation. Currently, models of such sizes cannot be solved on a contemporary workstation using conventional techniques.