Model Checking Markov Chains Using Krylov Subspace Methods: An Experience Report

摘要

The predominant technique for computing the transient distribution of a Continuous Time Markov Chain (CTMC) exploits uni-formization, which is known to be stable and efficient for non-stiff to mildly-stiff CTMCs. On stiff CTMCs however, uniformization suffers from severe performance degradation. In this paper, we report on our observations and analysis of an alternative technique using Krylov sub-spaces. We implemented a Krylov-based extension to MRMC (Markov Reward Model Checker) and conducted extensive experiments on five case studies from different application domains. The results reveal that the Krylov-based technique is an order of magnitude faster on stiff CTMCs.