TL;DR
This paper introduces a new, simple, and traditional tree-shaped tableau method for LTL that is easy to understand, implement, and suitable for parallel processing, improving upon existing complex tableau systems.
Contribution
The paper presents a novel traditional-style tree-shaped tableau for LTL that is sound, complete, easy to understand, and well-suited for automation and parallel implementation.
Findings
Proves the tableau is sound and complete.
Simplifies understanding and implementation of LTL tableaux.
Enhances potential for parallel processing in automated reasoning.
Abstract
Propositional linear time temporal logic (LTL) is the standard temporal logic for computing applications and many reasoning techniques and tools have been developed for it. Tableaux for deciding satisfiability have existed since the 1980s. However, the tableaux for this logic do not look like traditional tree-shaped tableau systems and their processing is often quite complicated. We present a new simple traditional-style tree-shaped tableau for LTL and prove that it is sound and complete. As well as being simple to understand, to introduce to students and to use manually, it also seems simple to implement and promises to be competitive in its automation. It is particularly suitable for parallel implementations.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.