Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems

This paper focuses on succinctness results for fragments of Linear Temporal Logic with Past ( \(\textsf{LTL}\) ) devoid of binary temporal operators like until, and provides methods to establish them. We prove that there is a family of cosafety languages \((\mathcal {L}_n)_{n \ge 1}\) such that \(\mathcal {L}_n\) can be expressed with a pure future formula of size \(\mathcal {O}(n)\) , but it requires formulae of size \(2^{\varOmega (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 \(\textsf{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  \(\textsf{CTL}\) .