Continuous time Markov chains (CTMCs) are a widely used formalism for the performance analysis of computer systems and communication networks. Many stochastic systems can be modelled as a CTMC, and the CTMC can be analysed using, for instance, probabilistic model checking. Required or desired performance properties are specified as formulas in the temporal logic CSL and then automatically verified using the appropriate model checking algorithms. Traditional methods for performance analysis typically require the generation, storage, and the processing of the underlying state space for the numerical solution. The numerical solution phase can be reduced to the solution of linear equation systems of the form Ax=0.
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 talk, we present computational techniques to alleviate the state space explosion problem. The techniques extend the size of analysable models on a single workstation and on multiple machines. We discuss explicit and symbolic 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 discuss a 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 discussed techniques, we demonstrate analysis of models with over 1.2 billion states and 16 billion transitions on a single and multiple workstation. Currently, models of such sizes cannot be solved on a contemporary workstation using conventional techniques.