Traditional modeling tools for High Availability systems do not combine intuitivity, efficiency, and modeling power under the same umbrella. For example, combinatorial methods like fault trees or reliability block diagrams are quite intuitive, allow for a stepwise refinement of the models and can be analyzed efficiently. However, their modeling power is limited, as traditional methods for analyzing these models rely on the fact that there are no statistical dependencies between the failure and repair behavior of the components. In contrast, state-based modeling methods like Markov chains (either designed by hand [11] or generated from high-level diagrams like Petri nets [1]) allow for the modeling of arbitrary dependencies like: failure propagation, failures with a common cause, limited repair resources, standby/warm/cold-redundancy, physical dependencies, imperfect coverage, etc.