The present book focuses on distributed systems operating under probabilistic influences like faults. How well can such systems provide their service under the effects of faults? How well can they recover from faults? Along with a thorough introduction into the area of fault tolerance, this book introduces a measure called limiting window availability to answer such questions. Furthermore, a method for computing the limiting window availability based on constructing the transition models from the system and environment models is developed. The method yet hinges on the transition model being exponential in the size of the constituting system models. This effect is commonly known as state space explosion. Combining decomposition and lumping methods for reducing the state space from the domain of model checking yet allows to dampen the state space explosion, thus enhancing the spectrum of systems that are tractable for an analysis significantly.