Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems (extended version)
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866911919595585536 |
|---|---|
| author | Geatti, Luca Mansutti, Alessio Montanari, Angelo |
| author_facet | Geatti, Luca Mansutti, Alessio Montanari, Angelo |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_09860 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems (extended version) Geatti, Luca Mansutti, Alessio Montanari, Angelo Logic in Computer Science Formal Languages and Automata Theory F.3.1; F.4.3 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. |
| title | Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems (extended version) |
| topic | Logic in Computer Science Formal Languages and Automata Theory F.3.1; F.4.3 |
| url | https://arxiv.org/abs/2401.09860 |