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.
ltl safety specification languages liveness bchi automata