This paper focuses on succinctness results for fragments of Linear Temporal Logic with Past (LTL) devoid of binary temporal operators like until, and provides methods to establish them. We prove that there is a family of cosafety languages (Ln)_{n>=1} such that Ln can be expressed with a pure future formula of size O(n), but it requires formulae of size 2^{\Omega}(n) to be captured with past formulae. As a by-product, such a succinctness result shows the optimality of the pastification algorithm proposed in [Artale et al., KR, 2023]. We show that, in the considered case, succinctness cannot be proven by relying on the classical automata-based method introduced in [Markey, Bull. EATCS, 2003]. In place of this method, we devise and apply a combinatorial proof system whose deduction trees represent LTL formulae. The system can be seen as a proof-centric (one-player) view on the games used by Adler and Immerman to study the succinctness of CTL.

翻译：本文聚焦于不含直到等二元时序算子的带过去算子线性时序逻辑（LTL）片段的简洁性结果，并提出了相关证明方法。我们证明存在一族协安全性语言（Ln）_{n≥1}，使得Ln可用大小为O(n)的纯将来公式表达，但用过去公式捕捉时需要大小为2^{Ω(n)}的公式。作为副产品，这一简洁性结果证明了[Artale等人，KR，2023]提出的过去化算法的最优性。我们指出，在所考虑的情形下，无法通过[Markey，Bull. EATCS，2003]中引入的经典自动机方法证明简洁性。作为替代，我们设计并应用了一种组合证明系统，其推导树可表示LTL公式。该系统可视为Adler与Immerman为研究计算树逻辑（CTL）简洁性所用博弈的以证明为中心（单参与者）视角。