| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 427447 | Information Processing Letters | 2014 | 6 Pages |
•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 φ.
