线性时序逻辑（Linear Temporal Logic，LTL）是最受欢迎的时序逻辑之一，在计算机科学的各个分支中发挥着作用。其被广泛使用的众多原因之一在于其强大的基础特性：LTL等价于无计数 omega-自动机、无星 omega-正则表达式，并且（根据 Kamp 定理）等价于线性序的一阶理论（First-Order Theory of Linear Orders，FO-TLO）。安全语言和共安全语言——分别仅需有限前缀即可判定一个字是否不属于或属于该语言——在降低诸如 LTL 的模型检验和反应式综合等问题的复杂度方面发挥着关键作用。SafetyLTL（对应地，coSafetyLTL）是 LTL 的一个片段，仅允许使用全称（对应地，存在）时序模态，它只能识别安全（对应地，共安全）语言。本文的主要贡献是引入了 FO-TLO 的一个片段，称为 SafetyFO，以及其对偶形式 coSafetyFO，它们在表达能力上对于 LTL 可定义的安全语言和共安全语言是完全的。我们证明它们分别精确刻画了 SafetyLTL 和 coSafetyLTL，这一结果与 Kamp 定理相契合，并为用一阶语言刻画 LTL（及其片段）提供了更清晰的视角。此外，它给出了一个直接、紧凑且自洽的证明，即任何可在 LTL 中定义的安全语言同样可在 SafetyLTL 中定义。作为副产品，我们获得了关于 SafetyLTL 的弱明天算子在有限字和无限字上解释时所具表达能力的一些有趣结果。而且，我们证明，当在有限字上解释时，去除了明天算子（对应地，弱明天算子）的 SafetyLTL（对应地，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.
City University of Hong Kong（香港城市大学）；Rutgers University（罗格斯大学）；University of Science and Technology of China（中国科学技术大学）；Universiteit van Amsterdam（阿姆斯特丹大学）；Baidu Inc（百度公司）
NASP-T: A Fuzzy Neuro-Symbolic Transformer for Logic-Constrained Aviation Safety Report Classification
Faculty of Science and Technology (REALTEK)（科学与技术学院）；Norwegian University of Life Sciences (NMBU)（挪威生命科学大学）；Dresden International University (DIU)（德累斯顿国际大学）
RoboSafe: Safeguarding Embodied Agents via Executable Safety Logic
Beihang University（北航大学）；AI Security Lab（360AI安全实验室）；The University of Sydney（悉尼大学）；Nanyang Technological University（南洋理工大学）；Peking University（北京大学）；Beijing Academy of Artificial Intelligence（北京人工智能研究院）
Autoformalizing Natural Language to First-Order Logic: A Case Study in Logical Fallacy Detection
Stanford University（斯坦福大学）；X, the moonshot factory（X moonshot工厂）；Max Planck Institute for Intelligent Systems（马克斯·普朗克智能系统研究所）；ETH Zürich（苏黎世联邦理工学院）；University of Toronto（多伦多大学）
Self-Aware Safety Augmentation: Leveraging Internal Semantic Understanding to Enhance Safety in Vision-Language Models
Shanghai Key Laboratory of Computer Software Testing and Evaluating（上海软件测试与评估 key laboratory）；Shanghai Normal University（上海Normal University）；TrustAI Pte. Ltd.；East China Normal University（东华师范大学）
Q-resafe: Assessing Safety Risks and Quantization-aware Safety Patching for Quantized Large Language Models
The State Key Laboratory of Blockchain and Data Security, Zhejiang University（区块链与数据安全国家重点实验室，浙江大学）；Sun Yat-sen University（中山大学）；Hangzhou High-Tech Zone (Binjiang) Institute of Blockchain and Data Security（杭州高新技术区（滨江）区块链与数据安全研究院）
State-Dependent Safety Failures in Multi-Turn Language Model Interaction
School of Cyber Science and Technology, University of Science and Technology of China, China（中国科学技术大学信息科学与技术学院）；Nanyang Technological University, Singapore（南洋理工大学）；Tsinghua University, Beijing, China（清华大学）；Beijing Electronic Science and Technology Institute, Beijing, China（北京电子科技研究所）
LLM Safety Alignment in Low-Resource Languages: A Systematic Literature Review
African Institute for Mathematical Sciences (AIMS)（非洲数学科学研究所）；Bayero University Kano（卡诺贝罗大学）；Brown University（布朗大学）；Centrum Wiskunde & Informatica（数学与计算机科学中心）；University of Pretoria（比勒陀利亚大学）；University of Hamburg（汉堡大学）；Imperial College London（伦敦帝国学院）
