Combining decomposition and reduction for state space analysis of a self-stabilizing system

Fault tolerance measures of distributed systems can be calculated precisely by state space analysis of the Markov chain corresponding to the product of the system components. The power of such an approach is inherently confined by the state space explosion, i.e. the exponential growth of the Markov chain in the size of the underlying system. We propose a decompositional method to alleviate this limitation. Lumping is a well-known reduction technique facilitating computation of the relevant measures on the quotient of the Markov chain under lumping equivalence. In order to avoid computation of lumping equivalences on intractably large Markov chains, we propose a system decomposition supporting local lumping on the considerably smaller Markov chains of the subsystems. Recomposing the lumped Markov chains of the subsystems constructs a lumped transition model of the whole system, thus avoiding the construction of the full product chain. An example demonstrates how the limiting window availability (i.e. a particular fault tolerance measure) can be computed for a self-stabilizing system exploiting lumping and decomposition.

► Hierarchical self-stabilizing systems allow composing transition models along DAGs.
► Without hierarchy, evaluating fault tolerance is exponential in the component count.
► Lumping prunes redundant information in the transition model.
► Local lumping before composition avoids construction of the full transition model.
► DAG allows for sequential construction and thereby for lumping to be applied locally.