Fast Dynamic Fault Tree Analysis by Model Checking Techniques

This paper presents a new state-space generation approach for dynamic fault trees (DFTs) that exploits several successful reduction techniques from the field of model checking. The key idea is to aggressively exploit the DFT structure-detecting symmetries, spurious non-determinism, and don't cares. Benchmarks show a gain of more than two orders of magnitude in terms of state-space generation and analysis time. This fast, scalable approach is complemented by an approximative technique that determines bounds on DFT measures by a partial state-space generation. This is shown to yield another order of magnitude gain while guaranteeing tight error bounds.