Dependability Analysis with Markov Chains: How Symmetries Improve Symbolic Computations

We propose a novel approach that combines two general and complementary methods for dependability analysis based on the steady state or transient analysis of Markov chains. The first method allows us to automatically detect all symmetries in a compositional Markovian model with state-sharing composition. Symmetries are detected with the help of an automorphism group of the model composition graph, which yields a reduction of the associated Markov chain due to lumpability. The second method allows us to represent and numerically solve the lumped Markov chain, even in the case of very large state spaces, with the help of symbolic data structures, in particular matrix diagrams. The overall approach has been implemented and is able to compute stationary and transient measures for large Markovian models of dependable systems.