Higher-Order Quantifier Elimination, Counter Simulations and Fault-Tolerant Systems