Efficient LTL compilation for SAT-based model checking

This work describes an algorithm of automata construction for LTL safety properties, suitable for bounded model checking. Existing automata construction methods are tailored to BDD-based symbolic model checking. The novelty of our approach is that we construct deterministic automata, unlike the standard approach, which constructs nondeterministic automata. We show that the proposed method has significant advantages for bounded model checking over traditional methods.