TL;DR
This paper introduces a simple, traditional-style tree-shaped tableau system for propositional LTL, making satisfiability checking more accessible, easier to implement, and suitable for parallel processing.
Contribution
It presents a novel tableau rule for LTL that results in a simple, sound, complete, and traditional tree-shaped tableau system, improving usability and implementation.
Findings
The new tableau is sound and complete.
It is simpler to understand and implement than existing systems.
The tableau is competitive with state-of-the-art tools and suitable for parallelization.
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. In this paper, we introduce a novel style of tableau rule which supports a new simple traditional-style tree-shaped tableau for LTL. We prove that it is sound and complete. As well as being simple to understand, to introduce to students and to use, it is also simple to implement and is competitive against state of the art systems. 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.