LTL is closed under topological closure

• We show that the smallest safety property containing any LTL formula is in LTL.
• We prove the safety-liveness decomposition theorem for LTL.
• We construct aperiodic Buchi automata from safety LTL formulas.

We constructively prove that for every LTL formula φ, the smallest safety property containing the property expressed by φ is also expressible in LTL. It immediately follows that LTL admits the safety-liveness decomposition: any property expressed by an LTL formula is equivalent to the intersection of a safety property and a liveness property, both of them expressible in LTL. Our proof is based on constructing a minimal deterministic counter-free Büchi automaton that recognizes the smallest safety property containing the property expressed by φ.