A Two-Phase Gauss-Seidel Algorithm for the Stationary Solution of EVMDD-Encoded CTMCs

We present a new symbolic approach for the steady-state solution of ergodic continuous-time Markov chains(CTMCs) using iterative methods, based on Edge-Valued Multi-way Decision Diagrams (EVMDDs) to store an indexing function for the structured states and the transition rate matrix. The approach is applicable to any structured CTMC, is memory efficient, and supports both Jacobi and Gauss-Seidel iterations. In particular, our main contribution is a new two-phase algorithm to perform Gauss-Seidel iterations with a reduced decision diagram traversal overhead (a cost also encountered by Kronecker-based approaches). Then, we show how even better speedup can be achieved through a caching scheme. The complexity of our algorithm is linear in the number of nonzero entries in the transition rate matrix, and, even more importantly, it is independent of the number L of submodels in which the CTMC is decomposed under most common conditions. This is an improvement over previous structured methods, which are plagued by this L factor in practice. The advantages of our algorithm are supported by experimental results and a comparison with the tool PRISM.