Abstract
Linear Temporal Logic (LTL) is one of the most popular temporal logics, thatcomes into play in a variety of branches of computer science. Among the variousreasons of its widespread use there are its strong foundational properties: LTLis equivalent to counter-free omega-automata, to star-free omega-regularexpressions, and (by Kamp's theorem) to the first-order theory of one successor(S1S[FO]). Safety and co-safety languages, where a finite prefix suffices toestablish whether a word does not belong or belongs to the language,respectively, play a crucial role in lowering the complexity of problems likemodel checking and reactive synthesis for LTL. SafetyLTL (resp., coSafetyLTL)is a fragment of LTL where only universal (resp., existential) temporalmodalities are allowed, that recognises safety (resp., co-safety) languagesonly. The main contribution of this paper is the introduction of a fragment ofS1S[FO], called SafetyFO, and of its dual coSafetyFO, which are expressivelycomplete with respect to the LTL-definable safety and co-safety languages. Weprove that they exactly characterize SafetyLTL and coSafetyLTL, respectively, aresult that joins Kamp's theorem, and provides a clearer view of thecharacterization of (fragments of) LTL in terms of first-order languages. Inaddition, it gives a direct, compact, and self-contained proof that any safetylanguage definable in LTL is definable in SafetyLTL as well. As a by-product,we obtain some interesting results on the expressive power of the weak tomorrowoperator of SafetyLTL, interpreted over finite and infinite words. Moreover, weprove that, when interpreted over finite words, SafetyLTL (resp. coSafetyLTL)devoid of the tomorrow (resp., weak tomorrow) operator captures the safety(resp., co-safety) fragment of LTL over finite words.