A first-order logic characterization of safety and co-safety languages

Linear Temporal Logic (LTL) is one of the most popular temporal logics and comes into play in a variety of branches of computer science. Among the various reasons of its widespread use there are its strong foundational properties: LTL is equivalent to counter-free ω-automata, to star-free ω-regular expressions, and (by Kamp's theorem) to the First-Order Theory of Linear Orders (FO-TLO). Safety and co-safety languages, where a finite prefix suffices to establish whether a word does not belong or belongs to the language, respectively, play a crucial role in lowering the complexity of problems like model checking and reactive synthesis for LTL. Safety-LTL (resp., coSafety-LTL) is a fragment of LTL where only the tomorrow, the weak tomorrow and the until temporal modalities (resp., the tomorrow, the weak tomorrow and the release temporal modalities) are allowed, that recognises safety (resp., co-safety) languages only. The main contribution of this paper is the introduction of a fragment of FO-TLO, called Safety-FO, and of its dual coSafety-FO, which are expressively complete with respect to the LTL-definable safety and co-safety languages. We prove that they exactly characterize Safety-LTL and coSafety-LTL, respectively, a result that joins Kamp's theorem, and provides a clearer view of the characterization of (fragments of) LTL in terms of first-order languages. In addition, it gives a direct, compact, and self-contained proof that any safety language definable in LTL is definable in Safety-LTL as well. As a by-product, we obtain some interesting results on the expressive power of the weak tomorrow operator of Safety-LTL, interpreted over finite and infinite words. Moreover, we prove that, when interpreted over finite words, Safety-LTL (resp.