# A New Rule for LTL Tableaux

arXiv: https://arxiv.org/abs/1609.04102 · HTML: https://mlsanity.com/paper/1609.04102/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Sep 2016.

## Built on by (most cited first, 4 of 4)

- [Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version)](https://mlsanity.com/paper/2204.13693/) (2022)
- [Decidable Fragments of LTLf Modulo Theories (Extended Version)](https://mlsanity.com/paper/2307.16840/) (2023)
- [Standpoint Linear Temporal Logic](https://mlsanity.com/paper/2304.14243/) (2023)
- [Enumerating Minimal Unsatisfiable Cores of LTLf formulas](https://mlsanity.com/paper/2409.09485/) (2024)

## Abstract (arXiv)

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.