一句话：提出 FO-TLO 的 SafetyFO/coSafetyFO 片段，精确刻画 SafetyLTL 与 coSafetyLTL 并给出表达力结果。
LTL 具有 Kamp 定理等一阶逻辑刻画，但其安全与余安全片段对应的 FO-TLO 片段尚不明确。本文引入 FO-TLO 的 SafetyFO 及其对偶 coSafetyFO，证明二者分别对 LTL 可定义的安全和余安全语言表达完备，并精确刻画 SafetyLTL 与 coSafetyLTL，从而衔接 Kamp 定理。作者给出直接、紧凑且自包含的证明：任何 LTL 可定义的安全语言都可用 SafetyLTL 定义。作为副产品，论文还分析 SafetyLTL 中 weak tomorrow 算子在有限与无限字上的表达力，并证明在有限字上，不含 tomorrow 的 SafetyLTL 与不含 weak tomorrow 的 coSafetyLTL 分别捕获 LTL 的有限字安全与余安全片段。
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.
@article{paperbot2196,
title = {A first-order logic characterization of safety and co-safety languages},
author = {Alessandro Cimatti and Luca Geatti and Nicola Gigante and Angelo Montanari and Stefano Tonetta},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 3},
year = {2023},
doi = {10.46298/lmcs-19(3:13)2023}
}