# Generalizing Non-Punctuality for Timed Temporal Logic with Freeze Quantifiers

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 May 2021.

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

- [Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete](https://mlsanity.com/paper/2309.00386/) (2023)

## Abstract (arXiv)

Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) are prominent real-time extensions of Linear Temporal Logic (LTL). In general, the satisfiability checking problem for these extensions is undecidable when both the future U and the past S modalities are used. In a classical result, the satisfiability checking for MITL[U,S], a non punctual fragment of MTL[U,S], is shown to be decidable with EXPSPACE complete complexity. Given that this notion of non punctuality does not recover decidability in the case of TPTL[U,S], we propose a generalization of non punctuality called non adjacency for TPTL[U,S], and focus on its 1-variable fragment, 1-TPTL[U,S]. While non adjacent 1-TPTL[U,S] appears to be be a very small fragment, it is strictly more expressive than MITL. As our main result, we show that the satisfiability checking problem for non adjacent 1-TPTL[U,S] is decidable with EXPSPACE complete complexity.