# Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 3 of its 44 references that are in the map.
- First posted on arXiv 1 Sep 2023.

## Builds on (most cited first, 3 of 3)

- [Metric Temporal Logic with Counting](https://mlsanity.com/paper/1512.09032/) (2015)
- [Revisiting Timed Logics with Automata Modalities](https://mlsanity.com/paper/1812.10146/) (2018)
- [Generalizing Non-Punctuality for Timed Temporal Logic with Freeze Quantifiers](https://mlsanity.com/paper/2105.09534/) (2021)

## Abstract (arXiv)

We investigate the decidability of the 0,∞ fragment of Timed Propositional Temporal Logic (TPTL). We show that the satisfiability checking of TPTL0,∞ is PSPACE-complete. Moreover, even its 1-variable fragment (1-TPTL0,∞) is strictly more expressive than Metric Interval Temporal Logic (MITL) for which satisfiability checking is EXPSPACE complete. Hence, we have a strictly more expressive logic with computationally easier satisfiability checking. To the best of our knowledge, TPTL0,∞ is the first multi-variable fragment of TPTL for which satisfiability checking is decidable without imposing any bounds/restrictions on the timed words (e.g. bounded variability, bounded time, etc.). The membership in PSPACE is obtained by a reduction to the emptiness checking problem for a new "non-punctual" subclass of Alternating Timed Automata with multiple clocks called Unilateral Very Weak Alternating Timed Automata (VWATA0,∞) which we prove to be in PSPACE. We show this by constructing a simulation equivalent non-deterministic timed automata whose number of clocks is polynomial in the size of the given VWATA0,∞.