Generalizing Non-Punctuality for Timed Temporal Logic with Freeze Quantifiers

TL;DR

This paper introduces a new fragment called non adjacency for TPTL with freeze quantifiers, proving its satisfiability is decidable and EXPSPACE complete, extending the boundaries of decidability in timed temporal logics.

Contribution

It generalizes the notion of non punctuality to TPTL, establishing decidability for the 1-variable fragment with EXPSPACE complexity, and surpasses MITL in expressiveness.

Findings

Decidability of satisfiability for non adjacent 1-TPTL[U,S]

EXPSPACE complete complexity result

More expressive than MITL

Abstract

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 \emph{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.