Linear Temporal Logic (LTL) is one of the most popular temporal logics, that 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 omega-automata, to star-free omega-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. SafetyLTL (resp., coSafetyLTL) is a fragment of LTL where only universal (resp., existential) 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 SafetyFO, and of its dual coSafetyFO, which are expressively complete with respect to the LTL-definable safety and co-safety languages. We prove that they exactly characterize SafetyLTL and coSafetyLTL, 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 SafetyLTL as well. As a by-product, we obtain some interesting results on the expressive power of the weak tomorrow operator of SafetyLTL, interpreted over finite and infinite words. Moreover, we prove 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.

翻译：线性时序逻辑（LTL）是计算机科学多个分支中最常用的时序逻辑之一。其广泛应用的诸多原因包括其强大的基础性质：LTL等价于无圈ω-自动机、无星ω-正则表达式，并且（根据坎普定理）等价于线性序一阶理论（FO-TLO）。安全语言和协同安全语言是指，分别通过有限前缀即可判定某个词是否不属于或属于该语言，这类语言在降低LTL模型检测和反应式合成等问题的复杂度方面起着关键作用。SafetyLTL（相应地，coSafetyLTL）是LTL的片段，仅允许全称（相应地，存在）时序模态，且仅识别安全（相应地，协同安全）语言。本文的主要贡献是引入了FO-TLO的一个片段，称为SafetyFO，及其对偶coSafetyFO，它们在表达能力上完全覆盖了LTL可定义的安全和协同安全语言。我们证明它们分别精确刻画了SafetyLTL和coSafetyLTL，这一结果衔接了坎普定理，并为一阶语言对LTL（及其片段）的刻画提供了更清晰的视角。此外，该结果直接、紧凑且自包含地证明了LTL可定义的任何安全语言同样可由SafetyLTL定义。作为副产品，我们获得了关于SafetyLTL的弱“明天”算子（在有限词和无限词上解释）表达能力的一些有趣结果。进一步，我们证明，当在有限词上解释时，不含“明天”（相应地，弱“明天”）算子的SafetyLTL（相应地，coSafetyLTL）恰好捕获了有限词上LTL的安全（相应地，协同安全）片段。