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.

翻译：本文聚焦于不含二元时序算子（如until）的线性时序逻辑（LTL）片段的简洁性结果，并提供了建立这些结果的方法。我们证明存在一族安全语言（Ln）_{n≥1}，使得Ln可用规模为O(n)的纯未来公式表达，但需要规模为2^{Ω(n)}的过去公式才能刻画。作为推论，该简洁性结果证明了[Artale等人，KR，2023]提出的过去化算法的最优性。我们指出，在研究的案例中，无法依赖[Markey，Bull. EATCS，2003]提出的经典基于自动机的方法证明简洁性。为此，我们设计并应用了一个组合证明系统，其演绎树可表征LTL公式。该系统可视为对Adler与Immerman用于研究CTL简洁性的博弈的证明中心化（单人）视角。