Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems (extended version)

Luca Geatti, Alessio Mansutti, Angelo Montanari

TL;DR

It is proved 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.

Abstract

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^Ω(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.

Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems (extended version)

TL;DR

It is proved 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.

Abstract

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^Ω(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.
Paper Structure (26 sections, 36 theorems, 26 equations, 2 figures)

This paper contains 26 sections, 36 theorems, 26 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Linear Temporal Logic with Past.
  4. Fragments of .
  5. The pastification problem.
  6. Succinctness.
  7. A problematic cosafety language for $\LTL[\tomorrow,\weaktomorrow,\eventually,\always]$
  8. A combinatorial proof system for $\LTL[\tomorrow,\weaktomorrow,\eventually,\always]$
  9. Further notation.
  10. The proof system
  11. Connections with the Adler--Immerman games
  12. The exponential lower bound for $\Phi_n$
  13. Setting up the sets of traces $\AA$ and $\BB$
  14. Separating $\AA$ from $\BB$ requires an exponential proof
  15. \ref{['theorem:LTLF-more-succint']}: a $2^{n}$ lower bound for $\LTL[\eventually]$ pastification
  16. ...and 11 more sections

Key Result

theorem 1

$\ltl{F}(\LTLPFinv)$ can be exponentially more succinct than $\LTLnountil$.

Figures (2)

  • Figure 1: The combinatorial proof system. Here, $A,B \subseteq \Sigma^+$.
  • Figure 2: A deduction tree proving $\separ{\{abaa,aaaa\},\{aaab\}}$. Here, $a \coloneqq \{p\}$ and ${b \coloneqq \emptyset}$.

Theorems & Definitions (61)

  • theorem 1
  • theorem 2
  • corollary 1
  • lemma 1
  • proof : Proof sketch
  • lemma 2
  • proof : Proof sketch
  • theorem 3
  • proof : Proof sketch
  • corollary 2
  • ...and 51 more