Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems (extended version)
Lecture Notes in Computer Science Foundations of Software Science and Computation Structures(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要