The predominant technique for computing the transient distribution of a Continuous Time Markov Chain (CTMC) exploits uniformization, 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 subspaces. 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. © 2010 Springer-Verlag.
CITATION STYLE
Dulat, F., Katoen, J. P., & Nguyen, V. Y. (2010). Model checking Markov chains using Krylov subspace methods: An experience report. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6342 LNCS, pp. 115–130). https://doi.org/10.1007/978-3-642-15784-4_8
Mendeley helps you to discover research relevant for your work.