安全与协安全语言的一阶逻辑刻画
人工智能
2024-02-14 v5 计算机科学中的逻辑
摘要
线性时序逻辑（LTL）是最流行的时序逻辑之一，在计算机科学诸多分支中发挥作用。其广泛使用的诸多原因中包括其坚实的奠基性质：LTL 等价于无计数器 omega 自动机、星自由 omega 正则表达式，以及（由 Kamp 定理）线性序一阶理论（FO-TLO）。安全与协安全语言（分别只需有限前缀即可确定某词不属于或属于该语言）在降低如 LTL 的模型检测与时序综合等问题的复杂度方面起关键作用。SafetyLTL（resp., coSafetyLTL）是 LTL 的一个片段，仅允许全称（resp., 存在）时序模态，仅识别安全（resp., 协安全）语言。本文的主要贡献是引入 FO-TLO 的一个片段，称为 SafetyFO，及其对偶 coSafetyFO，它们在表达力上相对于 LTL 可定义的安全与协安全语言是完备的。我们证明它们分别精确刻画 SafetyLTL 与 coSafetyLTL，该结果补充了 Kamp 定理，并更清晰地展现了以一阶语言刻画 LTL（片段）的图景。此外，它给出任一 LTL 可定义安全语言亦可由 SafetyLTL 定义的直截、紧凑且自包含的 proof。作为副产物，我们获得关于 SafetyLTL 弱明天算子（在有限与无限词上解释）表达力的一些有趣结果。而且，我们证明当在有限词上解释时，不含明天（resp., 弱明天）算子的 SafetyLTL（resp. coSafetyLTL）恰好捕获有限词上 LTL 的安全（resp., 协安全）片段。
引用
@article{arxiv.2209.02307,
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= {arXiv preprint arXiv:2209.02307},
year = {2024}
}