Solution of Large Markov Models Using Lumping Techniques and Symbolic Data Structures

Continuous time Markov chains (CTMCs) are among the most fundamental mathematical structures used for performance and dependability modeling of communication and computer systems. They are often constructed from models described in one of the various high-level formalisms. Since the size of a CTMC usually grows exponentially with the size of the corresponding high-level model, one often encounters the infamous state-space explosion problem, which often makes solution of the CTMCs intractable and sometimes makes it impossible. In state-based numerical analysis, which is the solution technique we have chosen to use to solve for measures defined on a CTMC, the state-space explosion problem is manifested in two ways: 1) large state transition rate matrices, and 2) large iteration vectors. The goal of this dissertation is to extend, improve, and combine existing solutions of the state-space explosion problem in order to make possible the construction and solution of very large CTMCs generated from high-level models. Our new techniques follow largeness avoidance and largeness tolerance approaches. In the former approach, we reduce the size of the CTMC that needs to be solved in order to compute the measures of interest. That makes both the transition matrix and the iteration vectors smaller. In the latter approach, we reduce the size of the representation of the transition matrix by using symbolic data structures. In particular, we have developed the fastest known CTMC lumping algorithm with the running time of \Ord(m \log n), where n and m are the number of states and non-zero entries of the generator matrix of the CTMC, respectively. The algorithm can be used both in isolation and along with all compositional lumping algorithms, including the one we have proposed in this dissertation. We have also combined the use of multi-valued decision diagram (MDD) and matrix diagram (MD) symbolic data structures with state-lumping techniques to develop an efficient symbolic state-space exploration algorithm for state-sharing replicate/join composed models that exploits lumpings that are due to equally behaving components created by the replicate operator. Finally, we have developed a new compositional algorithm that lumps CTMCs represented as MDs. Unlike other compositional lumping algorithms, our algorithm does not require any knowledge of the modeling formalisms from which the MDs were generated. Our approach relies on local conditions, i.e., conditions on individual nodes of the MD, which are often much smaller than the state transition rate matrix of the overall CTMC. We believe that our new approach has a simpler formulation, and thus is easier to understand