# One-Pass and Tree-Shaped Tableau Systems for TPTL and TPTLb+Past

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

## Key facts

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

## 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)
- [Computing unsatisfiable cores for LTLf specifications](https://mlsanity.com/paper/2203.04834/) (2022)

## Abstract (arXiv)

In this paper, we propose a novel one-pass and tree-shaped tableau method for Timed Propositional Temporal Logic and for a bounded variant of its extension with past operators. Timed Propositional Temporal Logic (TPTL) is a real-time temporal logic, with an EXPSPACE-complete satisfiability problem, which has been successfully applied to the verification of real-time systems. In contrast to LTL, adding past operators to TPTL makes the satisfiability problem for the resulting logic (TPTL+P) non-elementary. In this paper, we devise a one-pass and tree-shaped tableau for both TPTL and bounded TPTL+P (TPTLb+P), a syntactic restriction introduced to encode timeline-based planning problems, which recovers the EXPSPACE-complete complexity. The tableau systems for TPTL and TPTLb+P are presented in a unified way, being very similar to each other, providing a common skeleton that is then specialised to each logic. In doing that, we characterise the semantics of TPTLb+P in terms of a purely syntactic fragment of TPTL+P, giving a translation that embeds the former into the latter. Soundness and completeness of the system are proved fully. In particular, we give a greatly simplified model-theoretic completeness proof, which sidesteps the complex combinatorial argument used by known proofs for the one-pass and tree-shaped tableau systems for LTL and LTL+P.