通过组合证明系统研究LTL协安全片段的简洁性（扩展版）
计算机科学中的逻辑
2024-06-18 v2 形式语言与自动机理论
摘要
本文聚焦于不含until等二元时序算子的带过去线性时序逻辑片段的简洁性结果，并提供了建立这些结果的方法。我们证明存在一族协安全语言(Ln)_{n≥1}，使得Ln可以用大小为O(n)的纯未来公式表达，但需要用大小为2^{Ω(n)}的过去公式才能捕获。作为副产品，这一简洁性结果显示了[Artale et al., KR, 2023]中提出的过去化算法的最优性。我们证明，在所考虑的情况下，简洁性不能通过依赖[Markey, Bull. EATCS, 2003]中引入的经典基于自动机的方法来证明。取而代之，我们设计并应用了一个组合证明系统，其推导树表示LTL公式。该系统可以看作是Adler和Immerman用于研究CTL简洁性的博弈的以证明为中心的（单人）视角。
引用
@article{arxiv.2401.09860,
title = {Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems (extended version)},
author = {Luca Geatti and Alessio Mansutti and Angelo Montanari},
journal= {arXiv preprint arXiv:2401.09860},
year = {2024}
}