Disk-based techniques for efficient solution of large Markov chains

Computer systems are ubiquitous in almost all spheres of our life, motivat-ing the need for them to function correctly and in a timely manner. Con-tinuous time Markov chains (CTMCs) are a widely used formalism for the performance analysis of computer systems. A large variety of useful per-formance 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 method